Exact Phase-A-to-terminal order ledger for R-324

This module records the missing numeric bridge between the three literal primitive schedules used in the physical construction and the unified primitive-block partition. The bridge is derived from the actual schedule permutations, the two doubled-coordinate embeddings, and the residual inside-to-outside schedule. It does not assume an order decomposition.

The resulting equality splits the ambient perturbative order into the left within-half suffix, the right within-half suffix, the consumed nested-cross prefix, and the terminal marked/suffix payload. The final section also records the structural data that survive at that payload and the exact identification of the corrected refined-fibre sum with its physical integral. No analytic estimate or target-shaped final bound is introduced here.

The two Phase-A schedules inside the doubled carrier

@[simp]

theorem Anderson4D.residualBlockOrder_image_leftMomentIndex {m : ℕ} (B : Finset (Fin m)) : residualBlockOrder (Finset.image leftMomentIndex B) = residualBlockOrder B

@[simp]

theorem Anderson4D.residualBlockOrder_image_rightMomentIndex {m : ℕ} (B : Finset (Fin m)) : residualBlockOrder (Finset.image rightMomentIndex B) = residualBlockOrder B

theorem Anderson4D.r324LeftWithinHalfInitial_remainingOrder_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp : PartialPairing (Fin m)) : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder = (List.map residualBlockOrder (momentLeftExtractionBlocks κp)).sum

The literal left within-half initial suffix has the same exact order as the left-copy block family in the unified doubled schedule.

theorem Anderson4D.r324RightWithinHalfInitial_remainingOrder_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κm : PartialPairing (Fin m)) : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder = (List.map residualBlockOrder (momentRightExtractionBlocks κm)).sum

The literal right within-half initial suffix has the same exact order as the right-copy block family in the unified doubled schedule.

