Quantitative iteration for complete grouped cross heads

Paper Section 4.2, Steps 2(f)--3 keep the complete primitive-pairing sum grouped while the nested cross blocks are removed. This file is the quantitative iterator for that grouped object. It is deliberately neutral about the final (outermost) block: a later physical factorization supplies the terminal density and this iterator charges only the proper heads before it.

No triangle inequality over primitive pairings occurs here.

inductive Anderson4D.R324CompleteNestedCrossBudgetRun {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ρ : SmoothCutoff) (lam ε : ℝ) (res : R324NestedCrossResidualPrefix κp κm π) : ((↥res.activeCarrier → T4) → ℝ) → ℕ → ℕ → Prop

A budget-ready nested run whose proper constructors use the complete primitive-pairing head. The stop density is kept abstract so that the outermost block can later be bounded by one final application of Proposition 4.1 rather than by another scalar proper-head estimate.

• stop {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} (res : R324NestedCrossResidualPrefix κp κm π) (density : (↥res.activeCarrier → T4) → ℝ) (hnonneg : ∀ (v : ↥res.activeCarrier → T4), 0 ≤ density v) (hintegrable : MeasureTheory.Integrable density (MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure)) : R324CompleteNestedCrossBudgetRun ρ lam ε res density 0 res.remainingOrder
• proper {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} (ctx : R324NestedCrossProperStepContext κp κm π) (nextDensity : (ctx.step.PostCoordinate → T4) → ℝ) (nextPrefixOrder terminalOrder : ℕ) (next : R324CompleteNestedCrossBudgetRun ρ lam ε ctx.step.next nextDensity nextPrefixOrder terminalOrder) (hintegrable : MeasureTheory.Integrable (fun (v : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.completeNormalizedHeadDensity ρ 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)) * nextDensity fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure)) : R324CompleteNestedCrossBudgetRun ρ lam ε ctx.step.residual (fun (v : ↥ctx.step.residual.activeCarrier → T4) => ((ctx.step.completeNormalizedHeadDensity ρ 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)) * nextDensity fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (ctx.step.order + nextPrefixOrder) terminalOrder

theorem Anderson4D.R324CompleteNestedCrossBudgetRun.density_integrable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324CompleteNestedCrossBudgetRun ρ lam ε res density prefixOrder terminalOrder) : MeasureTheory.Integrable density (MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure)

theorem Anderson4D.R324CompleteNestedCrossBudgetRun.density_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324CompleteNestedCrossBudgetRun ρ lam ε res density prefixOrder terminalOrder) (v : ↥res.activeCarrier → T4) : 0 ≤ density v

theorem Anderson4D.R324CompleteNestedCrossBudgetRun.remainingOrder_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324CompleteNestedCrossBudgetRun ρ lam ε res density prefixOrder terminalOrder) : res.remainingOrder = prefixOrder + terminalOrder

The proper-prefix and terminal orders partition the literal remaining cross schedule.

theorem Anderson4D.R324CompleteNestedCrossBudgetRun.integral_completeProperDensity_of_current_integrable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} (ctx : R324NestedCrossProperStepContext κp κm π) (nextDensity : (ctx.step.PostCoordinate → T4) → ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (hcurrent : MeasureTheory.Integrable (fun (v : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.completeNormalizedHeadDensity ρ 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)) * nextDensity fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure)) : (∫ (v : ctx.step.SurvivingCoordinate → T4), ((ctx.step.completeNormalizedHeadDensity ρ 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)) * nextDensity fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i) ∂MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure) = ∫ (post : ctx.step.PostCoordinate → T4), ctx.completeProperHeadIntegral ρ lam ε (post ctx.nextLeftPostCoordinate) (post ctx.nextRightPostCoordinate) * nextDensity post ∂MeasureTheory.Measure.pi fun (x : ctx.step.PostCoordinate) => paperMeasure

Exact Fubini transition for one complete grouped proper head. Joint integrability of the current density supplies the almost-everywhere section integrability needed to invoke the complete-head endpoint identity.

theorem Anderson4D.R324CompleteNestedCrossBudgetRun.exists_terminal_integral_le {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε D : ℝ} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324CompleteProperHeadSharpProvider ρ lam ε D κp κm π) (run : R324CompleteNestedCrossBudgetRun ρ lam ε res density prefixOrder terminalOrder) : ∃ (terminalRes : R324NestedCrossResidualPrefix κp κm π) (terminalDensity : (↥terminalRes.activeCarrier → T4) → ℝ), terminalOrder = terminalRes.remainingOrder ∧ (∀ (v : ↥terminalRes.activeCarrier → T4), 0 ≤ terminalDensity v) ∧ MeasureTheory.Integrable terminalDensity (MeasureTheory.Measure.pi fun (x : ↥terminalRes.activeCarrier) => paperMeasure) ∧ (∫ (v : ↥res.activeCarrier → T4), density v ∂MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure) ≤ (D * lam) ^ (2 * prefixOrder) * ∫ (v : ↥terminalRes.activeCarrier → T4), terminalDensity v ∂MeasureTheory.Measure.pi fun (x : ↥terminalRes.activeCarrier) => paperMeasure

Iterating the complete proper-head estimate reaches one genuine terminal density and charges exactly the accumulated proper-prefix order.