Integrability propagated by one exact R-322 residual collapse

The proper-prefix value identity needs full integrability of the current residual in order to apply Fubini. This file proves that the same property is inherited by the post-collapse residual. The proof transports the current integrable function through the genuine coordinate split, integrates the removed block, and then uses the exact local collapse identity. No pointwise majorant for the complete residual is assumed.

theorem Anderson4D.R322AnalyticResidualPrefix.integrable_residualIntegrand_afterProper {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (z : T4) (hint : MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => res.residualIntegrand ρ ε (res.reconstruct z v)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hstandard : ∀ᵐ (outer : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable ((res.properStepContext step suffix hremaining hproper).localIntegrand ρ ε ((res.properStepContext step suffix hremaining hproper).predecessorPoint ((res.afterProper step suffix hremaining hproper).reconstruct z outer) - (res.properStepContext step suffix hremaining hproper).successorPoint ((res.afterProper step suffix hremaining hproper).reconstruct z outer))) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (res.properStepContext step suffix hremaining hproper).step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder step.2) (↑κB) (res.properStepContext step suffix hremaining hproper).internalEdges (primitiveAssemble (residualBlockOrder step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2 - 2)) => paperMeasure)) : MeasureTheory.Integrable (fun (outer : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4) => (res.afterProper step suffix hremaining hproper).residualIntegrand ρ ε ((res.afterProper step suffix hremaining hproper).reconstruct z outer)) (MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) => paperMeasure)

Full residual integrability is preserved by one genuine proper collapse. The section hypotheses are precisely those already consumed by residualValue_eq_afterProper.

Initial residual ledger

theorem Anderson4D.R322AnalyticResidualPrefix.initial_residualChainEdgeFactor_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (x : Fin (2 * q) → T4) (edge : Fin (2 * q - 1)) : (initial ρ lam ε hq κ hκ).residualChainEdgeFactor x edge = r322AnalyticChainEdgeFactorWith (fun (x : Fin (2 * q - 1)) => greenFn) κ x edge

At the initial all-active state, one sparse residual chain factor is literally the corresponding free-Green analytic chain factor.

theorem Anderson4D.R322AnalyticResidualPrefix.initial_residualChainProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (x : Fin (2 * q) → T4) : (initial ρ lam ε hq κ hκ).residualChainProduct x = r322AnalyticChainProductWith (fun (x : Fin (2 * q - 1)) => greenFn) κ x

The complete initial sparse chain is the frozen analytic Green chain.

theorem Anderson4D.R322AnalyticResidualPrefix.initial_residualStepDifference_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (x : Fin (2 * q) → T4) (step : R322ExtractionStep (2 * q)) : (initial ρ lam ε hq κ hκ).residualStepDifference x step = diffFactorJWith (fun (x : Fin (2 * q - 1)) => greenFn) x step.1

At the initial state, every residual signed difference reads the ordinary adjacent Green edge and hence equals diffFactorJWith.

theorem Anderson4D.R322AnalyticResidualPrefix.initial_residualDifferenceProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (x : Fin (2 * q) → T4) : (initial ρ lam ε hq κ hκ).residualDifferenceProduct x = r322AnalyticDiffProductWith (fun (x : Fin (2 * q - 1)) => greenFn) (r322AnalyticSchedule κ) x

The complete initial signed-difference product is the analytic schedule difference product.

theorem Anderson4D.R322AnalyticResidualPrefix.initial_remainingBlockIndex_eq_analyticBlockEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (j : Fin (r322AnalyticSchedule κ).length) : (initial ρ lam ε hq κ hκ).remainingBlockIndex j = (r322AnalyticBlockEquiv κ) j

The initial remaining-block coordinate is exactly the canonical analytic-schedule block coordinate.

theorem Anderson4D.R322AnalyticResidualPrefix.initial_residualPrimitiveProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (x : Fin (2 * q) → T4) : (initial ρ lam ε hq κ hκ).residualPrimitiveProduct ρ ε x = ∏ B : ExtractionBlockIndex κ, r322ExtractionBlockPrimitiveSum ρ ε κ B x

The initial primitive product contains every extraction block exactly once.

