Quantitative proper-prefix iteration for R-324 Step 3

The physical-to-canonical boundary produces a proof-relevant proper-prefix factorization and stops at the block carrying the selected projected covariance. This file performs only the quantitative integration of the proper heads preceding that block.

The sole analytic input is a transparent local provider for one proper head: its exact normalized head/connector density is integrable for every fixed next-suffix configuration, and its endpoint integral is bounded by the named even perturbative power. No final R-324 estimate, frequency decay, or target-shaped reduction predicate appears here.

The output retains the actual four-endpoint terminal payload exposed by the stop constructor. In particular, the Step 4 routing machinery still sees the original external endpoints and the complete marked/suffix context.

structure Anderson4D.R324ProperHeadSharpProvider (ρ : SmoothCutoff) (lam ε D : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Prop

Transparent local analytic provider for one proper nested cross head.

The constant D is the already-absorbed one-head constant. A later consumer obtains such a provider from the sharp proper inserted convolution estimate, absorbing its fixed scalar cost into D.

• headIntegral_le (ctx : R324NestedCrossProperStepContext κp κm π) (left right : T4) : ctx.properHeadIntegral ρ lam ε left right ≤ (D * lam) ^ (2 * ctx.step.order)

theorem Anderson4D.R324ProperHeadSharpProvider.exists_at_truncation (ρ : SmoothCutoff) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) {lam ε : ℝ} (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) : ∃ (D : ℝ), 0 < D ∧ R324ProperHeadSharpProvider ρ lam ε D κp κm π

Proposition 4.1 together with the sharp proper inserted convolution produces one fixed-ambient provider throughout the truncation range.

The ambient order is fixed in the provider type because Proposition 4.1 is only available under m ≤ truncOrder ε. The one-head scalar K is absorbed into D = max 1 K * C; positivity and the fact that every literal block has order at least one justify this absorption uniformly over all heads in the ambient schedule.

inductive Anderson4D.R324NestedCrossBudgetRun {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ρ : SmoothCutoff) (lam ε : ℝ) (stopCarrier : Finset (Fin (2 * m))) (x y z w : T4) (res : R324NestedCrossResidualPrefix κp κm π) : ((↥res.activeCarrier → T4) → ℝ) → ℕ → ℕ → Prop

The canonical majorant data needed by the quantitative iteration, with the physical source comparison erased only after it has generated the exact constructor-by-constructor majorant.

This auxiliary relation avoids dependent elimination through the a.e. proof fields of R324NestedCrossContextFactorization; no hypothesis is added.

