ClauseOneFinal

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

The clause-(i) endpoint with huglyf stitched in

The clause-(i) endpoint at the honest event reduces to the four slots hpref, hpret, huglyf, huglyt at 𝒢₀(m) ∩ 𝒢₁(m; s, √c⋆ γ^{−1/2}). FinalStitch produces the huglyf slot from the lattice chain, at the annulus family annularResponseMax. This module runs the composition, so that the endpoint's remaining inputs are

• hpref, hpret, huglyt — three hypotheses left as binders, unchanged; and
• hlam, hsignlow — the two obligations FinalStitch does not discharge (at the relaxed constant ¼; see FinalStitch and SigmaBarBudget). SignLowDischarge removes hsignlow from this list.

Three differences from the un-stitched composite, all forced by the producer:

1. K_tail = 2 and gradNf = 2 · annularGradBlock (so K_gn = 162). The lattice chain's fourth slot is the gauge of the whole increment k_L − k_{n−2}, and splitting it at m costs (X+Y)² ≤ 2X² + 2Y²; no choice of K_tail makes the coefficient of annularGradBlock equal to 1. The output constant is unaffected: clauseOneOutConstant C₁ C_shom still dominates 2 C_leg (4608 K_l2 + 576 K_gn) because C_shom ≥ 6.
2. Jannf is pinned to annularResponseMax, so hpref becomes a comparison of jLegField with a family of the same shape (a lattice maximum of scalarResponseMax).
3. The (2,2) slot is bridged from the literal atom to the measurable observable by annularErrorAtomMax_ae_le_annularErrorLatticeMax, one a.e. step at the display level — which is where the display already lives.

Part A -- the atom-to-observable bridge for the (2,2) slot

theorem Algsuperdiff.Section4.Provider.Annular.annularErrorAtomMax_ae_le_annularErrorLatticeMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (j n : ℤ), n ≤ j - 1 → annularErrorAtomMax M (↑s) omega j n ≤ annularErrorLatticeMax M s omega j n

The reconciliation. The annulus maximum of the literal (2,2) error atom is almost surely below the annulus maximum of the measurable observable — indeed the two agree a.s. The null set is the representative-choice set of the 𝒢₂ lane, taken over the countable family of scales and lattice indices.

Part B -- the summability of the doubled gradient family

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_two_annularGradBlock_of_eventG1 {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {s T : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hT : 0 ≤ T) {omega : Section3.Cutoff.CutoffSample d} (homega : omega ∈ Support.eventG1 M m s T) : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * (2 * annularGradBlock M m omega j n))

The hsumG binder at the doubled head-block gradient family.

Part C -- the clause-(i) composite at the lattice-chain pinning

theorem Algsuperdiff.Section4.Provider.Annular.clauseOne_bound_final {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) (hs1 : ↑s ≤ 1) (hsg : 8 * M.gamma ≤ ↑s) (hcstar4 : Section3.Disorder.cstar M ^ 4 ≤ 6) (hlog : 1 ≤ |Real.log M.gamma|) (hG1 : omega ∈ Support.eventG1 M m (↑s) (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)) (hsumE : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(↑s * ↑(m - n))) * annularErrorLatticeMax M s omega j n)) {Cshom : ℝ} (hCshom : 6 ≤ Cshom) (hshom : ∀ n ≤ m - 1, (↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ - 1) ^ 2 ≤ (Cshom * M.gamma * ↑(m - n) + Cshom * (2 * M.gamma + (Section3.Disorder.cstar M ^ 2)⁻¹ * (M.gamma * |Real.log M.gamma| ^ 2))) ^ 2 * 3 ^ (2 * M.gamma * ↑(m - n))) {Jannt : ℤ → ℤ → ℝ} {C₁ C : ℝ} (hC₁ : 0 ≤ C₁) (hC0 : 0 ≤ C) (hJannt0 : ∀ (j n : ℤ), 0 ≤ Jannt j n) (hpref : IsAnnularDecompPre (↑s) m (jLegField M L m omega) (annularResponseMax M L m omega) C₁) (hpret : IsAnnularDecompPre (↑s) m (jLegTranspose M L m omega) Jannt C₁) (huglyf : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → IsUglyJEstimate (annularResponseMax M L m omega j n) (annularErrorLatticeMax M s omega j n) ((↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ - 1) ^ 2) (annularL2Block M m omega j n) (2 * annularGradBlock M m omega j n + 2 * gradTailSq M m omega) (gradTailSq M m omega) (Section3.Disorder.cstar M) M.gamma (3 ^ (↑s * ↑(m - n))) (3 ^ ((↑s + M.gamma) * ↑(m - n))) C) (huglyt : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → IsUglyJEstimate (Jannt j n) (annularErrorLatticeMax M s omega j n) ((↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ - 1) ^ 2) (annularL2Block M m omega j n) (2 * annularGradBlock M m omega j n + 2 * gradTailSq M m omega) (gradTailSq M m omega) (Section3.Disorder.cstar M) M.gamma (3 ^ (↑s * ↑(m - n))) (3 ^ ((↑s + M.gamma) * ↑(m - n))) C) : IsClauseOneBound (Support.fluxCorrectedError M L m (↑s) omega ^ 2) (annDouble m fun (j n : ℤ) => 3 ^ (-(↑s * ↑(m - n))) * annularErrorLatticeMax M s omega j n) (M.gamma ^ 2 * |Real.log M.gamma| ^ 4) (gradTailSq M m omega) (∑' (v : ℕ), 3 ^ (-(↑s / 2) * ↑v) * shellBlockLatticeReal M m omega (m - ↑v) ^ 2) (↑s) (Section3.Disorder.cstar M) M.gamma (clauseOneOutConstant C₁ C 2 Cshom)

The clause-(i) composite with Jannf pinned and K_tail = 2. This is the honest-event clause-(i) composite re-run at the pinning the lattice chain produces: gradNf = 2 · annularGradBlock, K_gn = 162, K_tail = 2, Jannf = annularResponseMax. The output constant is the same clauseOneOutConstant.