Final hdet assembly: conditional closure of the deterministic moment bound

The analytic residuals are stated as named Props and composed to the exact hdet hypothesis of mainConditional_of_deterministic_bounds, with all constants fixed by the cutoff before the coupling.

• R324HdetCrossIntegralBound — the injectivity-retaining cross-density integral hypothesis of the uniform-branch closure exists_momentRefinedIntegratedReductionOutputAt_of_crossIntegral_and_mixed; the bijection sum is retained throughout.
• R324HdetBracketLedgerBound — the bracket-retaining variant at the same residual-refined fibre level: each fibre term sum pays the windowed value m⁸·K^m·L^{m-1} times the endpoint loss and one central eighth-order bracket at the natural pointwise-harvest scale ⟨ε‖freq(α+β)‖⟩⁻⁸ (funded by the half-symbol split r324HdetAssembly_exists_halfSymbol_sq_bracket, the product bracket r324HdetAssembly_prod_eighthDecay_le over the momentum-conserving keys, and increment telescoping).
• R324LedgerThreeMixedLedger — the proved mixed-fibre ledger.

Routed-branch interfaces. At m = 1 the countable central routed output is consumed unconditionally through the proved countableCentralRoutedMomentReductionOutput_of_routedWindow chain (coupling-uniform replay in the kit file). For m ≥ 2 the countable interface countableCentralRoutedMomentReductionOutput_of_signedCentralDecay demands the bracket at a routed-increment scale ⟨‖freq‖/nInc⟩⁻⁸ with 1 ≤ nInc ≤ truncOrder ε; on the admissible range ε ≤ 1/4 one has ε ≤ 1/truncOrder ε ≤ 1/nInc, so every admissible demand is strictly stronger than the ⟨ε‖freq‖⟩⁻⁸ bracket produced by the pointwise product harvest — the countable normalization cannot be met from this Prop. The m ≥ 2 branch therefore lands in the paper bracket through the proved flexible-amplitude combiner le_mul_min_of_le_of_le_mul and the scale comparison r324HdetAssembly_endpointLoss_mul_epsScale_le_paper, parallel to the proved countable consumer deterministicMomentPairingSum_paper_bound_of_uniform_and_countable used verbatim at m = 1.

Uniform-branch reduction

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_of_crossIntegral_and_mixed (ρ : SmoothCutoff) (hcross : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {ε : ℝ} (m : ℕ), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 3 ≤ m → ∀ (F : Finset (MomentContraction m)), (∀ e ∈ F, R324LedgerThreeAllCrossEntity e) → ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m ≤ K ^ m * |Real.log ε| ^ (m - 1)) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeMixedLedger ρ K) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C₀ 1

The complete uniform branch follows from an injectivity-retaining pure-cross integral bound and the mixed-fibre ledger.

Analytic hypotheses

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

Injectivity-retaining cross bound (uniform branch): verbatim the hcross hypothesis of the proved exists_momentRefinedIntegratedReductionOutputAt_of_crossIntegral_and_mixed: the phase-free integral of the summed pure-cross density — the bijection sum, before any permanent enlargement — carries the windowed value K^m·L^{m-1}.

Equations

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

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

Bracket-retaining fibre ledger (routed branch, m ≥ 2): every residual-refined contraction fibre term sum pays the windowed value m⁸·K^m·L^{m-1}, the endpoint loss ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴, and one central eighth-order bracket at the natural harvest scale ⟨ε‖freq(α+β)‖⟩⁻⁸. The m⁸ prices the pointwise product bracket over the 2m momentum-conserving covariance keys; the ⟨ε‖·‖⟩⁻⁸ normalization is the one produced by r324HdetAssembly_prod_eighthDecay_le applied to the half-symbol factors, and it dominates the frozen paper bracket by r324HdetAssembly_endpointLoss_mul_epsScale_le_paper.

Equations

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

Summation of the bracket ledger

theorem Anderson4D.r324HdetAssembly_pairingSum_le_of_bracketLedger {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324HdetBracketLedgerBound ρ K) (lam : ℝ) {ε : ℝ} {m : ℕ} (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hmtrunc : m ≤ truncOrder ε) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * (65536 * K) ^ m * lam ^ (2 * m - 2) * (r324EndpointLoss ε α β * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency (α + β)‖))

The bracket ledger sums to a pointwise bracket bound on the full signed pairing sum: signature and residual-schedule counting cost 4^{2m} each, the product-bracket price m⁸ is absorbed as m⁸ ≤ 256^m, and |λ_ε|^{2m}·L^{m-1} collapses to λ_ε²·λ^{2m-2} exactly.

Landing in the frozen deterministic right side

theorem Anderson4D.r324HdetAssembly_rhs_glue {value amplitude O P lam ε : ℝ} {m : ℕ} {α β : Z4} (h : value ≤ amplitude * min 1 (paperDeterministicMomentDecay ε α β)) (hamp : amplitude ≤ lamEps lam ε ^ 2 * O * (P * lam) ^ (2 * m - 2)) (hamp0 : 0 ≤ amplitude) : value ≤ deterministicMomentRHS O P lam ε m α β

Any amplitude dominated by the frozen shape lands the paper min bracket in deterministicMomentRHS, through paperDeterministicMomentDecay_le and min monotonicity.

theorem Anderson4D.r324HdetAssembly_paper_rhs_glue {value amplitude O P lam ε : ℝ} {m : ℕ} {α β : Z4} (h : value ≤ amplitude * min 1 (paperDeterministicMomentDecay ε α β)) (hamp : amplitude ≤ lamEps lam ε ^ 2 * O * (P * lam) ^ (2 * m - 2)) (hamp0 : 0 ≤ amplitude) : value ≤ paperDeterministicMomentRHS O P lam ε m α β

Strong landing lemma which keeps the exact Euclidean Japanese bracket printed in (3.24), without comparison to a sup-norm decay ledger.

theorem Anderson4D.r324HdetAssembly_exists_deterministicMoment_bound (ρ : SmoothCutoff) (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetCrossIntegralBound ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ 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 three analytic hypotheses. All constants are chosen by the cutoff before the coupling; the uniform branch is the injectivity-retaining closure, and the routed branch is the unconditional countable output at m = 1 and the summed bracket ledger at m ≥ 2.

The hdet hypothesis and the conditional main theorem

theorem Anderson4D.r324HdetAssembly_hdet (ρ : SmoothCutoff) (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetCrossIntegralBound ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ 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 mainConditional_of_deterministic_bounds, delivered from the three analytic hypotheses. The constants depend on the cutoff only and are fixed before the coupling; the scale hypotheses are discharged eventually along ε ↓ 0.

theorem Anderson4D.mainConditional_of_analyticResiduals {M : NoiseModel} {ρ : SmoothCutoff} (hcross : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetCrossIntegralBound ρ K) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : MainConditional M ρ

The conditional main theorem from the analytic residuals. The complete MainConditional M ρ follows from three analytic hypotheses:

• the injectivity-retaining cross-density integral bound (R324HdetCrossIntegralBound, uniform branch, m ≥ 3);
• the proved mixed-fibre ledger (R324LedgerThreeMixedLedger);
• the bracket-retaining fibre ledger (R324HdetBracketLedgerBound, routed branch, m ≥ 2).

The counterterm input is R322AnalyticResidualPrefix.exists_r322_renormC2q_bound; the order-one routed branch is unconditional.