Exact bridge from the two within-half terminal carriers to the nested cross carrier

After the left and right canonical within-half suffixes have both been processed, their surviving coordinates are precisely the two copies of finalActive. Paper §4.2 Step 3 starts from the union of those two copies. This file proves that identification as an actual coordinate equivalence and lifts it to a measure-preserving reindexing of product Haar measure.

The physical core below uses the genuine terminal within-half residual integrands and the genuine marker-preserving covariance product. Thus the integral bridge does not pass through a separately postulated, target-shaped density.

theorem Anderson4D.R324WithinHalfResidualPrefix.active_eq_finalActive_of_processed_eq_schedule {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) : res.state.active = finalActive pairing

A completed within-half prefix has exactly the paper's terminal active carrier.

theorem Anderson4D.R324NestedCrossResidualPrefix.initial_activeCarrier_eq_momentResidualActive {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (initial κp κm π).activeCarrier = momentResidualActive κp κm

The initial nested schedule carries exactly all variables left by the two within-half reductions.

Completed two-half data

structure Anderson4D.R324TwoHalfTerminalData (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) : Type

The proof-relevant endpoint of both literal within-half schedules.

• left : R324WithinHalfResidualPrefix ρ lam ε κp
• right : R324WithinHalfResidualPrefix ρ lam ε κm
• left_remaining : self.left.remaining = []
• right_remaining : self.right.remaining = []
• left_processed : self.left.state.processed = r322AnalyticSchedule κp
• right_processed : self.right.state.processed = r322AnalyticSchedule κm

@[reducible, inline]

abbrev Anderson4D.R324TwoHalfTerminalData.NestedCoordinate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (_terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : Type

Coordinates of the literal initial nested cross prefix.

Equations

• _terminal.NestedCoordinate π = ↥(Anderson4D.R324NestedCrossResidualPrefix.initial κp κm π).activeCarrier

@[implicit_reducible]

noncomputable instance Anderson4D.R324TwoHalfTerminalData.nestedCoordinateFintype {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : Fintype (terminal.NestedCoordinate π)

Equations

• terminal.nestedCoordinateFintype π = inferInstance

def Anderson4D.R324TwoHalfTerminalData.survivingSumToNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : terminal.left.SurvivingCoordinate ⊕ terminal.right.SurvivingCoordinate → terminal.NestedCoordinate π

The two terminal within-half carriers, with their ambient labels preserved, map canonically into the initial nested cross carrier.

Equations

• terminal.survivingSumToNested π (Sum.inl i) = ⟨Anderson4D.leftMomentIndex ↑i, ⋯⟩
• terminal.survivingSumToNested π (Sum.inr j) = ⟨Anderson4D.rightMomentIndex ↑j, ⋯⟩

noncomputable def Anderson4D.R324TwoHalfTerminalData.survivingSumEquivNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : terminal.left.SurvivingCoordinate ⊕ terminal.right.SurvivingCoordinate ≃ terminal.NestedCoordinate π

The two terminal within-half carriers, with their ambient labels preserved, are exactly the initial nested cross carrier.

Equations

• terminal.survivingSumEquivNested π = Equiv.ofBijective (terminal.survivingSumToNested π) ⋯

noncomputable def Anderson4D.R324TwoHalfTerminalData.terminalProductPiMeasurableEquivNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4) ≃ᵐ (terminal.NestedCoordinate π → T4)

Product terminal coordinates reindexed as the literal initial nested coordinate tuple.

Equations

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

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.terminalProductPiMeasurableEquivNested_apply_left {ρ : 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) (i : terminal.left.SurvivingCoordinate) : (terminal.terminalProductPiMeasurableEquivNested π) (vl, vr) ((terminal.survivingSumEquivNested π) (Sum.inl i)) = vl i

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.terminalProductPiMeasurableEquivNested_apply_right {ρ : 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) (j : terminal.right.SurvivingCoordinate) : (terminal.terminalProductPiMeasurableEquivNested π) (vl, vr) ((terminal.survivingSumEquivNested π) (Sum.inr j)) = vr j

theorem Anderson4D.R324TwoHalfTerminalData.measurePreserving_terminalProductPiMeasurableEquivNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : MeasureTheory.MeasurePreserving (⇑(terminal.terminalProductPiMeasurableEquivNested π)) ((MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure)) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)

The exact product-Haar measure is preserved by the two-half to nested coordinate reindexing.

Genuine terminal and nested physical cores

noncomputable def Anderson4D.R324TwoHalfTerminalData.terminalDoubledReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : Fin (2 * m) → T4

Assemble the two genuine terminal within-half reconstructions into the doubled ambient carrier. This definition is independent of the nested schedule.

Equations

• terminal.terminalDoubledReconstruct p k = match (Anderson4D.momentDoubleFinEquiv m).symm k with | Sum.inl i => terminal.left.reconstruct p.1 i | Sum.inr j => terminal.right.reconstruct p.2 j

noncomputable def Anderson4D.R324TwoHalfTerminalData.nestedReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (v : terminal.NestedCoordinate π → T4) : Fin (2 * m) → T4

Reconstruct the doubled ambient tuple from the literal initial nested carrier, setting only genuinely absent coordinates to zero.

Equations

• terminal.nestedReconstruct π v k = if hk : k ∈ (Anderson4D.R324NestedCrossResidualPrefix.initial κp κm π).activeCarrier then v ⟨k, hk⟩ else 0

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.nestedReconstruct_surviving {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (v : terminal.NestedCoordinate π → T4) (i : terminal.NestedCoordinate π) : terminal.nestedReconstruct π v ↑i = v i

theorem Anderson4D.R324TwoHalfTerminalData.terminalDoubledReconstruct_eq_nestedReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : terminal.terminalDoubledReconstruct p = terminal.nestedReconstruct π ((terminal.terminalProductPiMeasurableEquivNested π) p)

The abstract measure reindexing reconstructs exactly the same ambient doubled tuple as the two concrete terminal within-half reconstructions.

theorem Anderson4D.R324TwoHalfTerminalData.left_residualIntegrand_eq_chain {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (x y : T4) (v : Fin m → T4) : terminal.left.residualIntegrand ρ ε x y v = terminal.left.residualChainProduct x y v

At an actually completed suffix, no unprocessed difference or primitive factor remains hidden in the within-half residual integrand.

theorem Anderson4D.R324TwoHalfTerminalData.right_residualIntegrand_eq_chain {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (z w : T4) (v : Fin m → T4) : terminal.right.residualIntegrand ρ ε z w v = terminal.right.residualChainProduct z w v

Right-copy counterpart of left_residualIntegrand_eq_chain.

noncomputable def Anderson4D.R324TwoHalfTerminalData.terminalMarkedPhysicalCore {ρ : 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) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ℂ

Genuine post-phase-A physical fibre on the product of the two completed within-half carriers. The projected marker remains inside the complete physical covariance product.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedMarkedPhysicalCore {ρ : 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) (v : terminal.NestedCoordinate π → T4) : ℂ

The same genuine physical fibre, now expressed on the literal initial nested carrier. This is a lossless coordinate transport of terminalMarkedPhysicalCore, not an independently postulated model integrand.

Equations

• terminal.initialNestedMarkedPhysicalCore π selected L x y z w v = terminal.terminalMarkedPhysicalCore π selected L x y z w ((terminal.terminalProductPiMeasurableEquivNested π).symm v)

theorem Anderson4D.R324TwoHalfTerminalData.markedCovariance_terminal_eq_nested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (momentResidualActive κp κm) (terminal.terminalDoubledReconstruct p) = ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (momentResidualActive κp κm) (terminal.nestedReconstruct π ((terminal.terminalProductPiMeasurableEquivNested π) p))

In particular, the genuine marker-preserving covariance product is unchanged by the terminal-to-nested coordinate bridge.

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedMarkedPhysicalCore_reindex {ρ : 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) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : terminal.initialNestedMarkedPhysicalCore π selected L x y z w ((terminal.terminalProductPiMeasurableEquivNested π) p) = terminal.terminalMarkedPhysicalCore π selected L x y z w p

Pointwise losslessness of the physical terminal-to-nested transport.

theorem Anderson4D.R324TwoHalfTerminalData.integral_terminalMarkedPhysicalCore_eq_initialNested {ρ : 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) : ∫ (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) = ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

Exact two-half-to-nested Fubini bridge.

The integral of the actual completed two-half physical fibre is exactly the integral of that same fibre on R324NestedCrossResidualPrefix.initial. No norm, estimate, or enlarged density is introduced.

Weighted within-half transition

The scalar residual-value iteration from the earlier module is insufficient under a cross covariance, because that covariance depends on the coordinates which survive the current half. The following theorem is the required outer-functional strengthening: the outer function may depend arbitrarily on every post-head coordinate, but is fixed during the current local block integral.

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_residual_mul_postOuter_eq_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (outer : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * outer ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hstandard : ∀ (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4), MeasureTheory.Integrable ((res.headContext head tail hremaining).localIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2)) => paperMeasure)) (hinternal : ∀ (_v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4), ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * outer ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2 ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * (res.afterHead head tail hremaining).remainingOrder) * ∫ (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4), ↑((res.afterHead head tail hremaining).residualIntegrand ρ ε x y ((res.afterHead head tail hremaining).reconstruct v)) * outer v ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure

One exact head transition with a genuinely coordinate-dependent complex outer factor. Its pullback to the pre-head carrier is the second component of the proved measure-preserving head/post split.

inductive Anderson4D.R324WithinHalfWeightedTrace {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (x y : T4) : R324WithinHalfResidualPrefix ρ lam ε pairing → Type

A data-valued version of the exact within-half ready trace.

The earlier trace intentionally lives in Prop, so Lean correctly forbids eliminating it to obtain the terminal coordinate type. This Type-valued trace stores the same genuine step certificates and can therefore carry a coordinate-dependent outer function all the way to its actual terminal carrier.

• terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) : R324WithinHalfWeightedTrace x y res
• step {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ready : res.R324WithinHalfResidualStepReady head tail hremaining x y) (next : R324WithinHalfWeightedTrace x y (res.afterHead head tail hremaining)) : R324WithinHalfWeightedTrace x y res

def Anderson4D.R324WithinHalfWeightedTrace.terminalPrefix {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (trace : R324WithinHalfWeightedTrace x y res) : R324WithinHalfResidualPrefix ρ lam ε pairing

The literal terminal prefix reached by a data-valued trace.

Equations

• (Anderson4D.R324WithinHalfWeightedTrace.terminal res hremaining).terminalPrefix = res
• (Anderson4D.R324WithinHalfWeightedTrace.step res head tail hremaining ready next).terminalPrefix = next.terminalPrefix

def Anderson4D.R324WithinHalfWeightedTrace.terminalProjection {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (trace : R324WithinHalfWeightedTrace x y res) : (res.SurvivingCoordinate → T4) → trace.terminalPrefix.SurvivingCoordinate → T4

Restrict a current surviving tuple through every proved head/post split until it becomes a tuple on the actual terminal carrier.

Equations

• One or more equations did not get rendered due to their size.
• (Anderson4D.R324WithinHalfWeightedTrace.terminal res hremaining).terminalProjection = fun (v : res.SurvivingCoordinate → Anderson4D.T4) => v

def Anderson4D.R324WithinHalfWeightedTrace.WeightedIntegrableAlong {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (trace : R324WithinHalfWeightedTrace x y res) (outer : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) : Prop

Weighted integrability required exactly at the nonterminal nodes.

Equations

• One or more equations did not get rendered due to their size.
• (Anderson4D.R324WithinHalfWeightedTrace.terminal res hremaining).WeightedIntegrableAlong outer_2 = True

theorem Anderson4D.R324WithinHalfWeightedTrace.terminalPrefix_remaining_eq_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (trace : R324WithinHalfWeightedTrace x y res) : trace.terminalPrefix.remaining = []

The terminal prefix has an empty suffix.

theorem Anderson4D.R324WithinHalfWeightedTrace.terminalPrefix_processed_eq_schedule {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (trace : R324WithinHalfWeightedTrace x y res) : trace.terminalPrefix.state.processed = r322AnalyticSchedule pairing

The terminal prefix has processed the complete analytic schedule.

theorem Anderson4D.R324WithinHalfWeightedTrace.lamEps_pow_integral_mul_terminalOuter_eq_terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (trace : R324WithinHalfWeightedTrace x y res) (outer : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) (hweighted : trace.WeightedIntegrableAlong outer) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (v : res.SurvivingCoordinate → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct v)) * outer (trace.terminalProjection v) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (v : trace.terminalPrefix.SurvivingCoordinate → T4), ↑(trace.terminalPrefix.residualIntegrand ρ ε x y (trace.terminalPrefix.reconstruct v)) * outer v ∂MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure

Exact weighted iteration through the full literal suffix.

@[irreducible]

def Anderson4D.R324WithinHalfWeightedTrace.of_provider {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (x y : T4) (provider : R324WithinHalfResidualPrefix.R324WithinHalfResidualStepProvider x y) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : R324WithinHalfWeightedTrace x y res

A uniform genuine step provider constructs the data-valued trace needed for coordinate-dependent outer factors.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.ofTraces {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {x y z w : T4} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} (leftTrace : R324WithinHalfWeightedTrace x y leftRes) (rightTrace : R324WithinHalfWeightedTrace z w rightRes) : R324TwoHalfTerminalData ρ lam ε κp κm

Package the actual terminal prefixes of two data-valued within-half traces for the carrier/Fubini bridge above.

Equations

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

noncomputable def Anderson4D.R324WithinHalfWeightedTrace.terminalMarkedCrossFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {x y z w : T4} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} (leftTrace : R324WithinHalfWeightedTrace x y leftRes) (rightTrace : R324WithinHalfWeightedTrace z w rightRes) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4) (vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4) : ℂ

The genuine marked cross covariance, evaluated on the two actual terminal projections of a pair of weighted traces.

Equations

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

theorem Anderson4D.R324WithinHalfWeightedTrace.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} (leftTrace : R324WithinHalfWeightedTrace x y leftRes) (rightTrace : R324WithinHalfWeightedTrace z w rightRes) (cross : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) → (rightTrace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) (hleft : ∀ (vr : rightRes.SurvivingCoordinate → T4), leftTrace.WeightedIntegrableAlong fun (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4) => cross vl (rightTrace.terminalProjection vr)) (hright : rightTrace.WeightedIntegrableAlong 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 within-half iteration.

The left trace is collapsed with the right terminal projection fixed, then the right trace is collapsed with the completed left integral as its outer factor. The theorem stays in physical space and takes no norm.

theorem Anderson4D.R324WithinHalfWeightedTrace.integral_terminalMarkedPhysicalCore_eq_iterated {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {x y z w : T4} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} (leftTrace : R324WithinHalfWeightedTrace x y leftRes) (rightTrace : R324WithinHalfWeightedTrace z w rightRes) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (hintegrable : MeasureTheory.Integrable ((R324TwoHalfTerminalData.ofTraces 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))) : ∫ (p : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) × (rightTrace.terminalPrefix.SurvivingCoordinate → T4)), (R324TwoHalfTerminalData.ofTraces leftTrace rightTrace).terminalMarkedPhysicalCore π selected L x y z w p ∂(MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : rightTrace.terminalPrefix.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)) * leftTrace.terminalMarkedCrossFactor rightTrace π selected L vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : rightTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure

Fubini identifies the iterated terminal expression with the genuine product-carrier terminalMarkedPhysicalCore.

theorem Anderson4D.R324WithinHalfWeightedTrace.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} (leftTrace : R324WithinHalfWeightedTrace x y leftRes) (rightTrace : R324WithinHalfWeightedTrace z w rightRes) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (hleft : ∀ (vr : rightRes.SurvivingCoordinate → T4), leftTrace.WeightedIntegrableAlong fun (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4) => leftTrace.terminalMarkedCrossFactor rightTrace π selected L vl (rightTrace.terminalProjection vr)) (hright : rightTrace.WeightedIntegrableAlong fun (vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4) => ∫ (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4), ↑(leftTrace.terminalPrefix.residualIntegrand ρ ε x y (leftTrace.terminalPrefix.reconstruct vl)) * leftTrace.terminalMarkedCrossFactor rightTrace π selected L vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure) (hterminal : MeasureTheory.Integrable ((R324TwoHalfTerminalData.ofTraces 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)) * leftTrace.terminalMarkedCrossFactor rightTrace π 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.ofTraces leftTrace rightTrace).NestedCoordinate π → T4), (R324TwoHalfTerminalData.ofTraces leftTrace rightTrace).initialNestedMarkedPhysicalCore π selected L x y z w v ∂MeasureTheory.Measure.pi fun (x : (R324TwoHalfTerminalData.ofTraces leftTrace rightTrace).NestedCoordinate π) => paperMeasure

Full exact bridge: two physical within-half traces to the literal initial nested cross prefix.

Only integrability facts are assumed. The equality itself is derived from the genuine local collapse identities, Fubini, and the proved measure-preserving carrier equivalence.