LambdaDischarge

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

The hlam slot discharged, and the one-slot clause-(i) endpoint

ABK26, Section 4.1, p.mathcalE.annular.decomp Step 2.

LambdaBudget.sigmaBar_mul_inv_unitCubeLambda_two_gamma_le_of_mem_eventG0 proves the ugly chain's λ-budget outright, on 𝒢₀(m) and at the gapped gauge s = 2γ, at the explicit constant

C_l = annularLambdaConstant d C_cg = 8 (1 + 9^d) (1 + C_cg) .

This module feeds it into the endpoint. exists_clauseOne_final_one is the transposed clause-(i) endpoint with the hlam binder gone and C_l pinned to that constant: its remaining mathematical input is exactly hpref, the Step-1 leg.

N-invariance

hlam is consumed at ω and at Nω = −ω. The discharge respects that with no extra work and introduces no sub-event: it consumes only

• membership in 𝒢₀(m) itself, which is pointwise N-invariant (mem_eventG0_negateCutoffSample_iff), and
• deterministic triadic geometry plus the induction state, neither of which sees the sample at all.

So the same lemma applies verbatim at Nω via hmemN, and the transposed leg below does exactly that.

Why the endpoint is re-run rather than composed

The endpoint cannot be composed on top of its predecessor: the induction state that discharges hlam is produced inside the predecessor's proof from a constant C₀ of an ∃-package whose C_shom is opaque from outside. The proof below is therefore the same composition re-run with the slot filled in place — a forced re-derivation, not new mathematics. The display, the ranges, the event, the s-scaling and clauseOneOutConstant C₁ C_shom are unchanged.

theorem Algsuperdiff.Section4.Provider.Annular.exists_clauseOne_final_one (d : ℕ) (dimension : 2 ≤ d) : ∃ (Cs : ℝ) (Cshom : ℝ), 0 < Cs ∧ 6 ≤ Cshom ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ (Cshom ^ 10)⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ (Ccg : ℝ), 0 ≤ Ccg → ∀ (m : ℤ) (s : { s : ℝ // 0 < s }), ↑s ≤ 1 / 4 → 8 * M.gamma ≤ ↑s → Section3.Disorder.cstar M ^ 4 ≤ 6 → 1 ≤ |Real.log M.gamma| → ∀ (C₁ C : ℝ), 0 < C₁ → 0 < C → Cs * (1 + 196 * annularLambdaConstant d Ccg) ^ 2 * 4 * (1 + annularLambdaConstant d Ccg) + 16 * Cs * (1 + 196 * annularLambdaConstant d Ccg) ^ 2 * annularLambdaConstant d Ccg * (1 + Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst d ^ 2) + 4 * Cs * (1 + 4 * annularLambdaConstant d Ccg ^ 2) ≤ C → (∀ omega ∈ Support.eventG0 M Ccg 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₁) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (Support.eventG0 M Ccg m ∩ Support.eventG1 M m (↑s) (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)).indicator (Support.fluxCorrectedErrorObservableSqSup M m s) omega ≤ ENNReal.ofReal (clauseOneOutConstant C₁ C 2 Cshom * ↑s) * clauseOneTermOne M m s omega + ENNReal.ofReal (clauseOneOutConstant C₁ C 2 Cshom * (↑s)⁻¹ ^ 3 * (Section3.Disorder.cstar M)⁻¹ ^ 4 * M.gamma ^ 2 * |Real.log M.gamma| ^ 4) + ENNReal.ofReal (clauseOneOutConstant C₁ C 2 Cshom * (↑s)⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * clauseOneTermThree M m omega + ENNReal.ofReal (clauseOneOutConstant C₁ C 2 Cshom * (↑s)⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * clauseOneTermFour M m s omega

The clause-(i) endpoint at ONE remaining slot.

The transposed clause-(i) endpoint with hlam discharged by LambdaBudget.sigmaBar_mul_inv_unitCubeLambda_two_gamma_le_of_mem_eventG0 at C_l = annularLambdaConstant d C_cg = 8(1+9^d)(1+C_cg), so that the remaining inputs are exactly

• the printed ranges s ≤ 1/4, 8γ ≤ s, c⋆⁴ ≤ 6, 1 ≤ |log γ| and the standing regime γ ≤ C_shom^{−10} c⋆^{10};
• the typing nondegeneracies 0 ≤ C_cg, 0 < C₁, 0 < C and the constant inequality fixing C; and
• the single mathematical obligation hpref, the Step-1 leg.

Nothing else is assumed.