Exact signed collapse of the grouped initial residual fibre

This file discharges the section-integrability premises of the existing certified two-half collapse. It uses only the already proved initial residual integrability, terminal trace propagation, and the bounded grouped residual covariance factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.measurable_terminalProjection {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) : Measurable trace.terminalProjection

The literal head/post restrictions traversed by a certified trace give a measurable projection onto its terminal sparse carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_initialRootResidualSum_eq_initialNested_of_sections {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hleftSection : MeasureTheory.Integrable (fun (vl : (initial ρ lam ε κp).SurvivingCoordinate → T4) => ↑((initial ρ lam ε κp).residualIntegrand ρ ε x y ((initial ρ lam ε κp).reconstruct vl))) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure)) (hrightSection : MeasureTheory.Integrable (fun (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4) => ↑((initial ρ lam ε κm).residualIntegrand ρ ε z w ((initial ρ lam ε κm).reconstruct vr))) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * (initial ρ lam ε κm).remainingOrder) * ∫ (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4), ↑((initial ρ lam ε κm).residualIntegrand ρ ε z w ((initial ρ lam ε κm).reconstruct vr)) * (↑(lamEps lam ε) ^ (2 * (initial ρ lam ε κp).remainingOrder) * ∫ (vl : (initial ρ lam ε κp).SurvivingCoordinate → T4), ↑((initial ρ lam ε κp).residualIntegrand ρ ε x y ((initial ρ lam ε κp).reconstruct vl)) * ↑(r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct (initial ρ lam ε κp) (initial ρ lam ε κm) (vl, vr))) ∂MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure) ∂MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure) = ∫ (v : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π → T4), (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).initialNestedResidualSumPhysicalCore π x y z w v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

Existing root and terminal integrability closes every analytic premise of the grouped certified two-half collapse at fixed good endpoint pairs.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_initialRootProduct_eq_initialNested_of_sections {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hleftSection : MeasureTheory.Integrable (fun (vl : (initial ρ lam ε κp).SurvivingCoordinate → T4) => ↑((initial ρ lam ε κp).residualIntegrand ρ ε x y ((initial ρ lam ε κp).reconstruct vl))) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure)) (hrightSection : MeasureTheory.Integrable (fun (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4) => ↑((initial ρ lam ε κm).residualIntegrand ρ ε z w ((initial ρ lam ε κm).reconstruct vr))) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure)) : ↑(lamEps lam ε) ^ (2 * ((initial ρ lam ε κp).remainingOrder + (initial ρ lam ε κm).remainingOrder)) * ∫ (p : ((initial ρ lam ε κp).SurvivingCoordinate → T4) × ((initial ρ lam ε κm).SurvivingCoordinate → T4)), ↑((initial ρ lam ε κp).residualIntegrand ρ ε x y ((initial ρ lam ε κp).reconstruct p.1)) * (↑((initial ρ lam ε κm).residualIntegrand ρ ε z w ((initial ρ lam ε κm).reconstruct p.2)) * ↑(r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct (initial ρ lam ε κp) (initial ρ lam ε κm) p))) ∂(MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure) = ∫ (v : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π → T4), (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).initialNestedResidualSumPhysicalCore π x y z w v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

Product-measure form of the preceding theorem, matching the exact two-half root emitted by momentRefinedDeterministicTermSum_eq_initialTwoHalfRoot.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.eventually_twoHalf_lamEps_pow_integral_initialRootResidualSum_eq_initialNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (hε : 0 < ε) (hε1 : ε ≤ 1) : ∀ᵐ (xy : T4 × T4) (zw : T4 × T4) ∂paperMeasure.prod paperMeasure, (↑(lamEps lam ε) ^ (2 * (initial ρ lam ε κm).remainingOrder) * ∫ (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4), ↑((initial ρ lam ε κm).residualIntegrand ρ ε zw.1 zw.2 ((initial ρ lam ε κm).reconstruct vr)) * (↑(lamEps lam ε) ^ (2 * (initial ρ lam ε κp).remainingOrder) * ∫ (vl : (initial ρ lam ε κp).SurvivingCoordinate → T4), ↑((initial ρ lam ε κp).residualIntegrand ρ ε xy.1 xy.2 ((initial ρ lam ε κp).reconstruct vl)) * ↑(r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct (initial ρ lam ε κp) (initial ρ lam ε κm) (vl, vr))) ∂MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure) ∂MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure) = ∫ (v : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π → T4), (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).initialNestedResidualSumPhysicalCore π xy.1 xy.2 zw.1 zw.2 v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

The preceding exact signed collapse holds at almost every pair of endpoint pairs, with both section premises supplied by the proved all-Green root integrability theorem.