Signed slot budgets for the routed R-324 endpoint series

The final central-frequency route must attach one reciprocal eighth-order cost to a common-increment group without first replacing that group by the sum of the absolute covariance coefficients. This file splits the exact grouped route weight into its finitely many marked-slot contributions.

The qualitative facts (integrability and summability) are proved from the concrete grouped cores. The quantitative input left to the primitive collapse is slotwise, so the paper-scale total bound is no longer repeated as a field of the constructor.

The two endpoint cases in paper Step 4

inductive Anderson4D.SmoothCutoff.R324EndpointReductionCase : Type

The two cases at one external endpoint after the within-half reductions.

• directFourier is the case where the terminal endpoint is not contained in a removed fully-paired interval; its Green factor is Fourier integrated directly.
• insertedSacrifice is the case where the terminal endpoint belongs to such an interval; the same Fourier factor is retained, but the inserted primitive estimate is replaced by the ordinary one at cost ε⁻².

• directFourier : R324EndpointReductionCase
• insertedSacrifice : R324EndpointReductionCase

@[implicit_reducible]

instance Anderson4D.SmoothCutoff.instDecidableEqR324EndpointReductionCase : DecidableEq R324EndpointReductionCase

Equations

• Anderson4D.SmoothCutoff.instDecidableEqR324EndpointReductionCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Anderson4D.SmoothCutoff.instFintypeR324EndpointReductionCase : Fintype R324EndpointReductionCase

Equations

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

def Anderson4D.SmoothCutoff.r324EndpointReductionCaseOfFlag : Bool → R324EndpointReductionCase

Interpret an outgoing endpoint-difference flag as the paper's two-case split. This applies only to a right endpoint: incoming endpoints have a separate carrier-survival test below.

Equations

• Anderson4D.SmoothCutoff.r324EndpointReductionCaseOfFlag false = Anderson4D.SmoothCutoff.R324EndpointReductionCase.directFourier
• Anderson4D.SmoothCutoff.r324EndpointReductionCaseOfFlag true = Anderson4D.SmoothCutoff.R324EndpointReductionCase.insertedSacrifice

def Anderson4D.SmoothCutoff.r324IncomingEndpointReductionCase {m : ℕ} (κ : PartialPairing (Fin m)) : R324EndpointReductionCase

The incoming endpoint is direct precisely when the first internal vertex survives all within-half primitive collapses. If that vertex is removed, its free Green leg must be Fourier-integrated before the responsible block is absorbed, and the ordinary primitive estimate is used at the paper's ε⁻² sacrifice.

At order zero there is no internal endpoint and the choice is immaterial; we use the direct branch as the canonical empty-order value.

Equations

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

@[simp]

theorem Anderson4D.SmoothCutoff.r324IncomingEndpointReductionCase_eq_direct {m : ℕ} (κ : PartialPairing (Fin m)) (hm : 0 < m) (hfirst : ⟨0, hm⟩ ∈ finalActive κ) : r324IncomingEndpointReductionCase κ = R324EndpointReductionCase.directFourier

@[simp]

theorem Anderson4D.SmoothCutoff.r324IncomingEndpointReductionCase_eq_inserted {m : ℕ} (κ : PartialPairing (Fin m)) (hm : 0 < m) (hfirst : ⟨0, hm⟩ ∉ finalActive κ) : r324IncomingEndpointReductionCase κ = R324EndpointReductionCase.insertedSacrifice

noncomputable def Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice (ε : ℝ) : R324EndpointReductionCase → ℝ

Primitive-estimate cost of one endpoint case. The factor two from a Green difference belongs to the exact Fourier coefficient and is not counted again here.

Equations

• Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice ε Anderson4D.SmoothCutoff.R324EndpointReductionCase.directFourier = 1
• Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice ε Anderson4D.SmoothCutoff.R324EndpointReductionCase.insertedSacrifice = ε⁻¹ ^ 2

theorem Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice_nonneg (ε : ℝ) (c : R324EndpointReductionCase) : 0 ≤ r324EndpointPrimitiveSacrifice ε c

theorem Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (c : R324EndpointReductionCase) : r324EndpointPrimitiveSacrifice ε c ≤ ε⁻¹ ^ 2

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointReductionCase {m : ℕ} (p : R324RefinedScheduleIndex m) : Fin 4 → R324EndpointReductionCase

