The routed slot budget for R-324 (INEQ 2) and the capstone assembly

The second residual input of the final R-324 assembly is the routed slot budget: at every marked slot the countable signed route weight is dominated by the integrated inserted majorant. As with the interior estimate, the coupling power |λ_ε|^{2m} = λ^{2m}/|log ε|^m factors out of the slot series exactly, so the budget reduces to a coupling-free logarithmic inequality R324SlotLogBudget on the grouped-core slot series.

The capstone theorem exists_deterministicMoment_paper_bound_of_logBudgets then produces the paper bound (3.24) from the two logarithmic budgets alone: every Fourier-mode layer, endpoint case split, routing datum, and majorant integral is discharged unconditionally.

def Anderson4D.R324SlotLogBudget (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε primitiveConstant : ℝ) : Prop

The residual slot budget (INEQ 2, reduced form). At every marked slot, the |log ε|-weighted countable slot series of grouped interior L¹ masses against reciprocal routed costs is controlled by C^{2m} |log ε|^m. Like the interior budget, it mentions no coupling, no Fourier mode, no majorant integral, and no support constant.

Equations

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

theorem Anderson4D.r324SignedRouteSlotWeight_eq_pow_mul (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (p : R324RefinedScheduleIndex m × ℕ) : ρ.r324SignedRouteSlotWeight lam hm ε i p = |lamEps lam ε| ^ (2 * m) * (ρ.r324GroupedRefinedCoreL1 hm ε p * SmoothCutoff.r324GroupedIncrementCost hm p.2 i)

The signed route slot weight is the coupling power times the coupling-free grouped slot term.

theorem Anderson4D.slot_tsum_le_integral_insertedMajorant_of_logBudget {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hlam : 0 ≤ lam) (hsupport : 0 < supportConstant) (budget : R324SlotLogBudget ρ hm ε (min supportConstant 1 ^ 2 / supportConstant * primitiveConstant)) (i : Fin m) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure

The logarithmic slot budget discharges the routed slot budget. Same arithmetic as the interior bridge: the coupling power factors out of the slot series, the leftover |log ε|^{m-1} is absorbed by the majorant's near-field mass, and the support-constant distortion min(c,1)²/c ≤ 1 is paid inside the budget's constant.

The slot budget dominates the interior budget

theorem Anderson4D.one_le_r324GroupedIncrementCost {m : ℕ} (hm : 0 < m) (b : ℕ) (i : Fin m) : 1 ≤ SmoothCutoff.r324GroupedIncrementCost hm b i

Every reciprocal routed cost is at least one.

theorem Anderson4D.summable_groupedCoreL1_mul_cost (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hlog : 1 ≤ |Real.log ε|) (i : Fin m) : Summable fun (p : R324RefinedScheduleIndex m × ℕ) => ρ.r324GroupedRefinedCoreL1 hm ε p * SmoothCutoff.r324GroupedIncrementCost hm p.2 i

Coupling-free summability of the grouped slot series, extracted from the proved signed-route summability at coupling 1.

theorem Anderson4D.r324RefinedInteriorCoreIntegral_le_tsum_groupedCoreL1 (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (hsum : Summable fun (b : ℕ) => ρ.r324GroupedRefinedCoreL1 hm ε (p, b)) : r324RefinedInteriorCoreIntegral ρ ε m p ≤ ∑' (b : ℕ), ρ.r324GroupedRefinedCoreL1 hm ε (p, b)

Blockwise triangle comparison. The interior L¹ mass of one refined fibre is dominated by the ℕ-series of its grouped-core L¹ masses: the common-increment groups reassemble the fibre exactly (tsum_r324KeyGroupedRefinedEndpointCore), and the norm passes inside the countable regrouping by Tonelli.

theorem Anderson4D.r324InteriorCoreLogBudget_of_slotLogBudget {ρ : SmoothCutoff} {ε : ℝ} {m : ℕ} {primitiveConstant : ℝ} (hm : 0 < m) (hε : 0 < ε) (hlog : 1 ≤ |Real.log ε|) (budget : R324SlotLogBudget ρ hm ε primitiveConstant) : R324InteriorCoreLogBudget ρ ε m (4 * primitiveConstant)

The slot budget dominates the interior budget. For every refined fibre, at the marked slot 0: the fibre's interior L¹ mass is at most its own grouped slot series (triangle comparison, cost ≥ 1), which is a nonnegative sub-series of the full slot series. The factor 16 is absorbed by C ↦ 4C since 16 ≤ 16^m.

The capstone assembly

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_logBudgets {primitiveConstant : ℝ} (hprimitive : 0 < primitiveConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324InteriorCoreLogBudget ρ ε m primitiveConstant → R324SlotLogBudget ρ hm ε primitiveConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

The R-324 deterministic moment paper bound from the two logarithmic budgets. Both inputs of the P-3.5b-det chain are consumed in their reduced, coupling-free logarithmic form (at the support constant 1): the interior-core budget discharges the middle estimate at every Fourier mode, and the slot budget discharges the signed routed collapse datum. Everything else — the direct Fourier evaluation of the four endpoint legs, the countable regrouping of the route series, the majorant integrations, and the mode-decay bracket of (3.24) — is unconditional.

theorem Anderson4D.exists_deterministicMoment_decay_bound_of_logBudgets {primitiveConstant : ℝ} (hprimitive : 0 < primitiveConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324InteriorCoreLogBudget ρ ε m primitiveConstant → R324SlotLogBudget ρ hm ε primitiveConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

Literal decay form of the estimate: the min bracket of paperDeterministicMomentRHS is bounded by the P-3.5b-det decay ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε²(α+β)⟩⁻⁸.

The single-residual capstone

theorem Anderson4D.R324SlotLogBudget.mono {ρ : SmoothCutoff} {m : ℕ} {hm : 0 < m} {ε primitiveConstant primitiveConstant' : ℝ} (hC : 0 ≤ primitiveConstant) (hle : primitiveConstant ≤ primitiveConstant') (budget : R324SlotLogBudget ρ hm ε primitiveConstant) : R324SlotLogBudget ρ hm ε primitiveConstant'

The slot budget is monotone in its constant.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_slotBudget {primitiveConstant : ℝ} (hprimitive : 0 < primitiveConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324SlotLogBudget ρ hm ε primitiveConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (64 * primitiveConstant) lam ε m α β

The R-324 deterministic moment paper bound from the slot budget alone. The interior-core budget is derived from the slot budget by the blockwise triangle comparison, so a single residual scalar inequality — the |log ε|-weighted slot series against C^{2m}|log ε|^m — yields the complete paper bound (3.24) with power constant 64C.

theorem Anderson4D.exists_deterministicMoment_decay_bound_of_slotBudget {primitiveConstant : ℝ} (hprimitive : 0 < primitiveConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324SlotLogBudget ρ hm ε primitiveConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (64 * primitiveConstant * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

Literal decay form of the single-residual capstone.