SealPackaging

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The annular decomposition packaged at ONE slot

LambdaDischarge.exists_clauseOne_final_one is the clause-(i) endpoint with a single mathematical slot left, hpref (the Step-1 leg). This module packages it: one theorem whose conclusion is the target shape -- one constant, both clauses conjoined inside one ∀ᵐ, on the printed ranges -- carrying hpref as its one hypothesis.

What packaging costs

1. The two clauses share one ∀ᵐ. The chain delivers clause (i) as an ∀ᵐ statement and clause (ii) as a consumer of that display at a fixed ε. A naïve ∀ ε, ∀ᵐ ω → ∀ᵐ ω, ∀ ε swap is false in general (uncountably many ε), so clauseTwo_pointwise_of_display below repeats the proved clause-(ii) route pointwise at a single sample: every ingredient of that route (goodEventBase_subset_annularEvent, ClauseTwo.clauseOneDisplayRhs_le_of_goodEventBase, ClauseTwo.indicator_observableSup_le_of_sqSup, ClauseTwo.sqrt_four_mul_sq) is already sample-wise, so the null set comes only from the ε-free clause-(i) display and the ε-quantifier goes inside it.
2. One constant for both clauses and both regime gates. The endpoint produces the clause-(i) display at C_out = clauseOneOutConstant C₁ C_b 2 C_shom, clause (ii) at 2√C_out, and gates the regime at C_shom^10; the carried hpref gates its own regime at C_reg. The packaged constant is C_fin = max C_out (max (2√C_out) (max (C_shom^10) C_reg)); clause (i) rises to it by ClauseTwo.clauseOneDisplayRhs_mono, clause (ii) by monotonicity of ε ↦ Cε, and the regime hypothesis at the larger C_fin is stronger than either gate, so it implies both (inv_anti₀).
3. Three ranges the target does not carry are discharged, not assumed: c⋆⁴ ≤ 6 from Section3.Provider.Disorder.cstar_le_three_halves ((3/2)⁴ = 81/16 ≤ 6); 1 ≤ |log γ| from the standing M.shellPrefix.gamma_le_quarter and gamma_pos; and 0 ≤ C_cg from Support.cgEllipLowerConstant_pos. The ε-side range sε ≤ 1 needed by the event containment is s ≤ 1/4, ε ≤ 1/2.
4. Dimension. The endpoint needs 2 ≤ d; the target quantifies over all d. For d ≤ 1 the statement is vacuous, because ABKModel d bundles M.shellPrefix.dimension : 2 ≤ d -- the same split the Section 3 asymptotics anchor uses. The whole split stays inside this theorem: hpref is itself carried under 2 ≤ d, so a producer that needs the dimension (every producer on these carriers does) discharges the hypothesis directly and the low-dimensional branch never asks for it.

Why hpref is carried gated

The Step-1 leg is a statement about the manuscript's own regime: it is claimed for s ∈ [8γ, 1/4], under a smallness gate on γ, on 𝒢₀ ∩ 𝒢₁, for L ≥ m. Carrying it range-free would be carrying a stronger proposition than the manuscript asserts -- an obligation that may well be false as stated and could then never be discharged. So the hypothesis below quantifies its own regime constant C_reg and takes the two printed range clauses; every one of those gates is available at the point of use, so nothing is lost, and a range-free hpref (if one is ever proved) discharges this one by dropping the gates. Note the two facts c⋆⁴ ≤ 6 and 1 ≤ |log γ| are not gates of hpref: they are standing consequences of c⋆ ≤ 3/2 and γ ≤ 1/4, discharged in Part A.

The frozen event at y = 0

Clause (ii) is stated on the frozen goodEventAt M C_cg m 0 s ε, which is by definition Cutoff.translateCutoffSample 0 ⁻¹' Support.goodEventBase …; the proved GoodEvents.Api.goodEventAt_eq_preimage and ClauseTwo.goodEventBase_eq_translateZero_preimage identify it with Support.goodEventBase M C_cg m s ε, which is the event the chain carries. Only the frozen definition module Frozen.Section4.GoodEvents enters (through the proved Provider.GoodEvents.Api, exactly as Proportion.ProportionFinal does); no frozen theorem module is imported.