Explicit endpoint-case ledger for one refined schedule.

The incoming cases are governed by survival of the first internal vertex; the outgoing cases are governed by extraction of the final chain edge. These are distinct tests even though both ultimately select the same ordinary-versus-inserted primitive estimate.

Equations

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

@[simp]

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointReductionCase_zero {m : ℕ} (p : R324RefinedScheduleIndex m) : r324RefinedEndpointReductionCase p 0 = r324IncomingEndpointReductionCase (r324RefinedScheduleRepresentative p).fst

@[simp]

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointReductionCase_two {m : ℕ} (p : R324RefinedScheduleIndex m) : r324RefinedEndpointReductionCase p 2 = r324IncomingEndpointReductionCase (r324RefinedScheduleRepresentative p).snd.fst

@[simp]

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointReductionCase_one {m : ℕ} (p : R324RefinedScheduleIndex m) : r324RefinedEndpointReductionCase p 1 = r324EndpointReductionCaseOfFlag (r324OutgoingIsShortcut (r324RefinedScheduleRepresentative p).fst)

@[simp]

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointReductionCase_three {m : ℕ} (p : R324RefinedScheduleIndex m) : r324RefinedEndpointReductionCase p 3 = r324EndpointReductionCaseOfFlag (r324OutgoingIsShortcut (r324RefinedScheduleRepresentative p).snd.fst)

noncomputable def Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrificeProduct (ε : ℝ) (cases : Fin 4 → R324EndpointReductionCase) : ℝ

Product of the four explicit primitive-estimate case costs.

Equations

• Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrificeProduct ε cases = ∏ j : Fin 4, Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice ε (cases j)

theorem Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrificeProduct_nonneg (ε : ℝ) (cases : Fin 4 → R324EndpointReductionCase) : 0 ≤ r324EndpointPrimitiveSacrificeProduct ε cases

theorem Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrificeProduct_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (cases : Fin 4 → R324EndpointReductionCase) : r324EndpointPrimitiveSacrificeProduct ε cases ≤ ε⁻¹ ^ 8

Uniformizing the two cases only after all four endpoint Fourier integrations costs at most ε⁻⁸.

