Certified nonempty-root endpoint bridge for R-324

This module carries one residual-refined physical fibre through the two certified within-half traces and then through the exact four-endpoint Fubini identity. Every equality remains signed. In particular, the complete residual primitive sum is kept grouped and no norm or pointwise majorization is introduced.

The analytic premises retained below are the almost-everywhere root section integrability, the joint root-product integrability, and the terminal-product integrability genuinely consumed by the certified traces.

Initial doubled-coordinate reindexing

noncomputable def Anderson4D.r324InitialTwoHalfProductPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) : ((R324WithinHalfResidualPrefix.initial ρ lam ε κp).SurvivingCoordinate → T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε κm).SurvivingCoordinate → T4) ≃ᵐ (Fin (2 * m) → T4)

Reindex the two literal initial sparse half carriers as the ambient Fin (2m) tuple used by a residual-refined physical fibre.

Equations

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

theorem Anderson4D.measurePreserving_r324InitialTwoHalfProductPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) : MeasureTheory.MeasurePreserving (⇑(r324InitialTwoHalfProductPiMeasurableEquiv ρ lam ε κp κm)) ((MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure)) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

The initial two-half reindexing preserves the exact product Haar measure.

@[simp]

theorem Anderson4D.r324InitialTwoHalfProductPiMeasurableEquiv_apply (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (p : ((R324WithinHalfResidualPrefix.initial ρ lam ε κp).SurvivingCoordinate → T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε κm).SurvivingCoordinate → T4)) : (r324InitialTwoHalfProductPiMeasurableEquiv ρ lam ε κp κm) p = r324TwoHalfRootDoubledReconstruct (R324WithinHalfResidualPrefix.initial ρ lam ε κp) (R324WithinHalfResidualPrefix.initial ρ lam ε κm) p

The preceding measurable equivalence is pointwise the doubled reconstruction already consumed by the certified two-half collapse.

Exact refined-root coordinate bridge

theorem Anderson4D.integral_ambient_eq_initialTwoHalfProduct (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (F : (Fin (2 * m) → T4) → ℂ) : (∫ (v : Fin (2 * m) → T4), F v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ∫ (p : ((R324WithinHalfResidualPrefix.initial ρ lam ε κp).SurvivingCoordinate → T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε κm).SurvivingCoordinate → T4)), F (r324TwoHalfRootDoubledReconstruct (R324WithinHalfResidualPrefix.initial ρ lam ε κp) (R324WithinHalfResidualPrefix.initial ρ lam ε κm) p) ∂(MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure)

Integral transport from the ambient doubled tuple to the two initial sparse half carriers. No integrability premise is needed for this measure-preserving identity.

theorem Anderson4D.integral_momentRefinedPhysicalIntegrand_eq_initialTwoHalfRoot (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (x y z w : T4) : (∫ (v : Fin (2 * m) → T4), momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ∫ (p : ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).SurvivingCoordinate → T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).SurvivingCoordinate → T4)), momentFourierPhase α β x y z w * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).residualIntegrand ρ ε x y ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).reconstruct p.1)) * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).residualIntegrand ρ ε z w ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).reconstruct p.2)) * ↑(r324ResidualPrimitiveSumProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd (r324TwoHalfRootDoubledReconstruct (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst) (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst) p)) ∂(MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).SurvivingCoordinate) => paperMeasure)

At fixed external endpoints, one residual-refined root is exactly the product of its two initial certified residual carriers and the still-grouped cross-cut primitive sum.

theorem Anderson4D.r324RefinedPhysicalIntegral_eq_initialTwoHalfRoot (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hr : r ∈ momentResidualChainSignaturesAt m s) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) : r324RefinedPhysicalIntegral ρ ε m α β ⟨⟨s, hs⟩, ⟨r, hr⟩⟩ = ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (p : ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).SurvivingCoordinate → T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).SurvivingCoordinate → T4)), momentFourierPhase α β x y z w * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).residualIntegrand ρ ε x y ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).reconstruct p.1)) * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).residualIntegrand ρ ε z w ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).reconstruct p.2)) * ↑(r324ResidualPrimitiveSumProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd (r324TwoHalfRootDoubledReconstruct (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst) (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst) p)) ∂(MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).SurvivingCoordinate) => paperMeasure) ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

Fivefold form of the preceding bridge for the genuine signed r324RefinedPhysicalIntegral. Joint integrability is discharged by the already proved refined-fibre integrability theorem before any iterated integral is introduced.

theorem Anderson4D.momentRefinedDeterministicTermSum_eq_initialTwoHalfRoot (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hr : r ∈ momentResidualChainSignaturesAt m s) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) : momentRefinedDeterministicTermSum ρ ε m α β s r = ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (p : ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).SurvivingCoordinate → T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).SurvivingCoordinate → T4)), momentFourierPhase α β x y z w * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).residualIntegrand ρ ε x y ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).reconstruct p.1)) * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).residualIntegrand ρ ε z w ((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).reconstruct p.2)) * ↑(r324ResidualPrimitiveSumProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd (r324TwoHalfRootDoubledReconstruct (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst) (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst) p)) ∂(MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).SurvivingCoordinate) => paperMeasure) ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

The same exact fivefold root bridge with the scalar momentRefinedDeterministicTermSum used by the corrected R-324 output.

Certified collapse of the two initial roots

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_initialRootResidualSum_eq_initialNested_of_root {ρ : 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) (hleftRoot : ∀ᵐ (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable (fun (vl : (initial ρ lam ε κp).SurvivingCoordinate → T4) => ↑((initial ρ lam ε κp).residualIntegrand ρ ε x y ((initial ρ lam ε κp).reconstruct vl)) * (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).residualSumCrossFactor π (leftTrace.terminalProjection vl) (rightTrace.terminalProjection vr)) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure)) (hjoint : MeasureTheory.Integrable (fun (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)) * (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).residualSumCrossFactor π (leftTrace.terminalProjection p.1) (rightTrace.terminalProjection p.2))) ((MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κm).SurvivingCoordinate) => paperMeasure))) (hterminal : MeasureTheory.Integrable ((R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).terminalResidualSumPhysicalCore π x y z w) ((MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : rightTrace.terminalPrefix.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

Root section integrability supplies the exact weighted hypotheses for both certified traces, after which the existing signed two-half iteration reaches the initial nested-cross carrier. The endpoint-dependent premises are intentionally explicit: global product-space integrability yields them only almost everywhere.

Endpoint integration after the certified collapse

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_eq_phase_mul_initialNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (α β : Z4) (x y z w : T4) : ∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), terminal.externalModeResidualSumIntegrand π α β p x y z w ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure) = momentFourierPhase α β x y z w * ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedResidualSumPhysicalCore π x y z w v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

At fixed endpoints, the external Fourier phase may be kept outside the lossless terminal-to-nested coordinate transport.

theorem Anderson4D.integral_phase_mul_initialNestedResidualSum_eq_endpointIntegrated_of_storedCertificates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) : let terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace; ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), momentFourierPhase α β x y z w * ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedResidualSumPhysicalCore π x y z w v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

Once the two initial residuals have reached the nested carrier, the stored terminal certificates discharge the global endpoint/internal Fubini premise and evaluate all four endpoint modes.