• stop {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} (step : R324NestedCrossStepContext κp κm π) (hstop : step.head.carrier = stopCarrier) (context : T4 → T4 → T4 → T4 → (step.SurvivingCoordinate → T4) → ℝ) (hcontext : ∀ (v : step.SurvivingCoordinate → T4), 0 ≤ context x y z w v) (hmajorant : MeasureTheory.Integrable (R324NestedCrossTerminalPayload.ofContext lam ε step context x y z w).density (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure)) : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w step.residual (R324NestedCrossTerminalPayload.ofContext lam ε step context x y z w).density 0 step.residual.remainingOrder
• proper {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} (ctx : R324NestedCrossProperStepContext κp κm π) (hhead : ctx.step.head.carrier ≠ stopCarrier) (nextMajorant : (ctx.step.PostCoordinate → T4) → ℝ) (nextPrefixOrder terminalOrder : ℕ) (next : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w ctx.step.next nextMajorant nextPrefixOrder terminalOrder) (hmajorant : MeasureTheory.Integrable (fun (v : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextMajorant fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure)) : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w ctx.step.residual (fun (v : ↥ctx.step.residual.activeCarrier → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextMajorant fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (ctx.step.order + nextPrefixOrder) terminalOrder

theorem Anderson4D.R324NestedCrossContextFactorization.toBudgetRun {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} {res : R324NestedCrossResidualPrefix κp κm π} {source majorant : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (factorization : R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w res source majorant prefixOrder terminalOrder) : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w res majorant prefixOrder terminalOrder

Erase the physical source only after the honest local factorization has generated its canonical majorant and recursive integrability data.

theorem Anderson4D.R324NestedCrossBudgetRun.majorant_integrable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} {res : R324NestedCrossResidualPrefix κp κm π} {majorant : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w res majorant prefixOrder terminalOrder) : MeasureTheory.Integrable majorant (MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure)

Every majorant in a budget-ready run is genuinely integrable.

theorem Anderson4D.R324NestedCrossBudgetRun.majorant_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} {res : R324NestedCrossResidualPrefix κp κm π} {majorant : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w res majorant prefixOrder terminalOrder) (v : ↥res.activeCarrier → T4) : 0 ≤ majorant v

Every majorant in a budget-ready run is pointwise nonnegative.

theorem Anderson4D.R324NestedCrossBudgetRun.exists_terminalPayload_integral_le {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε D : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} {res : R324NestedCrossResidualPrefix κp κm π} {majorant : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (provider : R324ProperHeadSharpProvider ρ lam ε D κp κm π) (run : R324NestedCrossBudgetRun ρ lam ε stopCarrier x y z w res majorant prefixOrder terminalOrder) : ∃ (step : R324NestedCrossStepContext κp κm π) (_ : step.head.carrier = stopCarrier) (payload : R324NestedCrossTerminalPayload lam ε step), payload.x = x ∧ payload.y = y ∧ payload.z = z ∧ payload.w = w ∧ terminalOrder = step.residual.remainingOrder ∧ (∀ (v : step.SurvivingCoordinate → T4), 0 ≤ payload.unscaledDensity v) ∧ MeasureTheory.Integrable payload.density (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ∧ (∫ (v : ↥res.activeCarrier → T4), majorant v ∂MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure) ≤ (D * lam) ^ (2 * prefixOrder) * ∫ (v : step.SurvivingCoordinate → T4), payload.density v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure

Iterating the proper-head bound leaves the actual endpoint-preserving terminal payload and charges exactly the total proper-prefix order.

Besides the quantitative integral inequality, the witness records:

• the genuine stop head and its carrier equality;
• all four original external endpoints;
• the exact terminal perturbative order;
• pointwise nonnegativity of the unscaled terminal context; and
• genuine integrability of the weighted terminal density.

theorem Anderson4D.R324NestedCrossContextFactorization.exists_terminalPayload_integral_le {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε D : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} {res : R324NestedCrossResidualPrefix κp κm π} {source majorant : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (provider : R324ProperHeadSharpProvider ρ lam ε D κp κm π) (factorization : R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w res source majorant prefixOrder terminalOrder) : ∃ (step : R324NestedCrossStepContext κp κm π) (_ : step.head.carrier = stopCarrier) (payload : R324NestedCrossTerminalPayload lam ε step), payload.x = x ∧ payload.y = y ∧ payload.z = z ∧ payload.w = w ∧ terminalOrder = step.residual.remainingOrder ∧ (∀ (v : step.SurvivingCoordinate → T4), 0 ≤ payload.unscaledDensity v) ∧ MeasureTheory.Integrable payload.density (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ∧ (∫ (v : ↥res.activeCarrier → T4), majorant v ∂MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure) ≤ (D * lam) ^ (2 * prefixOrder) * ∫ (v : step.SurvivingCoordinate → T4), payload.density v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure

Quantitative consumer for the honest physical-to-canonical factorization. The source comparison has already been used to construct majorant; the conclusion retains the genuine stop payload.

theorem Anderson4D.R324InitialNestedContextFactorization.exists_terminalPayload_physicalIntegral_le {ρ : SmoothCutoff} {lam ε D : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {terminal : R324TwoHalfTerminalData ρ lam ε κp κm} {L : ℝ} {x y z w : T4} (provider : R324ProperHeadSharpProvider ρ lam ε D κp κm π) (factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w) (hphysical : MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)) : ∃ (step : R324NestedCrossStepContext κp κm π) (_ : step.head.carrier = r324MarkedResidualBlock κp κm π selected) (payload : R324NestedCrossTerminalPayload lam ε step), payload.x = x ∧ payload.y = y ∧ payload.z = z ∧ payload.w = w ∧ factorization.terminalOrder = step.residual.remainingOrder ∧ (∀ (v : step.SurvivingCoordinate → T4), 0 ≤ payload.unscaledDensity v) ∧ MeasureTheory.Integrable payload.density (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ∧ lamEps lam ε ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ‖∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ (D * lam) ^ (2 * factorization.prefixOrder) * ∫ (v : step.SurvivingCoordinate → T4), payload.density v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure

End-to-end Step 3 handoff from the physical initial nested integral to the actual endpoint-preserving terminal payload. This composes the honest physical-source comparison with the quantitative proper-prefix iteration; no target-shaped final R-324 estimate is inserted.