theorem Anderson4D.SmoothCutoff.one_le_r324EndpointPrimitiveSacrifice {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (c : R324EndpointReductionCase) : 1 ≤ r324EndpointPrimitiveSacrifice ε c

Every explicit endpoint-case cost is at least one in the paper regime. Thus introducing the case ledger never understates the exact endpoint Fourier integral.

theorem Anderson4D.SmoothCutoff.one_le_r324EndpointPrimitiveSacrificeProduct {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (cases : Fin 4 → R324EndpointReductionCase) : 1 ≤ r324EndpointPrimitiveSacrificeProduct ε cases

noncomputable def Anderson4D.SmoothCutoff.r324CaseSeparatedEndpointWeight (ε : ℝ) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (cases : Fin 4 → R324EndpointReductionCase) : ℝ

Endpoint coefficient budget before the two cases are uniformized. The Fourier coefficients, and hence the α/β decays, are evaluated before this nonnegative case cost is applied.

Equations

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

theorem Anderson4D.SmoothCutoff.r324CaseSeparatedEndpointWeight_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (cases : Fin 4 → R324EndpointReductionCase) : r324CaseSeparatedEndpointWeight ε α β anchors flags cases ≤ 16 * r324EndpointLoss ε α β

The explicit two-case endpoint ledger gives exactly the same final ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴ budget as the paper, while keeping the direct and inserted-sacrifice branches distinguishable upstream.

theorem Anderson4D.SmoothCutoff.norm_integral_r324EndpointSeparatedIntegrand_le_caseLedger {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (cases : Fin 4 → R324EndpointReductionCase) (core : ℂ) : ‖∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β anchors flags core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure‖ ≤ 16 * r324EndpointLoss ε α β * ‖core‖

Endpoint-first integration routed through the explicit case ledger. This is the local statement used below by the new routed constructor; it does not appeal to the old uniform-sacrifice endpoint theorem.

theorem Anderson4D.SmoothCutoff.norm_integral_r324EndpointSeparatedIntegrand_le_refinedCaseLedger {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) (core : ℂ) : ‖∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β (r324ContractionEndpointAnchors hm (r324RefinedScheduleRepresentative p) v) (r324ContractionEndpointFlags (r324RefinedScheduleRepresentative p)) core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure‖ ≤ 16 * r324EndpointLoss ε α β * ‖core‖

The canonical ledger attached to a refined schedule, with carrier-survival tests at the two incoming endpoints and extraction-edge tests at the two outgoing endpoints, controls its actual endpoint integral.

theorem Anderson4D.SmoothCutoff.norm_integral_r324EndpointSeparatedIntegrand_le_fourierOnly (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℂ) : ‖∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β anchors flags core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure‖ ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ‖core‖

The genuine endpoint Fourier estimate before any ordinary-versus-inserted primitive sacrifice is charged. This is the endpoint estimate used with the ε⁸-normalized route weight below.

Qualitative control of the signed grouped core

theorem Anderson4D.SmoothCutoff.norm_r324KeyGroupedCovarianceConfiguration_le (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ‖ρ.r324KeyGroupedCovarianceConfiguration hm ε p b v‖ ≤ ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p b

The norm of a common-increment covariance group is bounded by the fibrewise sum of the raw coefficient norms. The norm is taken only after the complete refined contraction fibre has been summed.

theorem Anderson4D.SmoothCutoff.norm_r324KeyGroupedRefinedEndpointCore_le (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p b v‖ ≤ r324SelectedInteriorSkeletonNormDensity (r324RefinedScheduleRepresentative p).fst (r324RefinedScheduleRepresentative p).snd.fst v * ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p b

Pointwise signed-core majorant. The complete compatible primitive fibre remains inside the norm on the left.

theorem Anderson4D.SmoothCutoff.integrable_norm_r324KeyGroupedRefinedEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (b : ℕ) : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p b v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

Every signed common-increment internal core has finite L¹ mass. This closes the qualitative field of IntegratedPrimitiveCollapseBudget without an analytic hypothesis.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedInteriorSkeletonL1 {m : ℕ} (p : R324RefinedScheduleIndex m) : ℝ

L¹ mass of the two signed, endpoint-independent Green profiles for one refined schedule.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedInteriorSkeletonL1_nonneg {m : ℕ} (p : R324RefinedScheduleIndex m) : 0 ≤ r324RefinedInteriorSkeletonL1 p

theorem Anderson4D.SmoothCutoff.r324GroupedRefinedCoreL1_le_skeleton_mul_covariance (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (b : ℕ) : ρ.r324GroupedRefinedCoreL1 hm ε (p, b) ≤ r324RefinedInteriorSkeletonL1 p * ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p b

The signed grouped core is bounded by its schedule's exact Green profile mass times the scalar covariance mass. This estimate is used only to prove qualitative summability, not for the paper-scale bound.

noncomputable def Anderson4D.SmoothCutoff.r324AllRefinedInteriorSkeletonL1 (m : ℕ) : ℝ

A finite qualitative envelope for all refined Green-profile masses at fixed order.

Equations

• Anderson4D.SmoothCutoff.r324AllRefinedInteriorSkeletonL1 m = ∑ p : Anderson4D.R324RefinedScheduleIndex m, Anderson4D.SmoothCutoff.r324RefinedInteriorSkeletonL1 p

theorem Anderson4D.SmoothCutoff.r324AllRefinedInteriorSkeletonL1_nonneg (m : ℕ) : 0 ≤ r324AllRefinedInteriorSkeletonL1 m

theorem Anderson4D.SmoothCutoff.r324RefinedInteriorSkeletonL1_le_all {m : ℕ} (p : R324RefinedScheduleIndex m) : r324RefinedInteriorSkeletonL1 p ≤ r324AllRefinedInteriorSkeletonL1 m

theorem Anderson4D.SmoothCutoff.summable_r324GroupedRouteBaseWeight_signed (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) : Summable (ρ.r324GroupedRouteBaseWeight lam hm ε)

The grouped route base weights are summable without assuming the paper-scale estimate. The coarse scalar majorant is confined to this qualitative convergence proof.

noncomputable def Anderson4D.SmoothCutoff.r324EndpointNormalizedGroupedRouteBaseWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : ℝ

Endpoint-normalized complete grouped route weight. The factor ε⁸ belongs to the primitive-collapse side and cancels the four possible ordinary-versus-inserted sacrifices.

Equations

• ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε p = ε ^ 8 * ρ.r324GroupedRouteBaseWeight lam hm ε p

theorem Anderson4D.SmoothCutoff.r324EndpointNormalizedGroupedRouteBaseWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : 0 ≤ ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε p

theorem Anderson4D.SmoothCutoff.summable_r324EndpointNormalizedGroupedRouteBaseWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) : Summable (ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε)

Local routed estimate with primitive-side normalization

theorem Anderson4D.SmoothCutoff.norm_r324GroupedEndpointConfigurationTerm_le_normalizedRouteWeight_mul_decay (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) (hcore : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2 v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) (i : Fin m) : ‖r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p.1) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2)‖ ≤ 16 * r324EndpointLoss ε α β * ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε p * eighthOrderFrequencyDecay ‖ρ.r324ConcreteRefinedIncrement lam hm ε α β p i‖

Local grouped routed estimate for the endpoint-normalized base weight. Only the genuine four Fourier coefficients are estimated at the endpoint; the ε⁻⁸ in r324EndpointLoss cancels the ε⁸ carried by the base weight. The primitive branch costs are therefore paid exactly once, inside the collapse data below.

theorem Anderson4D.SmoothCutoff.norm_r324GroupedEndpointConfigurationTerm_le_caseLedgerRouteWeight_mul_decay (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) (hcore : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2 v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) (i : Fin m) : ‖r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p.1) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2)‖ ≤ 16 * r324EndpointLoss ε α β * ρ.r324GroupedRouteBaseWeight lam hm ε p * eighthOrderFrequencyDecay ‖ρ.r324ConcreteRefinedIncrement lam hm ε α β p i‖

Raw-weight estimate for the pre-normalization helper API below.

Exact finite marked-slot decomposition

noncomputable def Anderson4D.SmoothCutoff.r324SignedRouteSlotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (p : R324RefinedScheduleIndex m × ℕ) : ℝ

Contribution of one marked increment slot to the grouped route weight. The norm is still taken after the complete compatible primitive fibre has been summed.

Equations

• ρ.r324SignedRouteSlotWeight lam hm ε i p = |Anderson4D.lamEps lam ε| ^ (2 * m) * ρ.r324GroupedRefinedCoreL1 hm ε p * Anderson4D.SmoothCutoff.r324GroupedIncrementCost hm p.2 i

noncomputable def Anderson4D.SmoothCutoff.r324EndpointNormalizedSignedRouteSlotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (p : R324RefinedScheduleIndex m × ℕ) : ℝ

Endpoint-normalized marked-slot weight. The factor ε⁸ is kept on the primitive-density side. It cancels the four possible ε⁻² ordinary-versus-inserted sacrifices before the hard-coded r324EndpointLoss is attached by the routing layer.

Equations

• ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i p = ε ^ 8 * ρ.r324SignedRouteSlotWeight lam hm ε i p

theorem Anderson4D.SmoothCutoff.r324SignedRouteSlotWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (p : R324RefinedScheduleIndex m × ℕ) : 0 ≤ ρ.r324SignedRouteSlotWeight lam hm ε i p

theorem Anderson4D.SmoothCutoff.r324EndpointNormalizedSignedRouteSlotWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (p : R324RefinedScheduleIndex m × ℕ) : 0 ≤ ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i p

theorem Anderson4D.SmoothCutoff.r324GroupedRouteBaseWeight_eq_sum_signedRouteSlotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : ρ.r324GroupedRouteBaseWeight lam hm ε p = ∑ i : Fin m, ρ.r324SignedRouteSlotWeight lam hm ε i p

The old base weight is definitionally the finite sum of the genuine marked-slot weights.

theorem Anderson4D.SmoothCutoff.r324EndpointNormalizedGroupedRouteBaseWeight_eq_sum_slotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε p = ∑ i : Fin m, ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i p

The normalized grouped weight is still exactly the finite sum of its normalized marked-slot pieces.

theorem Anderson4D.SmoothCutoff.r324SignedRouteSlotWeight_le_baseWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (p : R324RefinedScheduleIndex m × ℕ) : ρ.r324SignedRouteSlotWeight lam hm ε i p ≤ ρ.r324GroupedRouteBaseWeight lam hm ε p

Each marked-slot weight is bounded by the complete base weight.

theorem Anderson4D.SmoothCutoff.summable_r324SignedRouteSlotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) : Summable (ρ.r324SignedRouteSlotWeight lam hm ε i)

