Certified two-half physical collapse for R-324

This module joins the endpoint-independent certified within-half traces to the genuine two-half-to-nested physical bridge. Full integrability remains attached to the actual weighted scalar integrals traversed by a trace; no pointwise unweighted local-section premise is introduced.

noncomputable def Anderson4D.R324TwoHalfTerminalData.ofCertifiedTraces {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightScale) : R324TwoHalfTerminalData ρ lam ε κp κm

Package the actual terminal prefixes of two endpoint-independent certified traces.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.markedCrossFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (vl : terminal.left.SurvivingCoordinate → T4) (vr : terminal.right.SurvivingCoordinate → T4) : ℂ

The genuine marked cross covariance on an arbitrary completed two-half terminal datum.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.integral_terminalMarkedPhysicalCore_eq_iterated {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (x y z w : T4) (hintegrable : MeasureTheory.Integrable (terminal.terminalMarkedPhysicalCore π selected L x y z w) ((MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure))) : ∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), terminal.terminalMarkedPhysicalCore π selected L x y z w p ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure) = ∫ (vr : terminal.right.SurvivingCoordinate → T4), ↑(terminal.right.residualIntegrand ρ ε z w (terminal.right.reconstruct vr)) * ∫ (vl : terminal.left.SurvivingCoordinate → T4), ↑(terminal.left.residualIntegrand ρ ε x y (terminal.left.reconstruct vl)) * terminal.markedCrossFactor π selected L vl vr ∂MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure

Fubini identifies the terminal product-space physical core with its right-then-left iterated integral.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_eq_terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {x y z w : T4} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightScale) (cross : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) → (rightTrace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) (hleft : ∀ᵐ (vr : rightRes.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure, WeightedIntegrableAlong x y leftTrace fun (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4) => cross vl (rightTrace.terminalProjection vr)) (hright : WeightedIntegrableAlong z w rightTrace fun (vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4) => ∫ (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4), ↑(leftTrace.terminalPrefix.residualIntegrand ρ ε x y (leftTrace.terminalPrefix.reconstruct vl)) * cross vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure) : (↑(lamEps lam ε) ^ (2 * rightRes.remainingOrder) * ∫ (vr : rightRes.SurvivingCoordinate → T4), ↑(rightRes.residualIntegrand ρ ε z w (rightRes.reconstruct vr)) * (↑(lamEps lam ε) ^ (2 * leftRes.remainingOrder) * ∫ (vl : leftRes.SurvivingCoordinate → T4), ↑(leftRes.residualIntegrand ρ ε x y (leftRes.reconstruct vl)) * cross (leftTrace.terminalProjection vl) (rightTrace.terminalProjection vr) ∂MeasureTheory.Measure.pi fun (x : leftRes.SurvivingCoordinate) => paperMeasure) ∂MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure) = ∫ (vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4), ↑(rightTrace.terminalPrefix.residualIntegrand ρ ε z w (rightTrace.terminalPrefix.reconstruct vr)) * ∫ (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4), ↑(leftTrace.terminalPrefix.residualIntegrand ρ ε x y (leftTrace.terminalPrefix.reconstruct vl)) * cross vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : rightTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure

Exact two-sided weighted iteration through endpoint-independent certified traces, for an arbitrary terminal cross factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_eq_initialNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {x y z w : T4} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (hleft : ∀ᵐ (vr : rightRes.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure, WeightedIntegrableAlong x y leftTrace fun (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4) => (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).markedCrossFactor π selected L vl (rightTrace.terminalProjection vr)) (hright : WeightedIntegrableAlong z w rightTrace fun (vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4) => ∫ (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4), ↑(leftTrace.terminalPrefix.residualIntegrand ρ ε x y (leftTrace.terminalPrefix.reconstruct vl)) * (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).markedCrossFactor π selected L vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure) (hterminal : MeasureTheory.Integrable ((R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).terminalMarkedPhysicalCore π selected L 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 * rightRes.remainingOrder) * ∫ (vr : rightRes.SurvivingCoordinate → T4), ↑(rightRes.residualIntegrand ρ ε z w (rightRes.reconstruct vr)) * (↑(lamEps lam ε) ^ (2 * leftRes.remainingOrder) * ∫ (vl : leftRes.SurvivingCoordinate → T4), ↑(leftRes.residualIntegrand ρ ε x y (leftRes.reconstruct vl)) * (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).markedCrossFactor π selected L (leftTrace.terminalProjection vl) (rightTrace.terminalProjection vr) ∂MeasureTheory.Measure.pi fun (x : leftRes.SurvivingCoordinate) => paperMeasure) ∂MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure) = ∫ (v : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π → T4), (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).initialNestedMarkedPhysicalCore π selected L x y z w v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

Exact certified two-half physical collapse.

The genuine within-half physical residuals are collapsed on both sides, then Fubini and the proved terminal-to-nested carrier equivalence transport the same physical integrand to the literal initial nested cross prefix.