theorem Anderson4D.r324NestedCrossInitial_remainingOrder_eq {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder = (List.map residualBlockOrder (nonemptyMomentResidualCollapseBlocks κp κm π)).sum

The literal initial nested-cross suffix has the exact order of the nonempty residual block family in the unified doubled schedule.

Ambient order conservation

theorem Anderson4D.r324InitialSchedules_remainingOrders_eq_ambient (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder + (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder + (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder = m

The two actual Phase-A initial suffixes and the actual initial nested-cross suffix partition the full ambient perturbative order.

This is a derived schedule theorem: its proof passes through the unified nonempty primitive-block ledger and does not take the desired equality as an input.

theorem Anderson4D.R324InitialNestedContextFactorization.left_add_right_add_prefix_add_terminal_eq_ambient {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {terminal : R324TwoHalfTerminalData ρ lam ε κp κm} {L : ℝ} {x y z w : T4} (factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w) : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder + (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder + factorization.prefixOrder + factorization.terminalOrder = m

Replacing the initial cross order by the actual proper-prefix and terminal orders gives a genuine four-part partition of ambient order.

theorem Anderson4D.R324InitialNestedContextFactorization.pow_ambient_eq_four_part {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {terminal : R324TwoHalfTerminalData ρ lam ε κp κm} {L : ℝ} {x y z w : T4} (factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w) {A : Type u_1} [Monoid A] (a : A) : a ^ (2 * m) = a ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder) * (a ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder) * (a ^ (2 * factorization.prefixOrder) * a ^ (2 * factorization.terminalOrder)))

The exact four-part multiplicative ledger, valid in every monoid.

theorem Anderson4D.R324InitialNestedContextFactorization.lamEps_pow_ambient_eq_four_part {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {terminal : R324TwoHalfTerminalData ρ lam ε κp κm} {L : ℝ} {x y z w : T4} (factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w) : lamEps lam ε ^ (2 * m) = lamEps lam ε ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder) * (lamEps lam ε ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder) * (lamEps lam ε ^ (2 * factorization.prefixOrder) * lamEps lam ε ^ (2 * factorization.terminalOrder)))

Real coupling-power specialization of the exact four-part ledger.

theorem Anderson4D.R324InitialNestedContextFactorization.complex_lamEps_pow_ambient_eq_four_part {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {terminal : R324TwoHalfTerminalData ρ lam ε κp κm} {L : ℝ} {x y z w : T4} (factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w) : ↑(lamEps lam ε) ^ (2 * m) = ↑(lamEps lam ε) ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder) * (↑(lamEps lam ε) ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder) * (↑(lamEps lam ε) ^ (2 * factorization.prefixOrder) * ↑(lamEps lam ε) ^ (2 * factorization.terminalOrder)))

Complex coupling-power specialization used before taking the physical norm.

theorem Anderson4D.R324InitialNestedContextFactorization.abs_lamEps_pow_ambient_eq_four_part {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {terminal : R324TwoHalfTerminalData ρ lam ε κp κm} {L : ℝ} {x y z w : T4} (factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w) : |lamEps lam ε| ^ (2 * m) = |lamEps lam ε| ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder) * (|lamEps lam ε| ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder) * (|lamEps lam ε| ^ (2 * factorization.prefixOrder) * |lamEps lam ε| ^ (2 * factorization.terminalOrder)))

Absolute-value specialization matching the corrected integrated reduction boundary.

Structural data retained at the terminal payload

def Anderson4D.r324RecoveredEndpointFlags {m : ℕ} (κp κm : PartialPairing (Fin m)) : R324EndpointFlags

The four endpoint cases recoverable from the indexed left/right partial pairings at every terminal nested-cross payload.

Equations

• Anderson4D.r324RecoveredEndpointFlags κp κm = ![false, Anderson4D.r324OutgoingIsShortcut κp, false, Anderson4D.r324OutgoingIsShortcut κm]

@[simp]

theorem Anderson4D.r324RecoveredEndpointFlags_zero {m : ℕ} (κp κm : PartialPairing (Fin m)) : r324RecoveredEndpointFlags κp κm 0 = false

@[simp]

theorem Anderson4D.r324RecoveredEndpointFlags_one {m : ℕ} (κp κm : PartialPairing (Fin m)) : r324RecoveredEndpointFlags κp κm 1 = r324OutgoingIsShortcut κp

@[simp]

theorem Anderson4D.r324RecoveredEndpointFlags_two {m : ℕ} (κp κm : PartialPairing (Fin m)) : r324RecoveredEndpointFlags κp κm 2 = false

@[simp]

theorem Anderson4D.r324RecoveredEndpointFlags_three {m : ℕ} (κp κm : PartialPairing (Fin m)) : r324RecoveredEndpointFlags κp κm 3 = r324OutgoingIsShortcut κm

@[simp]

theorem Anderson4D.r324RecoveredEndpointFlags_eq_contraction {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : r324RecoveredEndpointFlags κp κm = r324ContractionEndpointFlags ⟨κp, ⟨κm, π⟩⟩

The recovered cases are definitionally the cases attached to the corresponding complete contraction.

def Anderson4D.R324NestedCrossTerminalPayload.recoveredEndpointFlags {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {lam ε : ℝ} {step : R324NestedCrossStepContext κp κm π} (_payload : R324NestedCrossTerminalPayload lam ε step) : R324EndpointFlags

The payload's indexed pairing data recover all four endpoint cases; the payload need not duplicate them as mutable fields.

Equations

• _payload.recoveredEndpointFlags = Anderson4D.r324RecoveredEndpointFlags κp κm

@[simp]

theorem Anderson4D.R324NestedCrossTerminalPayload.recoveredEndpointFlags_eq_contraction {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {lam ε : ℝ} {step : R324NestedCrossStepContext κp κm π} (payload : R324NestedCrossTerminalPayload lam ε step) : payload.recoveredEndpointFlags = r324ContractionEndpointFlags ⟨κp, ⟨κm, π⟩⟩

structure Anderson4D.R324TerminalPayloadStructuralLedger {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (selected : R324ResidualCovarianceSlot κp) {lam ε : ℝ} (step : R324NestedCrossStepContext κp κm π) (payload : R324NestedCrossTerminalPayload lam ε step) : Prop

Exact structural ledger at the stop of the proper-prefix run.

It records the genuine marked carrier, the literal unprocessed suffix, both endpoints of the selected covariance, the four endpoint cases recovered from the payload indices, and the unchanged four-endpoint context represented by unscaledDensity.

• head_carrier_eq : step.head.carrier = r324MarkedResidualBlock κp κm π selected
• literal_suffix : step.residual.remaining = step.head :: step.tail
• marked_lower_mem : r324ResidualMarkedLowerEndpoint selected ∈ step.head.carrier
• marked_upper_mem : r324ResidualMarkedUpperEndpoint π selected ∈ step.head.carrier
• recovered_flags : payload.recoveredEndpointFlags = r324ContractionEndpointFlags ⟨κp, ⟨κm, π⟩⟩
• unscaledDensity_eq : payload.unscaledDensity = payload.context payload.x payload.y payload.z payload.w

theorem Anderson4D.R324NestedCrossTerminalPayload.structuralLedger_of_stop {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (selected : R324ResidualCovarianceSlot κp) {lam ε : ℝ} {step : R324NestedCrossStepContext κp κm π} (payload : R324NestedCrossTerminalPayload lam ε step) (hstop : step.head.carrier = r324MarkedResidualBlock κp κm π selected) : R324TerminalPayloadStructuralLedger selected step payload

Every actual stop witness returned by the quantitative proper-prefix iteration supplies the complete terminal structural ledger.

Exact corrected-output / physical-integral boundary

theorem Anderson4D.momentRefinedDeterministicTermSum_eq_r324RefinedPhysicalIntegral (ρ : SmoothCutoff) {ε : ℝ} (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) : momentRefinedDeterministicTermSum ρ ε m α β s r = r324RefinedPhysicalIntegral ρ ε m α β ⟨⟨s, hs⟩, ⟨r, hr⟩⟩

The scalar refined-fibre term appearing in MomentRefinedIntegratedReductionData.refined_bound is exactly the corresponding genuine refined physical integral. This is an equality, not an estimate or a replacement reduction hypothesis.