theorem Anderson4D.R322AnalyticResidualPrefix.initial_residualIntegrand_eq_initialResidualIntegrand (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (x : Fin (2 * q) → T4) : (initial ρ lam ε hq κ hκ).residualIntegrand ρ ε x = r322InitialResidualIntegrand ρ ε κ head tail hschedule x

The complete initial residual integrand is exactly the existing endpoint-fibre integrand, expressed in the head-local/outer coordinates.

Initial surviving-coordinate reindex

def Anderson4D.R322AnalyticResidualPrefix.initialInternalEquivSurviving {q : ℕ} (ρ : SmoothCutoff) (lam ε : ℝ) {q✝ : ℕ} (hq : 1 ≤ q✝) (κ : PartialPairing (Fin (2 * q✝))) (hκ : κ ∈ nonSplitPairings q✝) : Fin (2 * q✝ - 2) ≃ (initial ρ lam ε hq κ hκ).SurvivingCoordinate

The initial residual surviving coordinates are exactly the ordinary internal coordinates 1, ..., 2q-2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.R322AnalyticResidualPrefix.initialInternalPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : ((initial ρ lam ε hq κ hκ).SurvivingCoordinate → T4) ≃ᵐ (Fin (2 * q - 2) → T4)

Measurable reindex from the initial sparse carrier to the standard internal-coordinate tuple.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R322AnalyticResidualPrefix.measurePreserving_initialInternalPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : MeasureTheory.MeasurePreserving (⇑(initialInternalPiMeasurableEquiv ρ lam ε hq κ hκ)) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε hq κ hκ).SurvivingCoordinate) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)

The initial internal-coordinate reindex preserves the paper product measure exactly.

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.initialInternalPiMeasurableEquiv_apply (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (v : (initial ρ lam ε hq κ hκ).SurvivingCoordinate → T4) (j : Fin (2 * q - 2)) : (initialInternalPiMeasurableEquiv ρ lam ε hq κ hκ) v j = v ((initialInternalEquivSurviving ρ lam ε hq κ hκ) j)

theorem Anderson4D.R322AnalyticResidualPrefix.initial_reconstruct_eq_primitiveAssemble (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (z : T4) (v : (initial ρ lam ε hq κ hκ).SurvivingCoordinate → T4) : (initial ρ lam ε hq κ hκ).reconstruct z v = primitiveAssemble q hq z 0 ((initialInternalPiMeasurableEquiv ρ lam ε hq κ hκ) v)

Reconstructing the ambient tuple after the initial reindex gives the standard primitive assembly with endpoints z and 0.

theorem Anderson4D.R322AnalyticResidualPrefix.integrable_initial_residualIntegrand_of_schedule (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : MeasureTheory.Integrable (fun (v : (initial ρ lam ε hq κ hκ).SurvivingCoordinate → T4) => (initial ρ lam ε hq κ hκ).residualIntegrand ρ ε ((initial ρ lam ε hq κ hκ).reconstruct z v)) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε hq κ hκ).SurvivingCoordinate) => paperMeasure)

Integrability of the genuine endpoint-fibre sections transports to the initial sparse residual for a displayed nonempty analytic schedule.

theorem Anderson4D.R322AnalyticResidualPrefix.integrable_initial_residualIntegrand (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : MeasureTheory.Integrable (fun (v : (initial ρ lam ε hq κ hκ).SurvivingCoordinate → T4) => (initial ρ lam ε hq κ hκ).residualIntegrand ρ ε ((initial ρ lam ε hq κ hκ).reconstruct z v)) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε hq κ hκ).SurvivingCoordinate) => paperMeasure)

Integrability of the genuine endpoint-fibre sections gives full integrability of the canonical initial residual. Schedule nonemptiness is derived from non-splitting rather than assumed.

theorem Anderson4D.R322AnalyticResidualPrefix.endpointFiberDetJSum_eq_initial_residualValue (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = (initial ρ lam ε hq κ hκ).residualValue ρ lam ε z

The grouped endpoint fibre is exactly the scalar value of the canonical initial residual. This is only the finite-sum and product-coordinate reindexing ledger; no collapse estimate is used.