Initial endpoint-grouped majorant to the complete nested run

This file closes the pointwise seam between the grouped majorant obtained after the four external endpoint integrations and the literal initial Steps 2--3 density. It only reindexes the two endpoint-erased terminal half paths and the still-grouped residual primitive sum. No nested-shell iteration is performed here.

theorem Anderson4D.R324TwoHalfTerminalData.initial_leftHalfPullback_eq_terminalActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : r324LeftHalfPullback (R324NestedCrossResidualPrefix.initial κp κm π).activeCarrier = terminal.left.state.active

On the initial nested carrier, the left-half pullback is exactly the completed left terminal carrier. This carrier identity is also used by the endpoint-pattern splice, so it is intentionally public.

theorem Anderson4D.R324TwoHalfTerminalData.initial_rightHalfPullback_eq_terminalActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : r324RightHalfPullback (R324NestedCrossResidualPrefix.initial κp κm π).activeCarrier = terminal.right.state.active

On the initial nested carrier, the right-half pullback is exactly the completed right terminal carrier. This carrier identity is also used by the endpoint-pattern splice, so it is intentionally public.

Public initial-carrier transport package

The three lemmas above are the coordinate calculation used by the complete run. The marked-word run needs exactly the same calculation, with the marked payload left untouched. These wrappers deliberately expose only the resulting equalities; no implementation detail of the initial endpoint majorant is exported.

theorem Anderson4D.R324TwoHalfTerminalData.initialTerminalProduct_left_eq_initialLeftTuple {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (v : terminal.NestedCoordinate π → T4) : ((terminal.terminalProductPiMeasurableEquivNested π).symm v).1 = terminal.leftTupleOfNestedStep (r324InitialNestedCrossStepContext κp κm π head tail hremaining) v

The completed left terminal tuple is the left tuple read by the initial nested step.

theorem Anderson4D.R324TwoHalfTerminalData.initialTerminalProduct_right_eq_initialRightTuple {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (v : terminal.NestedCoordinate π → T4) : ((terminal.terminalProductPiMeasurableEquivNested π).symm v).2 = terminal.rightTupleOfNestedStep (r324InitialNestedCrossStepContext κp κm π head tail hremaining) v

The completed right terminal tuple is the right tuple read by the initial nested step.

theorem Anderson4D.R324TwoHalfTerminalData.initialTerminalDoubledReconstruct_symm_eq_stepReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (v : terminal.NestedCoordinate π → T4) : terminal.terminalDoubledReconstruct ((terminal.terminalProductPiMeasurableEquivNested π).symm v) = (r324InitialNestedCrossStepContext κp κm π head tail hremaining).reconstruct v

Reconstructing the completed terminal pair agrees with reconstructing the initial nested step.

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedEndpointIntegratedGroupedMajorant_mul_coupling_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (π : ↥κp.singles ≃ ↥κm.singles) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (v : terminal.NestedCoordinate π → T4) : let step := r324InitialNestedCrossStepContext κp κm π head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; lamEps lam ε ^ (2 * step.residual.remainingOrder) * terminal.initialNestedEndpointIntegratedGroupedMajorant leftScale rightScale hleft hright π v = ((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * terminal.completeNestedRunDensity step hleftInitial hrightInitial v

theorem Anderson4D.R324TwoHalfTerminalData.ae_coupling_mul_norm_initialNestedEndpointIntegratedResidualDensity_le_completeNestedRun {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (α β : Z4) : let terminal := ofCertifiedTraces leftTrace rightTrace; let step := r324InitialNestedCrossStepContext κp κm π head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (fun (v : terminal.NestedCoordinate π → T4) => lamEps lam ε ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure] fun (v : terminal.NestedCoordinate π → T4) => ((∏ edge ∈ terminal.left.activeEdgeSlots, leftTrace.terminalScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightTrace.terminalScale edge) * invSqKerMass ^ 4 * terminal.completeNestedRunDensity step hleftInitial hrightInitial v

The initial endpoint-integrated grouped bound is exactly the literal initial Steps 2--3 complete-run density, up to the two stored terminal scale products and the four endpoint inverse-square masses. The residual primitive covariance sum remains grouped and the coupling is inserted only after the endpoint norm bound has been established.