ClauseOne

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

The clause-(i) assembly of the annular decomposition

ABK26, Section 4.1, the proof of p.mathcalE.annular.decomp, assembled end to end at the literal flux-corrected carrier Support.fluxCorrectedError.

The chain composed here is the manuscript's own:

  the (infinity,2) opening  e.mathcal.E.eight.ess.bound      (EightEss)
   -> the two J-sums (field leg + transposed leg)   (BlockResponse/DescendantLattice)
   -> the annular cover                             (Step1, IsAnnularDecompPre)
   -> the per-cube ugly estimate                    (UglyChain, IsUglyJEstimate)
   -> e.mathcalE.annular.decomp.pre.zero            (Resum.preZero_of_pre_and_ugly)
   -> the three Step-3 resummations                 (Step3Producers)
   -> e.mathcalE.annular.decomp                     (Step3.annularDecomp_of_preZero)

The two structural moves made explicit here

• The transposed leg. The manuscript discharges the second J-sum by asserting that "the right side of e.mathcalE.annular.decomp.pre.zero does not change if we replace the field with its transpose". Here the two legs are run through the same composite with the same five right-hand families, sig, L2f, gradNf, gradTailSq; each of the five terms is therefore literally the same expression for the two legs, and the assertion is reduced to its one genuine content, the transposed leg's per-cube ugly estimate.
• pre.zero's fourth term carries grad(k_L - k_{n-2}) while the Step-3 resummation display carries grad(k_m - k_{n-2}); the manuscript substitutes silently.

Part A -- the two arithmetic bridges of the opening

theorem Algsuperdiff.Section4.Provider.Annular.one_sub_three_rpow_neg_two_le {s : ℝ} (hs0 : 0 ≤ s) : 1 - 3 ^ (-(2 * s)) ≤ 4 * s