Every marked-slot series is summable, independently of the paper-scale quantitative collapse.

theorem Anderson4D.SmoothCutoff.summable_r324EndpointNormalizedSignedRouteSlotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) : Summable (ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i)

theorem Anderson4D.SmoothCutoff.tsum_r324GroupedRouteBaseWeight_eq_sum_slot_tsum (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedRouteBaseWeight lam hm ε p = ∑ i : Fin m, ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p

Exact exchange of the countable grouped sum with the finite marked slot sum. This is the cancellation-preserving boundary at which the primitive collapse may estimate one selected high-frequency edge.

theorem Anderson4D.SmoothCutoff.tsum_r324EndpointNormalizedGroupedRouteBaseWeight_eq_sum_slot_tsum (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε p = ∑ i : Fin m, ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i p

Non-circular primitive-collapse consumer

structure Anderson4D.SmoothCutoff.SignedRoutedPrimitiveSlotBudget (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (slotAmplitude : Fin m → ℝ) : Prop

Quantitative output expected from the signed marked-edge primitive collapse. It bounds each marked slot separately; it does not contain the downstream total tsum_baseWeight_le statement.

The endpoint cases are recoverable from r324RefinedEndpointReductionCase, while the central-frequency cost is attached only to r324SignedRouteSlotWeight.

• slot_tsum_le (i : Fin m) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p ≤ slotAmplitude i

structure Anderson4D.SmoothCutoff.EndpointNormalizedSignedRoutedPrimitiveSlotBudget (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (slotAmplitude : Fin m → ℝ) : Prop

Slotwise budget for the endpoint-normalized weights used by the paper-faithful routed constructor.

• slot_tsum_le (i : Fin m) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i p ≤ slotAmplitude i

Proposition 4.1 / phase-A input boundary

noncomputable def Anderson4D.SmoothCutoff.r324EndpointCasePrimitiveMajorant (c : R324EndpointReductionCase) (C lam ε supportConstant : ℝ) (m : ℕ) (z : T4) : ℝ

The actual Proposition 4.1 majorant used by one endpoint case. The direct branch retains the diameter insertion. The sacrifice branch, which occurs when the adjacent internal vertex is absorbed by a primitive collapse, is the ordinary J majorant.

Equations

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

theorem Anderson4D.SmoothCutoff.r324EndpointCasePrimitiveMajorant_le_sacrifice_mul_inserted (c : R324EndpointReductionCase) (C lam supportConstant : ℝ) (m : ℕ) {ε : ℝ} (hε : 0 < ε) (z : T4) : r324EndpointCasePrimitiveMajorant c C lam ε supportConstant m z ≤ r324EndpointPrimitiveSacrifice ε c * primitiveInsertedMajorant C lam ε supportConstant m z

Constructive ordinary-versus-inserted bridge.

The direct branch is already inserted. In the absorbed-vertex branch the terminal density is the ordinary J majorant and Proposition 4.1's diameter insertion is genuinely given up at cost ε⁻². The cost is therefore charged to the primitive density, not to a Fourier coefficient. This description applies equally to incoming and outgoing endpoints.

theorem Anderson4D.SmoothCutoff.integrable_r324EndpointCasePrimitiveMajorant (c : R324EndpointReductionCase) (C lam supportConstant : ℝ) (m : ℕ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (r324EndpointCasePrimitiveMajorant c C lam ε supportConstant m) paperMeasure

The case majorant is integrable in both branches.

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324EndpointReductionPattern : Type

The finite four-endpoint case pattern retained by the collapse certificate.

Equations

• Anderson4D.SmoothCutoff.R324EndpointReductionPattern = (Fin 4 → Anderson4D.SmoothCutoff.R324EndpointReductionCase)

noncomputable def Anderson4D.SmoothCutoff.r324EndpointPatternAdjustedPrimitiveMajorant (ε : ℝ) (cases : R324EndpointReductionPattern) (C lam supportConstant : ℝ) (m : ℕ) (z : T4) : ℝ

Density majorant after applying the constructive one-endpoint bridge at every endpoint in a case pattern.

Equations

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

theorem Anderson4D.SmoothCutoff.eps_pow_eight_mul_endpointPatternAdjustedMajorant_le_inserted {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (cases : R324EndpointReductionPattern) {C lam : ℝ} (hC : 0 ≤ C) (hlam : 0 ≤ lam) (supportConstant : ℝ) (m : ℕ) (z : T4) : ε ^ 8 * r324EndpointPatternAdjustedPrimitiveMajorant ε cases C lam supportConstant m z ≤ primitiveInsertedMajorant C lam ε supportConstant m z

Multiplying a four-case-adjusted density by ε⁸ cancels all possible ordinary-J sacrifices.

structure Anderson4D.SmoothCutoff.SignedRoutedPrimitiveSlotCollapseData (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (primitiveConstant supportConstant : ℝ) : Type

The canonical scalar output of the signed phase-A iteration and the one-open-edge cross-terminal consumer.

For every possible routed slot, phase A splits the actual relative-endpoint density by the four endpoint-case pattern. The direct branch retains primitiveInsertedMajorant; the absorbed-vertex branch uses ordinary primitiveKernelMajorant, and the constructive theorem above charges its ε⁻² loss to the density. The four adjusted costs are then cancelled by the ε⁸ normalization before the routing layer introduces r324EndpointLoss.

The forthcoming marker-preserving phase-A closure can instantiate the fields directly by grouping schedules according to r324RefinedEndpointReductionCase.

• density : Fin m → R324EndpointReductionPattern → T4 → ℝ
• density_integrable (i : Fin m) (cases : R324EndpointReductionPattern) : MeasureTheory.Integrable (self.density i cases) paperMeasure
• normalized_slot_fiber_le_scaled_case_density_integrals (i : Fin m) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324EndpointNormalizedSignedRouteSlotWeight lam hm ε i p ≤ ∑ cases : R324EndpointReductionPattern, ∫ (z : T4), ε ^ 8 * self.density i cases z ∂paperMeasure
• pointwise_case_domination (i : Fin m) (cases : R324EndpointReductionPattern) (z : T4) : self.density i cases z ≤ r324EndpointPatternAdjustedPrimitiveMajorant ε cases primitiveConstant lam supportConstant m z

def Anderson4D.SmoothCutoff.signedRoutedPrimitiveSlotCollapseData_of_rawCaseDensities (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (hm : 0 < m) (primitiveConstant supportConstant : ℝ) (density : Fin m → R324EndpointReductionPattern → T4 → ℝ) (density_integrable : ∀ (i : Fin m) (cases : R324EndpointReductionPattern), MeasureTheory.Integrable (density i cases) paperMeasure) (raw_slot_fiber_le_case_density_integrals : ∀ (i : Fin m), ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p ≤ ∑ cases : R324EndpointReductionPattern, ∫ (z : T4), density i cases z ∂paperMeasure) (pointwise_case_domination : ∀ (i : Fin m) (cases : R324EndpointReductionPattern) (z : T4), density i cases z ≤ r324EndpointPatternAdjustedPrimitiveMajorant ε cases primitiveConstant lam supportConstant m z) : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant

Construct the normalized collapse datum from the raw phase-A case-fibre inequality. This is the exact place where the ε⁸ normalization is moved through the countable sum and the finite family of density integrals.

Equations

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

theorem Anderson4D.SmoothCutoff.endpointNormalizedSignedRoutedPrimitiveSlotBudget_of_collapseData (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (primitiveConstant supportConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (d : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant) : ρ.EndpointNormalizedSignedRoutedPrimitiveSlotBudget lam ε m hm fun (_i : Fin m) => 16 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure

A concrete phase-A/cross-terminal certificate gives the normalized slot budget. The proof first uses the actual ordinary-J case costs in the density, then cancels those costs with ε⁸; it never attaches the cost to a Fourier coefficient.

theorem Anderson4D.SmoothCutoff.integratedPrimitiveCollapseBudget_of_signedRoutedPrimitiveSlots (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (slotAmplitude : Fin m → ℝ) (d : ρ.SignedRoutedPrimitiveSlotBudget lam ε m hm slotAmplitude) : ρ.IntegratedPrimitiveCollapseBudget lam ε m hm (∑ i : Fin m, slotAmplitude i)

Slotwise signed primitive estimates construct the old downstream budget. Integrability and summability are theorems here, not fields repeated as analytic assumptions.

theorem Anderson4D.SmoothCutoff.countableCentralRoutedMomentReductionOutput_of_integratedPrimitiveCollapseBudget_caseLedger (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (α β : Z4) (amplitude : ℝ) (budget : ρ.IntegratedPrimitiveCollapseBudget lam ε m hm amplitude) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (16 * amplitude * r324EndpointLoss ε α β)

Case-ledger routed consumer. Its exact countable configuration expansion uses the local estimate the theorem above whose endpoint proof explicitly traverses the four R324EndpointReductionCases.

theorem Anderson4D.SmoothCutoff.countableCentralRoutedMomentReductionOutput_of_signedRoutedPrimitiveSlots (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (α β : Z4) (slotAmplitude : Fin m → ℝ) (d : ρ.SignedRoutedPrimitiveSlotBudget lam ε m hm slotAmplitude) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β ((16 * ∑ i : Fin m, slotAmplitude i) * r324EndpointLoss ε α β)

Direct routed-output constructor from the slotwise signed collapse. The endpoint loss is introduced only after the explicit endpoint case ledger and the central marked-slot budget have both closed.

Canonical inserted-majorant amplitude and order absorption

theorem Anderson4D.SmoothCutoff.tsum_endpointNormalizedGroupedRouteBaseWeight_le_of_signedPrimitiveCollapse (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (primitiveConstant supportConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (d : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324EndpointNormalizedGroupedRouteBaseWeight lam hm ε p ≤ ↑m * (16 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure)

The exact normalized endpoint-free budget obtained from a phase-A/cross-terminal certificate. The factor 16 is the number of four-endpoint case patterns; the only order-dependent loss is the literal number m of possible marked slots.

theorem Anderson4D.SmoothCutoff.countableCentralRoutedMomentReductionOutput_of_signedRoutedPrimitiveCollapse (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (α β : Z4) (primitiveConstant supportConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (d : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (16 * (↑m * (16 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure)) * r324EndpointLoss ε α β)

Direct routed output at the unabsorbed canonical Proposition 4.1 integral. Ordinary-J absorbed-vertex branches have already been paid on the density side and cancelled by the normalized base weight.

theorem Anderson4D.SmoothCutoff.r324_order_le_two_pow_double_sub_two {m : ℕ} (hm : 1 ≤ m) : m ≤ 2 ^ (2 * m - 2)

The number of possible marked slots is exponentially harmless in the exact exponent needed after extracting the leading coupling square.

theorem Anderson4D.SmoothCutoff.exists_signedRoutedPrimitiveCollapse_paperAmplitude {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (lam ε : ℝ) (m : ℕ), 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → 16 * (↑m * (16 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure)) ≤ lamEps lam ε ^ 2 * outerConstant * (2 * primitiveConstant * lam) ^ (2 * m - 2)

Radial integration plus the exact m-slot sum has the standard paper-scale coupling form. The loss m is absorbed by m ≤ 2^(2m-2), so it changes only the named power constant C ↦ 2C; no polynomial-in-order factor remains.

theorem Anderson4D.SmoothCutoff.exists_countableCentralRoutedMomentReductionOutput_of_signedPrimitiveCollapse {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → ∀ (a : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant), CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (2 * primitiveConstant * lam) ^ (2 * m - 2) * r324EndpointLoss ε α β)

Phase A and the selected cross-terminal certificate therefore produce the routed paper-scale output directly. The conclusion is monotone from the exact unabsorbed endpoint budget, so no target-shaped total estimate is assumed.