Terminal projection of the exact R-324 residual primitive sum

The within-half certified traces delete only coordinates belonging to the within-half extraction blocks. Consequently the remaining cross-cut primitive sum reads only coordinates which survive both certified traces. This file records that fact before any norm or estimate is taken, and transports the resulting exact physical core to the initial nested-cross carrier.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalCoordinateEmbedding {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) : trace.terminalPrefix.SurvivingCoordinate → res.SurvivingCoordinate

Regard a coordinate surviving the whole certified trace as a coordinate of the prefix at which the trace starts.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalCoordinateEmbedding_val {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (i : trace.terminalPrefix.SurvivingCoordinate) : ↑(trace.terminalCoordinateEmbedding i) = ↑i

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalProjection_apply {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (v : res.SurvivingCoordinate → T4) (i : trace.terminalPrefix.SurvivingCoordinate) : trace.terminalProjection v i = v (trace.terminalCoordinateEmbedding i)

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.reconstruct_terminalProjection {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (v : res.SurvivingCoordinate → T4) (i : trace.terminalPrefix.SurvivingCoordinate) : res.reconstruct v ↑i = trace.terminalPrefix.reconstruct (trace.terminalProjection v) ↑i

Reconstruction at every terminal coordinate is unchanged by the full certified terminal projection.

Coordinate support of the residual primitive sum

theorem Anderson4D.primitivePartitionBlockCovarianceFactor_congr_on {n : ℕ} {κ : PartialPairing (Fin n)} (ρ : SmoothCutoff) (ε : ℝ) (P : PrimitiveBlockPartition κ) (B : PrimitivePartitionBlockIndex P) (σ : ↥(primitiveFullPairings (residualBlockOrder ↑B))) (v w : Fin n → T4) (hvw : ∀ i ∈ ↑B, v i = w i) : primitivePartitionBlockCovarianceFactor ρ ε P B σ v = primitivePartitionBlockCovarianceFactor ρ ε P B σ w

One complete primitive covariance factor reads only coordinates in its ambient primitive block.

theorem Anderson4D.r324PrimitivePartitionBlockSum_congr_on {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (v w : Fin (2 * m) → T4) (hvw : ∀ i ∈ B, v i = w i) : r324PrimitivePartitionBlockSum ρ ε κp κm π B v = r324PrimitivePartitionBlockSum ρ ε κp κm π B w

The complete primitive-pairing sum on a block reads only coordinates in that block.

theorem Anderson4D.r324ResidualPrimitiveSumProduct_congr_on_active {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v w : Fin (2 * m) → T4) (hvw : ∀ i ∈ momentResidualActive κp κm, v i = w i) : r324ResidualPrimitiveSumProduct ρ ε κp κm π v = r324ResidualPrimitiveSumProduct ρ ε κp κm π w

The remaining exact primitive sum depends only on the doubled residual carrier.

Two-half certified terminal projection

noncomputable def Anderson4D.r324TwoHalfRootDoubledReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (leftRes : R324WithinHalfResidualPrefix ρ lam ε κp) (rightRes : R324WithinHalfResidualPrefix ρ lam ε κm) (p : (leftRes.SurvivingCoordinate → T4) × (rightRes.SurvivingCoordinate → T4)) : Fin (2 * m) → T4

Reconstruct a doubled ambient tuple at the starting prefixes of two certified within-half traces.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.r324TwoHalfRootDoubledReconstruct_eq_terminal_on_active {ρ : 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) (p : (leftRes.SurvivingCoordinate → T4) × (rightRes.SurvivingCoordinate → T4)) (k : Fin (2 * m)) (hk : k ∈ momentResidualActive κp κm) : r324TwoHalfRootDoubledReconstruct leftRes rightRes p k = (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).terminalDoubledReconstruct (leftTrace.terminalProjection p.1, rightTrace.terminalProjection p.2) k

On the doubled residual carrier, reconstruction at the roots of two certified traces is exactly reconstruction from their terminal projections.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.r324ResidualPrimitiveSumProduct_eq_terminalProjection {ρ : 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) (π : ↥κp.singles ≃ ↥κm.singles) (p : (leftRes.SurvivingCoordinate → T4) × (rightRes.SurvivingCoordinate → T4)) : r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct leftRes rightRes p) = r324ResidualPrimitiveSumProduct ρ ε κp κm π ((R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).terminalDoubledReconstruct (leftTrace.terminalProjection p.1, rightTrace.terminalProjection p.2))

Exact terminal-projection theorem for the residual primitive sum.

The cross-cut primitive factor at the genuine two-half root reads only the terminal projections of the two certified within-half traces.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.r324ResidualPrimitiveSumProduct_complex_eq_terminalProjection {ρ : 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) (π : ↥κp.singles ≃ ↥κm.singles) (p : (leftRes.SurvivingCoordinate → T4) × (rightRes.SurvivingCoordinate → T4)) : ↑(r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct leftRes rightRes p)) = ↑(r324ResidualPrimitiveSumProduct ρ ε κp κm π ((R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).terminalDoubledReconstruct (leftTrace.terminalProjection p.1, rightTrace.terminalProjection p.2)))

Complex-valued form used directly inside the physical integrals.

Exact terminal and nested residual-sum cores

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

The exact residual primitive sum on the completed two-half carrier.

Equations

• terminal.residualSumCrossFactor π vl vr = ↑(Anderson4D.r324ResidualPrimitiveSumProduct ρ ε κp κm π (terminal.terminalDoubledReconstruct (vl, vr)))

noncomputable def Anderson4D.R324TwoHalfTerminalData.terminalResidualSumPhysicalCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ℂ

The completed two-half physical core with the exact residual primitive sum retained as a signed factor.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedResidualSumPhysicalCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : terminal.NestedCoordinate π → T4) : ℂ

Lossless reindexing of the exact terminal residual-sum core onto the literal initial nested-cross carrier.

Equations

• terminal.initialNestedResidualSumPhysicalCore π x y z w v = terminal.terminalResidualSumPhysicalCore π x y z w ((terminal.terminalProductPiMeasurableEquivNested π).symm v)

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedResidualSumPhysicalCore_reindex {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : terminal.initialNestedResidualSumPhysicalCore π x y z w ((terminal.terminalProductPiMeasurableEquivNested π) p) = terminal.terminalResidualSumPhysicalCore π x y z w p

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

Exact measure-preserving transport of the signed residual-sum core to the initial nested-cross coordinate space.

theorem Anderson4D.R324TwoHalfTerminalData.integral_terminalResidualSumPhysicalCore_eq_iterated {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (hintegrable : MeasureTheory.Integrable (terminal.terminalResidualSumPhysicalCore π 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.terminalResidualSumPhysicalCore π 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.residualSumCrossFactor π vl vr ∂MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure

Fubini identifies the exact terminal product-space core with the right-then-left iterated integral. Integrability is kept as an explicit endpoint-dependent hypothesis.

Certified two-half collapse of the exact residual-sum core

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_residualSum_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) (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).residualSumCrossFactor π 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).residualSumCrossFactor π vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.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 * 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).residualSumCrossFactor π (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).initialNestedResidualSumPhysicalCore π x y z w v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

Exact certified two-half collapse followed by the lossless terminal to initial-nested transport for the signed residual primitive sum.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_lamEps_pow_integral_rootResidualSum_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) (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).residualSumCrossFactor π 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).residualSumCrossFactor π vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.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 * 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)) * ↑(r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct leftRes rightRes (vl, 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).initialNestedResidualSumPhysicalCore π x y z w v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

Root-coordinate form of the exact bridge. Its cross factor is the literal r324ResidualPrimitiveSumProduct occurring before either within-half trace is collapsed; the preceding projection theorem is the only rewrite used to reach the terminal cross factor.