The c_{2s} discount is linear in s. 1 - 3^(-2s) <= 4 s for s >= 0, from 1 + y <= exp y and log 3 <= 2. This is what converts the normalizing factor c_{2s} of the (infinity,2) opening into the prefactor C s of the first conclusion term.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_guard_eq_tsum_shell (m : ℤ) (s : ℝ) (J : ℤ → ℝ) : (∑' (n : ℤ), if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * J n else 0) = ∑' (l : ℕ), 3 ^ (-(2 * s) * ↑l) * J (m - ↑l)

The scale-index bridge. The (infinity,2) opening sums over the depth l in N; every downstream module sums over the scale n <= m. Under n = m - l the two weighted sums agree.

Part B -- the m-vs-L tail routing

theorem Algsuperdiff.Section4.Provider.Annular.isUglyJEstimate_routeTail {Jval E2 sigDiff L2 gradN gradM cstar gam w wgam C Ktail : ℝ} (hC0 : 0 ≤ C) (hcstar0 : 0 ≤ cstar⁻¹) (hgam0 : 0 ≤ gam) (hE20 : 0 ≤ E2) (hsig0 : 0 ≤ sigDiff) (hL20 : 0 ≤ L2) (hgradN0 : 0 ≤ gradN) (hgradM0 : 0 ≤ gradM) (hKtail0 : 0 ≤ Ktail) (hw0 : 0 ≤ w) (hw : w ≤ wgam) (h : IsUglyJEstimate Jval E2 sigDiff L2 (gradN + Ktail * gradM) gradM cstar gam w wgam C) : IsUglyJEstimate Jval E2 sigDiff L2 gradN gradM cstar gam w wgam ((1 + Ktail) * C)

e.mathcalE.annular.decomp.pre.zero's fourth term carries the gradient of `k_L

• k_{n-2}while the Step-3 resummation display carries the gradient ofk_m - k_{n-2}; the manuscript substitutes one for the other without comment. Honestly k_L - k_{n-2} = (k_m - k_{n-2}) + (k_L - k_m), and the triangle inequality leaves a k > m` tail.

This lemma states the routing: if the per-cube estimate holds with the tail included in the fourth slot, at a tail budget Ktail * gradM proportional to the fifth term's own content, then it holds in the clean five-term shape at the constant (1 + Ktail) C. The move is available because on the annular region n <= j - 1 <= m - 1 the fifth term's weight w_gamma = 3^((s+gamma)(m-n)) dominates the fourth's w = 3^(s(m-n)), so the tail is absorbed by the term whose content is exactly the k >= m object.

Part C -- one leg of the opening, taken to the pre.zero shape

theorem Algsuperdiff.Section4.Provider.Annular.preZero_leg {s gamma cstar Cbf C₁ C₂ C gradM Ecal2 : ℝ} {m : ℤ} {Jleg : ℤ → ℝ} {Jann E2 L2f gradNf : ℤ → ℤ → ℝ} {sig : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hcstar : 0 < cstar) (hCbf : 0 ≤ Cbf) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hgradM : 0 ≤ gradM) (hJleg0 : ∀ (n : ℤ), 0 ≤ Jleg n) (hJann0 : ∀ (j n : ℤ), 0 ≤ Jann j n) (hE0 : ∀ (j n : ℤ), 0 ≤ E2 j n) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hL20 : ∀ (j n : ℤ), 0 ≤ L2f j n) (hgrad0 : ∀ (j n : ℤ), 0 ≤ gradNf j n) (hess : Ecal2 ≤ Cbf * (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(2 * s) * ↑l) * Jleg (m - ↑l)) (hpreA : IsAnnularDecompPre s m Jleg Jann C₁) (hugly : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → IsUglyJEstimate (Jann j n) (E2 j n) (sig n) (L2f j n) (gradNf j n) gradM cstar gamma (3 ^ (s * ↑(m - n))) (3 ^ ((s + gamma) * ↑(m - n))) C₂) (hsumE : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n)) (hsumS : Summable (annFam m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n)) (hsumL : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n)) (hsumG : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n)) (hCge : 24 * Cbf * C₁ * C₂ ≤ C) : Ecal2 ≤ ((((C * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) + C * s * annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n) + C * cstar⁻¹ * (s ^ 2)⁻¹ * gamma * gradM

One leg of the opening, taken to the pre.zero shape.

Given

• hess -- the leg's contribution to the (infinity,2) opening, in the shape eightEss_of_blockResponse_le produces it;
• hpreA -- the Step-1 annular cover at the leg's grid family;
• hugly -- the per-cube ugly estimate at the manuscript's weights;
• the four summability facts of preZero_of_pre_and_ugly,

the leg satisfies the five-term e.mathcalE.annular.decomp.pre.zero shape. The work done here beyond preZero_of_pre_and_ugly is the conversion of the c_{2s} prefactor into 4 Cbf s and the scale-index bridge.

Part D -- the four-term shape with separated constants

The Step-3 four-term shape carries ONE constant across all four right-hand terms.

def Algsuperdiff.Section4.Provider.Annular.IsClauseOneBound (Ecal2 G2 Rem G1a G1b s cstar gamma C : ℝ) : Prop

Ecal2 <= C s G2 + C s^(-3) cstar^(-4) Rem
         + C s^(-2) cstar^(-1) gamma G1a + C s^(-2) cstar^(-1) gamma G1b .

A naming convenience inside this provider module; it is not a source-facing declaration and closes no node.

Equations

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

theorem Algsuperdiff.Section4.Provider.Annular.clauseOneBound_of_preZero {Ecal2 G2raw SigSum GradSum L2Sum Gm Rem G1a G1b s cstar gamma D Csig Cgrad CL2 C : ℝ} (hs0 : 0 < s) (hcstar : 0 < cstar) (hgamma : 0 ≤ gamma) (hD : 0 ≤ D) (hG2raw : 0 ≤ G2raw) (hRem : 0 ≤ Rem) (hG1a0 : 0 ≤ G1a) (hG1b0 : 0 ≤ G1b) (hpre : Ecal2 ≤ D * s * G2raw + D * s * SigSum + D * cstar⁻¹ * gamma * s * GradSum + D * cstar⁻¹ * gamma * s * L2Sum + D * cstar⁻¹ * (s ^ 2)⁻¹ * gamma * Gm) (hsig : SigSum ≤ Csig * s⁻¹ * (s ^ 3)⁻¹ * (cstar ^ 4)⁻¹ * Rem) (hgrad : GradSum ≤ Cgrad * (s ^ 3)⁻¹ * G1b) (hL2 : L2Sum ≤ CL2 * (s ^ 3)⁻¹ * G1b) (hGm : Gm ≤ G1a) (hC1 : D ≤ C) (hC2 : D * Csig ≤ C) (hC3 : D * (Cgrad + CL2) ≤ C) : IsClauseOneBound Ecal2 G2raw Rem G1a G1b s cstar gamma C

The Step-3 regrouping at separated constants. The regrouping in which the sigma-bar slot's extra s^(-1) is carried by the second term's exponent rather than by the shared constant, so the output constant is s-free.

Part D' -- the two legs and the Step-3 regrouping

theorem Algsuperdiff.Section4.Provider.Annular.clauseOneBound_of_legs {s gamma cstar C Cshom Kl2 Kgn Cout gradM Ecal2 Ecal2f Ecal2t : ℝ} {m : ℤ} {E2 L2f gradNf : ℤ → ℤ → ℝ} {sig A : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hcstar0 : 0 < cstar) (hcstar4 : cstar ^ 4 ≤ 6) (hlog : 1 ≤ |Real.log gamma|) (hC0 : 0 ≤ C) (hKl2 : 0 ≤ Kl2) (hKgn : 0 ≤ Kgn) (hgradM : 0 ≤ gradM) (hE0 : ∀ (j n : ℤ), 0 ≤ E2 j n) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hL20 : ∀ (j n : ℤ), 0 ≤ L2f j n) (hgrad0 : ∀ (j n : ℤ), 0 ≤ gradNf j n) (hsplit : Ecal2 ≤ Ecal2f + Ecal2t) (hlegf : Ecal2f ≤ ((((C * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) + C * s * annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n) + C * cstar⁻¹ * (s ^ 2)⁻¹ * gamma * gradM) (hlegt : Ecal2t ≤ ((((C * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) + C * s * annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n) + C * cstar⁻¹ * gamma * s * annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n) + C * cstar⁻¹ * (s ^ 2)⁻¹ * gamma * gradM) (hshom : ∀ n ≤ m - 1, sig n ≤ (Cshom * gamma * ↑(m - n) + Cshom * (2 * gamma + (cstar ^ 2)⁻¹ * (gamma * |Real.log gamma| ^ 2))) ^ 2 * 3 ^ (2 * gamma * ↑(m - n))) (hAsum : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) (hcsL2 : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → L2f j n ≤ Kl2 * (↑(m - n) + 2) * 3 ^ (2 * gamma * ↑(m - n)) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) (hcsGn : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → gradNf j n ≤ Kgn * (↑(m - n) + 2) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) (hCout1 : 2 * C ≤ Cout) (hCout2 : 2 * C * (7000 * Cshom ^ 2) ≤ Cout) (hCout3 : 2 * C * (4608 * Kl2 + 576 * Kgn) ≤ Cout) : IsClauseOneBound Ecal2 (annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) (gamma ^ 2 * |Real.log gamma| ^ 4) gradM (∑' (v : ℕ), 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) s cstar gamma Cout

The two-leg Step-3 regrouping.

The field leg and the transposed leg are both taken to the five-term pre.zero shape at the same five right-hand families; adding them doubles the constant and nothing else. This is the machine-visible content of the manuscript's transpose remark: each of the five right-hand terms is literally the same expression for the two legs, so "the right side does not change" is not a claim about the terms at all -- its whole content is that the transposed leg admits the same per-cube ugly estimate, which is the caller's hlegt.

The three Step-3 resummations are then discharged from their comparison inputs (hshom, hcsL2, hcsGn) and the regrouping is clauseOneBound_of_preZero.

Part E -- the composite at the flux-corrected carrier

noncomputable def Algsuperdiff.Section4.Provider.Annular.gradTailSq {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

gradTailSq M m omega = ( sum_{k >= m} 3^((2-gamma) m) ‖grad j_k‖_{W^{1,infinity}(Box_m)} )^2 .

The square is outside the sum; the printed display puts it inside, and the inside-square variant cannot dominate the fifth pre.zero term.

Equations

• Algsuperdiff.Section4.Provider.Annular.gradTailSq M m omega = (∑' (k : { k : ℤ // m ≤ k }), 3 ^ ((2 - M.gamma) * ↑m) * Algsuperdiff.Section4.Support.shellW1InfGradNorm m (↑omega ↑k)) ^ 2

theorem Algsuperdiff.Section4.Provider.Annular.gradTailSq_nonneg {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ gradTailSq M m omega

theorem Algsuperdiff.Section4.Provider.Annular.clauseOne_bound {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hsg : 8 * M.gamma ≤ s) (omega : Section3.Cutoff.CutoffSample d) {Jlegf Jlegt : ℤ → ℝ} {Jannf Jannt E2 L2f gradNf : ℤ → ℤ → ℝ} {sig A : ℤ → ℝ} {Cbf C₁ C₂ Cleg Cshom Kl2 Kgn Ktail Cout : ℝ} (hCbf : 0 ≤ Cbf) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hKl2 : 0 ≤ Kl2) (hKgn : 0 ≤ Kgn) (hKtail : 0 ≤ Ktail) (hJf0 : ∀ (n : ℤ), 0 ≤ Jlegf n) (hJt0 : ∀ (n : ℤ), 0 ≤ Jlegt n) (hJannf0 : ∀ (j n : ℤ), 0 ≤ Jannf j n) (hJannt0 : ∀ (j n : ℤ), 0 ≤ Jannt j n) (hE0 : ∀ (j n : ℤ), 0 ≤ E2 j n) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hL20 : ∀ (j n : ℤ), 0 ≤ L2f j n) (hgrad0 : ∀ (j n : ℤ), 0 ≤ gradNf j n) (hbfJ : ∀ (l : ℕ), HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) (m - ↑l) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m)) ≤ Cbf * (Jlegf (m - ↑l) + Jlegt (m - ↑l))) (hsumFl : Summable fun (l : ℕ) => 3 ^ (-(2 * s) * ↑l) * Jlegf (m - ↑l)) (hsumTl : Summable fun (l : ℕ) => 3 ^ (-(2 * s) * ↑l) * Jlegt (m - ↑l)) (hpref : IsAnnularDecompPre s m Jlegf Jannf C₁) (hpret : IsAnnularDecompPre s m Jlegt Jannt C₁) (huglyf : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → IsUglyJEstimate (Jannf j n) (E2 j n) (sig n) (L2f j n) (gradNf j n + Ktail * 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) (E2 j n) (sig n) (L2f j n) (gradNf j n + Ktail * 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₂) (hsumE : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n)) (hsumS : Summable (annFam m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n)) (hsumL : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n)) (hsumG : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n)) (hcstar4 : Section3.Disorder.cstar M ^ 4 ≤ 6) (hlog : 1 ≤ |Real.log M.gamma|) (hshom : ∀ n ≤ m - 1, sig n ≤ (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))) (hAsum : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) (hcsL2 : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → L2f j n ≤ Kl2 * (↑(m - n) + 2) * 3 ^ (2 * M.gamma * ↑(m - n)) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) (hcsGn : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → gradNf j n ≤ Kgn * (↑(m - n) + 2) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) (hCleg : 24 * Cbf * C₁ * ((1 + Ktail) * C₂) ≤ Cleg) (hCout1 : 2 * Cleg ≤ Cout) (hCout2 : 2 * Cleg * (7000 * Cshom ^ 2) ≤ Cout) (hCout3 : 2 * Cleg * (4608 * Kl2 + 576 * Kgn) ≤ Cout) : IsClauseOneBound (Support.fluxCorrectedError M L m s omega ^ 2) (annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * E2 j n) (M.gamma ^ 2 * |Real.log M.gamma| ^ 4) (gradTailSq M m omega) (∑' (v : ℕ), 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) s (Section3.Disorder.cstar M) M.gamma Cout

The clause-(i) composite at the literal flux-corrected carrier.

• hbfJ -- the e.bfJ.general conversion of the depth-l descendant maximum of the normalized block response into the two lattice J-maxima (A4a proves it at the constant 1; the manuscript's C >= 1 is carried here);
• hpref / hpret -- the Step-1 annular cover at the two legs;
• huglyf / huglyt -- the per-cube ugly estimate at the lattice cube z + Box_n, with the k > m tail included in the fourth slot (the honest m-vs-L reading; isUglyJEstimate_routeTail moves it to the fifth term);
• hshom -- e.shom.m.vs.shom.n in the manuscript's own shape;
• hcsL2 / hcsGn -- the two Step-3 cube comparisons;
• the summability facts, and the constant inequalities.

The conclusion is the four-term shape at the concrete left-hand carrier, the concrete G_1^a content gradTailSq, and the concrete remainder gamma^2 |log gamma|^4.

theorem Algsuperdiff.Section4.Provider.Annular.hbfJ_of_lattice_bounds {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {Jlegf Jlegt : ℤ → ℝ} {Cbf : ℝ} (hCbf : 1 ≤ Cbf) (hJf0 : ∀ (n : ℤ), 0 ≤ Jlegf n) (hJt0 : ∀ (n : ℤ), 0 ≤ Jlegt n) (hfld : ∀ (l : ℕ), ∀ v ∈ Support.latticeCubeSet d (m - ↑l) m, ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube (m - ↑l) v)) ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube (m - ↑l) v)) (Section3.Observable.inverseSqrtLoad (Section3.Annealed.sigmaBar M m) e) (Section3.Observable.sqrtLoad (Section3.Annealed.sigmaBar M m) e) ≤ Jlegf (m - ↑l)) (htrn : ∀ (l : ℕ), ∀ v ∈ Support.latticeCubeSet d (m - ↑l) m, ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube (m - ↑l) v)) ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube (m - ↑l) v)).transpose (Section3.Observable.inverseSqrtLoad (Section3.Annealed.sigmaBar M m) e) (Section3.Observable.sqrtLoad (Section3.Annealed.sigmaBar M m) e) ≤ Jlegt (m - ↑l)) (l : ℕ) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (HCPolySupport.originCube d m) (m - ↑l) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m)) ≤ Cbf * (Jlegf (m - ↑l) + Jlegt (m - ↑l))

The e.bfJ.general slot at the manuscript's constant C >= 1, from A4a's C = 1 producer: a bound on the two lattice J-maxima, for the field and for its transpose, at every depth.