Joint integrability through a stopped R-324 trace

This module propagates genuine joint integrability through every block actually consumed by an R324WithinHalfStopBeforeStepTrace. The measured parameter may control both displayed endpoints and the final outer factor. The proof invokes the concrete one-head joint-integrability theorem at every step and stops before the named retained block.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.integrable_joint_residualIntegrand_mul_stopOuter_stopPrefix {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (x y : Y → T4) (outer : Y → (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) (hcurrent : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => ↑(res.residualIntegrand ρ ε (x p.1) (y p.1) (res.reconstruct p.2)) * outer p.1 (trace.stopProjection p.2)) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (fun (p : Y × (trace.stopPrefix.SurvivingCoordinate → T4)) => ↑(trace.stopPrefix.residualIntegrand ρ ε (x p.1) (y p.1) (trace.stopPrefix.reconstruct p.2)) * outer p.1 p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : trace.stopPrefix.SurvivingCoordinate) => paperMeasure))

Joint integrability propagates through every genuine head consumed by a stopped trace.

The hypothesis is the actual current residual density multiplied by the final stop outer factor pulled back through stopProjection. The conclusion is the corresponding actual stopped residual density.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.integrable_residualIntegrand_mul_stopOuter_stopPrefix {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (x y : T4) (outer : (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) (hcurrent : MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct v)) * outer (trace.stopProjection v)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : MeasureTheory.Integrable (fun (v : trace.stopPrefix.SurvivingCoordinate → T4) => ↑(trace.stopPrefix.residualIntegrand ρ ε x y (trace.stopPrefix.reconstruct v)) * outer v) (MeasureTheory.Measure.pi fun (x : trace.stopPrefix.SurvivingCoordinate) => paperMeasure)

Scalar specialization of the joint theorem.

This is the exact premise needed to conclude ordinary integrability of the stopped residual density with a fixed pair of displayed endpoints.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.eventually_weightedIntegrableAlong_of_integrable_joint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (x y : Y → T4) (outer : Y → (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) (hcurrent : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => ↑(res.residualIntegrand ρ ε (x p.1) (y p.1) (res.reconstruct p.2)) * outer p.1 (trace.stopProjection p.2)) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : ∀ᵐ (a : Y) ∂ν, WeightedIntegrableAlong (x a) (y a) trace (outer a)

Joint integrability at the current prefix supplies, for almost every parameter, all scalar weighted-integrability hypotheses traversed by the stopped trace.

The proof is itself a trace induction. At each step, product integrability gives the current scalar section almost everywhere, while the concrete one-head joint theorem propagates the joint premise to the induction hypothesis.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.lamEps_pow_integral_joint_mul_stopOuter_eq_stop {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (x y : Y → T4) (outer : Y → (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) (hcurrent : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => ↑(res.residualIntegrand ρ ε (x p.1) (y p.1) (res.reconstruct p.2)) * outer p.1 (trace.stopProjection p.2)) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : ↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (p : Y × (res.SurvivingCoordinate → T4)), ↑(res.residualIntegrand ρ ε (x p.1) (y p.1) (res.reconstruct p.2)) * outer p.1 (trace.stopProjection p.2) ∂ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * trace.stopPrefix.remainingOrder) * ∫ (p : Y × (trace.stopPrefix.SurvivingCoordinate → T4)), ↑(trace.stopPrefix.residualIntegrand ρ ε (x p.1) (y p.1) (trace.stopPrefix.reconstruct p.2)) * outer p.1 p.2 ∂ν.prod (MeasureTheory.Measure.pi fun (x : trace.stopPrefix.SurvivingCoordinate) => paperMeasure)

Exact joint integral transport through every block consumed by the stopped trace.

Both sides are genuine product-space integrals. The named stop step and its suffix remain unintegrated, so the right-hand side retains the exact power 2 * trace.stopPrefix.remainingOrder.