Exact suffix iteration for the nested cross blocks in R-324

Paper §4.2 Step 3 successively removes the proper cross-cut primitive blocks from inside to outside until it reaches the block carrying the selected projected covariance. This file keeps the two logically different inputs separate:

• an upstream bridge first takes the honest norm/edge majorants of the post-two-half physical fibre and exposes the resulting proper prefix together with an explicit four-endpoint context;
• the iteration below performs the exact coordinate/Fubini transitions, applies Proposition 4.1 only to unmarked proper heads, and returns the complete marked/endpoint payload to the Step 4 routing machinery.

The elementary critical convolution between two inverse-square connector edges and the inserted majorant is exposed as a local analytic provider. It is not a final R-324 estimate and its constant may depend on the fixed support constant, but is uniform in the schedule, order, scale and endpoints.

Translation of the genuine cross-gap term

noncomputable def Anderson4D.R324NestedCrossStepContext.blockTranslation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (a : T4) : (Fin (2 * ctx.order) → T4) ≃ᵐ (Fin (2 * ctx.order) → T4)

Translation of every standard block coordinate by the same torus point.

Equations

• ctx.blockTranslation a = MeasurableEquiv.piCongrRight fun (x : Fin (2 * ctx.order)) => MeasurableEquiv.addRight a

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.blockTranslation_apply {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (a : T4) (x : Fin (2 * ctx.order) → T4) : (ctx.blockTranslation a) x = fun (i : Fin (2 * ctx.order)) => x i + a

theorem Anderson4D.R324NestedCrossStepContext.measurePreserving_blockTranslation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (a : T4) : MeasureTheory.MeasurePreserving (⇑(ctx.blockTranslation a)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure)

theorem Anderson4D.R324NestedCrossStepContext.primitiveChainProduct_add_const {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (x : Fin (2 * ctx.order) → T4) (a : T4) : (primitiveChainProduct ctx.order ⋯ G fun (i : Fin (2 * ctx.order)) => x i + a) = primitiveChainProduct ctx.order ⋯ G x

theorem Anderson4D.R324NestedCrossStepContext.primitiveCovarianceProduct_add_const {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (x : Fin (2 * ctx.order) → T4) (a : T4) : (primitiveCovarianceProduct ρ ε ctx.order ctx.blockPairing fun (i : Fin (2 * ctx.order)) => x i + a) = primitiveCovarianceProduct ρ ε ctx.order ctx.blockPairing x

theorem Anderson4D.R324NestedCrossStepContext.primitiveIntegrand_add_const {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (x : Fin (2 * ctx.order) → T4) (a : T4) : (primitiveIntegrand ρ ε ctx.order ⋯ G ctx.blockPairing fun (i : Fin (2 * ctx.order)) => x i + a) = primitiveIntegrand ρ ε ctx.order ⋯ G ctx.blockPairing x

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveIntegrand_add_const {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (x : Fin (2 * ctx.order) → T4) (a : T4) : (ctx.crossGapPrimitiveIntegrand ρ ε G fun (i : Fin (2 * ctx.order)) => x i + a) = ctx.crossGapPrimitiveIntegrand ρ ε G x

noncomputable def Anderson4D.R324NestedCrossStepContext.internalTranslation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (a : T4) : (Fin (2 * ctx.order - 2) → T4) ≃ᵐ (Fin (2 * ctx.order - 2) → T4)

Internal coordinates of a primitive block translated simultaneously.

Equations

• ctx.internalTranslation a = MeasurableEquiv.piCongrRight fun (x : Fin (2 * ctx.order - 2)) => MeasurableEquiv.addRight a

theorem Anderson4D.R324NestedCrossStepContext.measurePreserving_internalTranslation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (a : T4) : MeasureTheory.MeasurePreserving (⇑(ctx.internalTranslation a)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveTerm_eq_diff {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (z w : T4) : ctx.crossGapPrimitiveTerm ρ lam ε G z w = ctx.crossGapPrimitiveTerm ρ lam ε G (z - w) 0

The genuine central-gap primitive term depends only on the endpoint difference. This is an exact Haar change of variables, not a law-level or pointwise-majorant replacement.

Canonical normalized density for a literal cross block

noncomputable def Anderson4D.R324NestedCrossStepContext.normalizedInput {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Fin (2 * ctx.order - 1) → T4 → ℝ

The normalized inverse-square input on every internal edge of a literal cross block. Heterogeneous physical edge scales are extracted outside this normalized density and propagated separately below.

Equations

• ctx.normalizedInput x✝ = Anderson4D.invSqKer

noncomputable def Anderson4D.R324NestedCrossStepContext.normalizedHeadDensity {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (t : Fin (2 * ctx.order) → T4) : ℝ

The exact coupled central-gap density on all standard coordinates of one literal block.

Equations

• ctx.normalizedHeadDensity ρ lam ε t = Anderson4D.lamEps lam ε ^ (2 * ctx.order) * ctx.crossGapPrimitiveIntegrand ρ ε ctx.normalizedInput t

Honest norm boundary from the physical two-half bridge

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedMarkedNormDensity {ρ : 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 first real nonnegative density after the endpoint-explicit complex physical bridge. No Green edge or covariance has yet been replaced.

Equations

• terminal.initialNestedMarkedNormDensity π selected L x y z w v = ‖terminal.initialNestedMarkedPhysicalCore π selected L x y z w v‖

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedMarkedNormDensity_nonneg {ρ : 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) : 0 ≤ terminal.initialNestedMarkedNormDensity π selected L x y z w v

theorem Anderson4D.R324TwoHalfTerminalData.integrable_initialNestedMarkedNormDensity {ρ : 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) (hphysical : MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)) : MeasureTheory.Integrable (terminal.initialNestedMarkedNormDensity π selected L x y z w) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)

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

Taking the norm occurs only after the complete endpoint-explicit physical integral.

theorem Anderson4D.R324TwoHalfTerminalData.norm_integral_initialNestedMarkedPhysicalCore_le_of_ae_majorant {ρ : 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) (majorant : (terminal.NestedCoordinate π → T4) → ℝ) (hphysical : MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)) (hmajorant : MeasureTheory.Integrable majorant (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)) (hle : terminal.initialNestedMarkedNormDensity π selected L x y z w ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure] majorant) : ‖∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ ∫ (v : terminal.NestedCoordinate π → T4), majorant v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

Honest consumer for a later a.e. edgewise majorization. The majorization is intentionally a.e. because the inserted distance² × invSqKer factors are totalized to zero on the diagonal.

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedMarkedNormDensity_eq_terminalFactors {ρ : 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) : terminal.initialNestedMarkedNormDensity π selected L x y z w v = |terminal.left.residualIntegrand ρ ε x y (terminal.left.reconstruct ((terminal.terminalProductPiMeasurableEquivNested π).symm v).1)| * |terminal.right.residualIntegrand ρ ε z w (terminal.right.reconstruct ((terminal.terminalProductPiMeasurableEquivNested π).symm v).2)| * ‖ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (momentResidualActive κp κm) (terminal.terminalDoubledReconstruct ((terminal.terminalProductPiMeasurableEquivNested π).symm v))‖

Exact norm ledger before any canonical inverse-square majorization. The four external endpoints remain inside the two terminal chain factors, and the selected projected covariance remains inside the marked physical product.

The canonical nonnegative residual density

def Anderson4D.R324NestedCrossResidualPrefix.headContext {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : res.remaining = head :: tail) : R324NestedCrossStepContext κp κm π

The proof-relevant head context attached to a literal nonempty suffix.

Equations

• res.headContext head tail hremaining = { residual := res, head := head, tail := tail, remaining_eq := hremaining }

structure Anderson4D.R324NestedCrossProperStepContext {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

A nonterminal literal head together with the next outer cross block. The two connector edges of paper Step 3 run from the endpoints of head to the central-gap coordinates of nextHead.

• step : R324NestedCrossStepContext κp κm π
• nextHead : R324NestedCrossBlock κp κm π
• rest : List (R324NestedCrossBlock κp κm π)
• tail_eq : self.step.tail = self.nextHead :: self.rest

def Anderson4D.R324NestedCrossProperStepContext.nextContext {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : R324NestedCrossStepContext κp κm π

The next literal head context after deleting the current head.

Equations

• ctx.nextContext = { residual := ctx.step.next, head := ctx.nextHead, tail := ctx.rest, remaining_eq := ⋯ }

def Anderson4D.R324NestedCrossProperStepContext.nextLeftPostCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : ctx.step.PostCoordinate

The inner-left coordinate of the next outer shell, viewed in the post-head carrier.

Equations

• ctx.nextLeftPostCoordinate = ⟨ctx.nextHead.leftGap, ⋯⟩

def Anderson4D.R324NestedCrossProperStepContext.nextRightPostCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : ctx.step.PostCoordinate

The inner-right coordinate of the next outer shell, viewed in the post-head carrier.

Equations

• ctx.nextRightPostCoordinate = ⟨ctx.nextHead.rightGap, ⋯⟩

noncomputable def Anderson4D.R324NestedCrossProperStepContext.connector {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (t : Fin (2 * ctx.step.order) → T4) (v : ctx.step.PostCoordinate → T4) : ℝ

The two genuine chain edges connecting the current block to the next outer shell.

Equations

• ctx.connector t v = Anderson4D.invSqKer (v ctx.nextLeftPostCoordinate - t ⟨0, ⋯⟩) * Anderson4D.invSqKer (t (Anderson4D.primitiveLast ctx.step.order ⋯) - v ctx.nextRightPostCoordinate)

theorem Anderson4D.R324NestedCrossProperStepContext.connector_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (t : Fin (2 * ctx.step.order) → T4) (v : ctx.step.PostCoordinate → T4) : 0 ≤ ctx.connector t v

theorem Anderson4D.R324NestedCrossProperStepContext.connector_measurable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (post : ctx.step.PostCoordinate → T4) : Measurable fun (t : Fin (2 * ctx.step.order) → T4) => ctx.connector t post

theorem Anderson4D.R324NestedCrossProperStepContext.connector_joint_measurable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Measurable fun (p : (Fin (2 * ctx.step.order) → T4) × (ctx.step.PostCoordinate → T4)) => ctx.connector p.1 p.2

Joint measurability of the two connector edges in head/post coordinates.

noncomputable def Anderson4D.R324NestedCrossProperStepContext.properHeadIntegral {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (left right : T4) : ℝ

The exact endpoint integral produced after the internal coordinates of one proper cross block have been integrated.

Equations

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

theorem Anderson4D.R324NestedCrossProperStepContext.properHeadIntegral_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (left right : T4) : 0 ≤ ctx.properHeadIntegral ρ lam ε left right

theorem Anderson4D.R324NestedCrossProperStepContext.integral_normalizedHeadDensity_mul_connector {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (post : ctx.step.PostCoordinate → T4) (hint : MeasureTheory.Integrable (fun (t : Fin (2 * ctx.step.order) → T4) => ctx.step.normalizedHeadDensity ρ lam ε t * ctx.connector t post) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.step.order)) => paperMeasure)) : (∫ (t : Fin (2 * ctx.step.order) → T4), ctx.step.normalizedHeadDensity ρ lam ε t * ctx.connector t post ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.step.order)) => paperMeasure) = ctx.properHeadIntegral ρ lam ε (post ctx.nextLeftPostCoordinate) (post ctx.nextRightPostCoordinate)

Exact endpoint/internal Fubini identity for one proper block. The right side contains the genuine crossGapPrimitiveTerm; Proposition 4.1 has not yet been applied.

theorem Anderson4D.R324NestedCrossStepContext.invSqKer_memE : MemEClassT4 invSqKer

The normalized inverse-square edge belongs to the paper's symmetry class.

theorem Anderson4D.R324NestedCrossStepContext.normalizedInput_measurable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (j : Fin (2 * ctx.order - 1)) : Measurable (ctx.normalizedInput j)

theorem Anderson4D.R324NestedCrossStepContext.normalizedInput_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (j : Fin (2 * ctx.order - 1)) (z : T4) : 0 ≤ ctx.normalizedInput j z

theorem Anderson4D.R324NestedCrossStepContext.normalizedInput_admissible {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : IsAdmissiblePrimitiveInput ctx.order ctx.normalizedInput

theorem Anderson4D.R324NestedCrossStepContext.order_le_ambient {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.order ≤ m

Every literal block order is bounded by the ambient perturbative order.

theorem Anderson4D.R324NestedCrossStepContext.ae_centralGapCancellation_reconstruct_eq_one {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ∀ᵐ (v : ctx.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure, ctx.head.centralGapNumerator (ctx.reconstruct v) * invSqKer (ctx.reconstruct v ctx.head.leftGap - ctx.reconstruct v ctx.head.rightGap) = 1

On the genuine current surviving carrier, inserting the moving central-gap numerator times its inverse-square bridge is exactly one almost everywhere. This is the lossless insertion used before any Green edge is replaced by its inverse-square majorant.

theorem Anderson4D.R324NestedCrossStepContext.normalizedHeadDensity_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (t : Fin (2 * ctx.order) → T4) : 0 ≤ ctx.normalizedHeadDensity ρ lam ε t

theorem Anderson4D.R324NestedCrossStepContext.normalizedHeadDensity_measurable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (ctx.normalizedHeadDensity ρ lam ε)

theorem Anderson4D.R324NestedCrossStepContext.exists_normalizedCrossGapTerm_le_majorant_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (ctx : R324NestedCrossStepContext κp κm π) (lam ε : ℝ), 0 < lam → 0 < ε → ε ≤ 1 → m ≤ truncOrder ε → ∀ (z : T4), 0 ≤ ctx.crossGapPrimitiveTerm ρ lam ε ctx.normalizedInput z 0 ∧ ctx.crossGapPrimitiveTerm ρ lam ε ctx.normalizedInput z 0 ≤ primitiveInsertedMajorant C lam ε supportConstant ctx.order z

Truncation-range form of Proposition 4.1 for every normalized literal cross head. The constants are selected once, before the ambient order and the residual schedule.

theorem Anderson4D.R324NestedCrossStepContext.integral_normalizedHeadDensity_eq_endpointTerms {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (hint : MeasureTheory.Integrable (ctx.normalizedHeadDensity ρ lam ε) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure)) : (∫ (t : Fin (2 * ctx.order) → T4), ctx.normalizedHeadDensity ρ lam ε t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure) = ∫ (p : T4 × T4), ctx.crossGapPrimitiveTerm ρ lam ε ctx.normalizedInput p.1 p.2 ∂paperMeasure.prod paperMeasure

Standalone endpoint/internal Fubini identity for one bare normalized block. This is useful inside a proper-head calculation; it is not a claim that the physical Step 4 terminal context can be discarded.

Proper-prefix runs and the explicit Step 4 payload

Paper Step 3 does not collapse the last physical block to a bare radial primitive term. The four external Green edges are still attached to the first, left-gap, right-gap and last coordinates of the remaining block. Moreover, the block containing the selected projected covariance need not be the last element of the unmarked schedule.

Consequently this run removes only literal proper heads which precede a chosen stop carrier. At that carrier it returns the complete four-endpoint context unchanged. The routed endpoint machinery of Step 4, rather than this file, consumes that payload.

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

A concrete four-endpoint context at the point where the proper-prefix iteration stops. No factorization or estimate is hidden in this record: the eventual physical adapter must supply the actual context.

• context : T4 → T4 → T4 → T4 → (step.SurvivingCoordinate → T4) → ℝ
• x : T4
• y : T4
• z : T4
• w : T4

def Anderson4D.R324NestedCrossTerminalPayload.ofContext {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (lam ε : ℝ) (step : R324NestedCrossStepContext κp κm π) (context : T4 → T4 → T4 → T4 → (step.SurvivingCoordinate → T4) → ℝ) (x y z w : T4) : R324NestedCrossTerminalPayload lam ε step

Named constructor for a concrete terminal context and its four external endpoints.

Equations

• Anderson4D.R324NestedCrossTerminalPayload.ofContext lam ε step context x y z w = { context := context, x := x, y := y, z := z, w := w }

def Anderson4D.R324NestedCrossTerminalPayload.unscaledDensity {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {lam ε : ℝ} {step : R324NestedCrossStepContext κp κm π} (payload : R324NestedCrossTerminalPayload lam ε step) : (step.SurvivingCoordinate → T4) → ℝ

The unscaled four-endpoint context at the stop carrier.

Equations

• payload.unscaledDensity = payload.context payload.x payload.y payload.z payload.w

noncomputable def Anderson4D.R324NestedCrossTerminalPayload.density {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {lam ε : ℝ} {step : R324NestedCrossStepContext κp κm π} (payload : R324NestedCrossTerminalPayload lam ε step) : (step.SurvivingCoordinate → T4) → ℝ

The terminal payload retains the exact perturbative weight of the marked head and every outer suffix block. Only the prefix before this carrier may be charged by the proper-run constructors.

Equations

• payload.density v = Anderson4D.lamEps lam ε ^ (2 * step.residual.remainingOrder) * payload.unscaledDensity v

inductive Anderson4D.R324NestedCrossProperPrefixRun {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ρ : SmoothCutoff) (lam ε : ℝ) (stopCarrier : Finset (Fin (2 * m))) (res : R324NestedCrossResidualPrefix κp κm π) : ((↥res.activeCarrier → T4) → ℝ) → ℕ → ℕ → Prop

Proof-relevant exact factorization of the canonical majorant on the unmarked proper prefix before a chosen stop carrier.

The stop constructor deliberately leaves its four-endpoint density opaque. A proper constructor is allowed only when the current head is not the stop carrier and records exactly head × two connectors × next payload. Thus the relation cannot silently apply the proper convolution to the marked/terminal block. The separate physical adapter must justify the preceding norm and edgewise majorization; this relation does not pretend those are equalities.

• stop {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} (step : R324NestedCrossStepContext κp κm π) (hstop : step.head.carrier = stopCarrier) (payload : R324NestedCrossTerminalPayload lam ε step) : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier step.residual payload.density 0 step.residual.remainingOrder
• proper {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} (ctx : R324NestedCrossProperStepContext κp κm π) (hhead : ctx.step.head.carrier ≠ stopCarrier) (nextDensity : (ctx.step.PostCoordinate → T4) → ℝ) (nextPrefixOrder terminalOrder : ℕ) (next : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier ctx.step.next nextDensity nextPrefixOrder terminalOrder) : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier ctx.step.residual (fun (v : ↥ctx.step.residual.activeCarrier → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextDensity fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (ctx.step.order + nextPrefixOrder) terminalOrder

theorem Anderson4D.R324NestedCrossProperPrefixRun.remainingOrder_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier res density prefixOrder terminalOrder) : res.remainingOrder = prefixOrder + terminalOrder

A proper-prefix run partitions the exact remaining cross order into the order charged by the literal proper heads and the order retained in the terminal four-endpoint payload.

theorem Anderson4D.R324NestedCrossProperPrefixRun.prefixOrder_add_terminalOrder {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier res density prefixOrder terminalOrder) : prefixOrder + terminalOrder = res.remainingOrder

Additive orientation of remainingOrder_eq, convenient for consumers which accumulate the proper prefix from inside to outside.

theorem Anderson4D.R324NestedCrossProperPrefixRun.lamEps_pow_remainingOrder_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier res density prefixOrder terminalOrder) : lamEps lam ε ^ (2 * res.remainingOrder) = lamEps lam ε ^ (2 * prefixOrder) * lamEps lam ε ^ (2 * terminalOrder)

Exact multiplication ledger for the perturbative weight along a proper-prefix run.

theorem Anderson4D.R324NestedCrossProperPrefixRun.abs_lamEps_pow_remainingOrder_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {res : R324NestedCrossResidualPrefix κp κm π} {density : (↥res.activeCarrier → T4) → ℝ} {prefixOrder terminalOrder : ℕ} (run : R324NestedCrossProperPrefixRun ρ lam ε stopCarrier res density prefixOrder terminalOrder) : |lamEps lam ε| ^ (2 * res.remainingOrder) = |lamEps lam ε| ^ (2 * prefixOrder) * |lamEps lam ε| ^ (2 * terminalOrder)

Absolute-value form of the exact multiplication ledger, used at the physical norm boundary.

def Anderson4D.R324NestedCrossResidualPrefix.ContainsCarrier {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (stopCarrier : Finset (Fin (2 * m))) : Prop

A residual suffix still contains the chosen stop carrier.

Equations

• res.ContainsCarrier stopCarrier = ∃ block ∈ res.remaining, block.carrier = stopCarrier

theorem Anderson4D.R324NestedCrossResidualPrefix.initial_contains_markedCarrier {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : (initial κp κm π).ContainsCarrier (r324MarkedResidualBlock κp κm π selected)

The initial literal nested schedule contains the unique block carrying the selected projected covariance.

theorem Anderson4D.exists_r324NestedCrossProperPrefixRun_of_containsCarrier {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ρ : SmoothCutoff) (lam ε : ℝ) (stopCarrier : Finset (Fin (2 * m))) (terminalPayload : (step : R324NestedCrossStepContext κp κm π) → step.head.carrier = stopCarrier → R324NestedCrossTerminalPayload lam ε step) (res : R324NestedCrossResidualPrefix κp κm π) (hcontains : res.ContainsCarrier stopCarrier) : ∃ (density : (↥res.activeCarrier → T4) → ℝ) (prefixOrder : ℕ) (terminalOrder : ℕ), R324NestedCrossProperPrefixRun ρ lam ε stopCarrier res density prefixOrder terminalOrder

Structural construction of the proper-prefix trace up to a carrier known to occur in the literal suffix.

The only supplied datum is the actual four-endpoint payload to use when that carrier becomes the head. No terminal majorant, scalar bound, or radial replacement is assumed.

theorem Anderson4D.exists_r324NestedCrossProperPrefixRun_to_markedCarrier {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ρ : SmoothCutoff) (lam ε : ℝ) (terminalPayload : (step : R324NestedCrossStepContext κp κm π) → step.head.carrier = r324MarkedResidualBlock κp κm π selected → R324NestedCrossTerminalPayload lam ε step) : ∃ (density : (↥(R324NestedCrossResidualPrefix.initial κp κm π).activeCarrier → T4) → ℝ) (prefixOrder : ℕ) (terminalOrder : ℕ), R324NestedCrossProperPrefixRun ρ lam ε (r324MarkedResidualBlock κp κm π selected) (R324NestedCrossResidualPrefix.initial κp κm π) density prefixOrder terminalOrder

Specialization of the structural run to the genuine block carrying the selected projected covariance.

Exact integral transition for one proper constructor

This identity is deliberately stated before Proposition 4.1 and retains the genuine cross-gap primitive term. There is no terminal analogue in this file: Step 4 must consume the explicit four-endpoint payload.

theorem Anderson4D.R324NestedCrossProperStepContext.integral_exactProperDensity {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (nextDensity : (ctx.step.PostCoordinate → T4) → ℝ) (hcurrent : MeasureTheory.Integrable (fun (w : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => w (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => w (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => w (ctx.step.postSurvivingCoordinate i)) * nextDensity fun (i : ctx.step.PostCoordinate) => w (ctx.step.postSurvivingCoordinate i)) (MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure)) (hhead : ∀ (post : ctx.step.PostCoordinate → T4), MeasureTheory.Integrable (fun (t : Fin (2 * ctx.step.order) → T4) => ctx.step.normalizedHeadDensity ρ lam ε t * ctx.connector t post) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.step.order)) => paperMeasure)) : (∫ (w : ctx.step.SurvivingCoordinate → T4), ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => w (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => w (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => w (ctx.step.postSurvivingCoordinate i)) * nextDensity fun (i : ctx.step.PostCoordinate) => w (ctx.step.postSurvivingCoordinate i) ∂MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure) = ∫ (post : ctx.step.PostCoordinate → T4), ctx.properHeadIntegral ρ lam ε (post ctx.nextLeftPostCoordinate) (post ctx.nextRightPostCoordinate) * nextDensity post ∂MeasureTheory.Measure.pi fun (x : ctx.step.PostCoordinate) => paperMeasure

Integrating a proper exact-run constructor first over its current head gives the genuine endpoint cross term times the untouched suffix density.