Part A -- the three discharged ranges

Part B -- clause (ii) at a single sample

Part C -- the packaged statement

theorem Algsuperdiff.Section4.Provider.Annular.annular_decomposition_of_hpref (d : ℕ) (hpref : 2 ≤ d → ∃ (C₁ : ℝ) (Creg : ℝ), 0 < C₁ ∧ 0 < Creg ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ Creg⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ (m : ℤ) (s : { s : ℝ // 0 < s }), ↑s ≤ 1 / 4 → 8 * M.gamma ≤ ↑s → ∀ omega ∈ Support.eventG0 M (Support.cgEllipLowerConstant d) m ∩ Support.eventG1 M m (↑s) (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹), ∀ (L : ℤ), m ≤ L → IsAnnularDecompPre (↑s) m (jLegField M L m omega) (annularResponseMax M L m omega) C₁) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ s ∈ Set.Icc (8 * M.gamma) (1 / 4), ∀ (hs : 0 < s) (m : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (Support.eventG0 M (Support.cgEllipLowerConstant d) m ∩ Support.eventG1 M m s (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSqSup M m ⟨s, hs⟩ omega') omega ≤ (ENNReal.ofReal (C * s) * ∑' (j : { j : ℤ // j ≤ m }) (n : { n : ℤ // n ≤ ↑j - 1 }), ENNReal.ofReal (Real.rpow 3 (-s * ↑(m - ↑n))) * ⨆ (v : ↑(Support.latticeAnnulusSet d (↑n) (↑j) (↑j - 1))), ENNReal.ofReal (Support.annularErrorObservable M ↑n ⟨s, hs⟩ (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint ↑n ↑v) omega) ^ 2)) + ENNReal.ofReal (C * s⁻¹ ^ 3 * (Section3.Disorder.cstar M)⁻¹ ^ 4 * M.gamma ^ 2 * |Real.log M.gamma| ^ 4) + ENNReal.ofReal (C * s⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * (∑' (k : { k : ℤ // m ≤ k }), ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k))) ^ 2 + ENNReal.ofReal (C * s⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * ∑' (n : { n : ℤ // n ≤ m }), ENNReal.ofReal (Real.rpow 3 (-(1 / 2) * s * ↑(m - ↑n))) * ∑ k ∈ Finset.Icc (↑n - 1) m, (ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑k)) * ⨆ (v : ↑(Support.latticeCubeSet d k m)), ENNReal.ofReal (Support.shellW2InfNormAt (Support.triadicLatticePoint k ↑v) k (↑omega k))) ^ 2 ∧ ∀ ep ∈ Set.Ioc 0 (1 / 2), M.gamma * |Real.log M.gamma| ^ 2 ≤ s.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * ep → (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) m 0 ⟨s, hs⟩ ep).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M m ⟨s, hs⟩ omega') omega ≤ ENNReal.ofReal (C * ep)

The annular decomposition, packaged at ONE slot.

The single hypothesis is hpref -- the Step-1 leg, at one constant C₁ > 0 uniform in (M, m, s, ω, L), at the coarse-ellipticity constant the target itself names, under 2 ≤ d, and gated exactly as the manuscript gates it: its own regime constant C_reg, the printed ranges s ≤ 1/4 and 8γ ≤ s, the event 𝒢₀ ∩ 𝒢₁, and L ≥ m. It is an explicitly documented conditional A obligation, not a source premise. The three further facts the endpoint carries (c⋆⁴ ≤ 6, 1 ≤ |log γ|, 0 ≤ C_cg) are discharged here from standing facts, and nothing else is assumed.

Disclosure: a proved local Provider helper.