Order-capped R-324 conditional closure

The paper uses the fibre bounds only for orders m ≤ truncOrder ε = ⌊|log ε|⌋. Under that cap the factorial count is affordable inside the same budget: for 1 ≤ m ≤ truncOrder ε

m! ≤ m^m ≤ 2^m · |log ε|^{m-1} (r324CappedRebase_factorial_affordable), so the floor C₀·m!·c^m ≤ ∫ (cross density) is compatible with ∫ ≤ K^m·|log ε|^{m-1} for K ≥ 2c — no explicit m! allowance is needed in the capped Props, and none may appear in the term-sum ledger (a factorial there could not pass the per-order bridge with an ε-uniform primitive constant). The capped cross Prop still implies the recorded weakest residual form R324PermCrossOrderCappedCrossBound (R324CappedCrossLedger.toOrderCappedCrossBound).

The capped Props are threaded through the per-m bridge and the final assembly — which only ever instantiates m ≤ truncOrder ε — to the capped conditional main theorem mainConditional_of_analyticResiduals_capped.

The capped residual Props

def Anderson4D.R324CappedCrossLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

Capped cross ledger (uniform branch): the phase-free integral of the summed pure-cross density carries the windowed value K^m·L^{m-1}, for orders up to the paper truncation A = ⌊|log ε|⌋ = truncOrder ε only. By r324CappedRebase_factorialFloor_affordable this budget affords the proved m!-floor on the capped range, unlike its refuted uncapped ancestor R324HdetCrossIntegralBound.

Equations

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

def Anderson4D.R324CappedMixedLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

Capped mixed ledger: the residual-refined fibre logarithmic bound on fibres retaining a within-half pair, for orders up to the paper truncation only.

Equations

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

def Anderson4D.R324CappedBracketLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

Capped bracket ledger (routed branch): the proved R324HdetBracketLedgerBound already carries the order cap 2 ≤ m ≤ truncOrder ε and needs no change; it is re-exported under the capped naming scheme.

Equations

• Anderson4D.R324CappedBracketLedger ρ K = Anderson4D.R324HdetBracketLedgerBound ρ K

Affordability of the factorial under the cap

theorem Anderson4D.r324CappedRebase_factorial_affordable {ε : ℝ} {m : ℕ} (hm : 1 ≤ m) (hcap : m ≤ truncOrder ε) : ↑m.factorial ≤ 2 ^ m * |Real.log ε| ^ (m - 1)

The affordability lemma. On the capped range 1 ≤ m ≤ truncOrder ε ≤ |log ε| the factorial fibre count fits the logarithmic budget: m! ≤ m^m ≤ 2^m·|log ε|^{m-1}.

theorem Anderson4D.r324CappedRebase_factorialFloor_affordable {ε c : ℝ} {m : ℕ} (hc : 0 ≤ c) (hm : 1 ≤ m) (hcap : m ≤ truncOrder ε) : ↑m.factorial * c ^ m ≤ (2 * c) ^ m * |Real.log ε| ^ (m - 1)

The precise reconciliation form: on the capped range the proved factorial floor m!·c^m sits inside the geometric logarithmic budget at the doubled constant, so the capped cross Prop is not floor-refutable.

theorem Anderson4D.R324CappedCrossLedger.toOrderCappedCrossBound {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324CappedCrossLedger ρ K) : R324PermCrossOrderCappedCrossBound ρ K

The capped cross ledger implies the recorded weakest sound residual form (which grants an explicit m! allowance).

The capped uniform branch

theorem Anderson4D.r324CappedRebase_fibreLogBound {ρ : SmoothCutoff} {K₁ K₂ : ℝ} (hK₁ : 0 ≤ K₁) (hK₂ : 0 ≤ K₂) (hcross : R324CappedCrossLedger ρ K₁) (hmixed : R324CappedMixedLedger ρ K₂) {ε : ℝ} (m : ℕ) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm3 : 3 ≤ m) (hcap : m ≤ truncOrder ε) : R324GeneralPeelFibreLogBound ρ ε m α β (max K₁ K₂)

The two capped case ledgers fund the per-fibre logarithmic ledger at each fixed capped order, through the proved density majorization on pure-cross fibres.

theorem Anderson4D.r324CappedRebase_exists_outputAt (ρ : SmoothCutoff) (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedger ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedMixedLedger ρ K) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → m ≤ truncOrder ε → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C₀ 1

Capped uniform-branch supply. One per-cutoff primitive constant discharges the residual-refined reduction obligation at every capped order 1 ≤ m ≤ truncOrder ε: the proved unconditional low orders below three, the capped ledgers through the proved per-m bridge from three.

Landing in the frozen deterministic right side

theorem Anderson4D.r324CappedRebase_exists_deterministicMoment_bound (ρ : SmoothCutoff) (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedger ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedBracketLedger ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 ≤ lam → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The fixed-scale deterministic (3.24) bound from the three capped residual Props. Verbatim the proved assembly r324HdetAssembly_exists_deterministicMoment_bound with the uniform branch re-based on the capped supply: the assembly only ever instantiates orders m ≤ truncOrder ε, so the cap threads through with no loss.

The hdet hypothesis and the capped conditional main theorem

theorem Anderson4D.r324CappedRebase_hdet (ρ : SmoothCutoff) (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedger ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedBracketLedger ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The exact hdet hypothesis of the proved mainConditional_of_deterministic_bounds, delivered from the three capped residual Props.

theorem Anderson4D.mainConditional_of_analyticResiduals_capped {M : NoiseModel} {ρ : SmoothCutoff} (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedger ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedBracketLedger ρ K) : MainConditional M ρ

The capped conditional main theorem. The complete MainConditional M ρ follows from the three order-capped analytic obligations, each restricted to the paper truncation range m ≤ truncOrder ε = ⌊|log ε|⌋:

• the capped pure-cross density bound (R324CappedCrossLedger, uniform branch, 3 ≤ m ≤ truncOrder ε) — the sound replacement of the refuted R324HdetCrossIntegralBound;
• the capped mixed-fibre ledger (R324CappedMixedLedger, 3 ≤ m ≤ truncOrder ε) — the sound replacement of the (jointly refuted) uncapped R324LedgerThreeMixedLedger;
• the bracket-retaining fibre ledger (R324CappedBracketLedger = proved R324HdetBracketLedgerBound, routed branch, 2 ≤ m ≤ truncOrder ε, unchanged).

The counterterm input is the proved unconditional R322AnalyticResidualPrefix.exists_r322_renormC2q_bound; the order-one routed branch is proved and unconditional. The three capped Props are genuine analytic hypotheses; unlike their uncapped counterparts they are not refutable by the factorial fibre floor (r324CappedRebase_factorialFloor_affordable).