AssemblyFeed

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

The assembly feed of the clause-(i) composite

ClauseOne.clauseOne_bound (ABK26, Section 4.1) carries seven summability binders, two J-leg families and the e.bfJ.general slot hbfJ. This module supplies the mechanical half of that feed:

• Part A -- the polynomial-absorption layer. 1 + x <= 3^x is the single transcendental input; everything above it is linarith only on abstract reals. The two consumers are linear_le_threeRpow and sq_linear_le_threeRpow, which convert the annulus multiplicity (m-n)+2 (and its square, from the sigma-bar continuity term) into an arbitrarily small power of the triadic weight.
• Part B -- the summability criteria for the guarded annular family Resum.annFam. summable_annFam_of_le is the raw geometric comparison; summable_annFam_of_poly_le is the polynomial-times-geometric form; the three named producers summable_annFam_sig, summable_annFam_grad and summable_annFam_l2 are the hsumS, hsumG and hsumL binders of clauseOne_bound, each derived from the binder that sits next to it in the same theorem (hshom, hcsGn, hcsL2) plus one partial-sum budget for the shell family. No probabilistic input enters Part B.
• Part C -- the two lattice J-maxima, and the hbfJ discharge. jLegField and jLegTranspose -- the Jlegf and Jlegt families of clauseOne_bound -- are defined as the 0-floored lattice maxima max_{z in 3^n Z^d cap cu_m} max_{|e|=1} J(z + cu_n;.), for the field and for its transpose. The inner maximum over the unit sphere is an honest sSup: it is bounded above because the scalar response at the normalized loading is one of the block response values (the Section 2.4 bridge for the field leg, BlockResponse's mirror for the transpose leg), so no junk value can enter. hbfJ_latticeMax is then A4a's producer at these carriers, and summable_jLegField / summable_jLegTranspose are the hsumFl / hsumTl binders -- unconditional: CoarseGraining's maxDescendantNormalizedBlockResponseAtScale_le_uniform bounds every scale by one cube-cu_m ellipticity constant, so the two J-sums are dominated by a bare geometric series.

Part A -- polynomial absorption into the triadic weight

theorem Algsuperdiff.Section4.Provider.Annular.one_add_le_threeRpow {x : ℝ} (hx : 0 ≤ x) : 1 + x ≤ 3 ^ x

1 + x <= 3^x for x >= 0. The one transcendental input of the polynomial-absorption layer: exp y >= 1 + y together with log 3 >= 1.

theorem Algsuperdiff.Section4.Provider.Annular.linear_le_threeRpow {c q : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hq : 0 ≤ q) : q + 2 ≤ 2 / c * 3 ^ (c * q)

The annulus multiplicity is absorbed by an arbitrarily small power of the triadic weight: q + 2 <= 2 c^(-1) 3^(c q) for q >= 0 and c in (0,1].

theorem Algsuperdiff.Section4.Provider.Annular.sq_linear_le_threeRpow {c q : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hq : 0 ≤ q) : (q + 2) ^ 2 ≤ (4 / c) ^ 2 * 3 ^ (c * q)

The squared form of linear_le_threeRpow.

Part B -- summability of the guarded annular families

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_of_le {m : ℤ} {h : ℤ → ℤ → ℝ} {K c : ℝ} (hc0 : 0 < c) (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hle : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → h j n ≤ K * 3 ^ (-(c * ↑(m - n)))) : Summable (annFam m h)

The geometric comparison. A nonnegative guarded annular family dominated on its region by K 3^(-c(m-n)) is summable.

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_of_poly_le {m : ℤ} {h : ℤ → ℤ → ℝ} {K b c : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hK0 : 0 ≤ K) (hbc : b + 2 * c ≤ 0) (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hle : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → h j n ≤ K * (↑(m - n) + 2) ^ 2 * 3 ^ (b * ↑(m - n))) : Summable (annFam m h)

The polynomial-times-geometric comparison. If the family is dominated by K ((m-n)+2)^2 3^(b(m-n)) with b + 2c <= 0 for some c in (0,1], it is summable: the square of the annulus multiplicity costs only 3^(c(m-n)).

The three named producers

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_sig {m : ℤ} {s gamma a B : ℝ} {sig : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hg0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (ha0 : 0 ≤ a) (hB0 : 0 ≤ B) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hshom : ∀ n ≤ m - 1, sig n ≤ (a * ↑(m - n) + B) ^ 2 * 3 ^ (2 * gamma * ↑(m - n))) : Summable (annFam m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n)

The hsumS binder. The sigma-bar continuity family is summable over the annular region: the hshom bound of clauseOne_bound is (a(m-n)+B)^2 3^{2 gamma (m-n)}, and 8 gamma <= s leaves the honest decay 3^{-(3/4)s(m-n)} after the weight.

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_grad {m : ℤ} {s Kgn Ksh : ℝ} {gradNf : ℤ → ℤ → ℝ} {A : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hKgn : 0 ≤ Kgn) (hKsh : 0 ≤ Ksh) (hgrad0 : ∀ (j n : ℤ), 0 ≤ gradNf j n) (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) (hpart : ∀ n ≤ m, ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2 ≤ Ksh * 3 ^ (s / 4 * ↑(m - n))) : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * gradNf j n)

The hsumG binder. From the hcsGn slot of clauseOne_bound and a partial-sum budget Ksh 3^{(s/4)(m-n)} for the shell family.

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_l2 {m : ℤ} {s gamma Kl2 Ksh : ℝ} {L2f : ℤ → ℤ → ℝ} {A : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hsg : 8 * gamma ≤ s) (hKl2 : 0 ≤ Kl2) (hKsh : 0 ≤ Ksh) (hL20 : ∀ (j n : ℤ), 0 ≤ L2f j n) (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) (hpart : ∀ n ≤ m, ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2 ≤ Ksh * 3 ^ (s / 4 * ↑(m - n))) : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * L2f j n)

The hsumL binder. From the hcsL2 slot of clauseOne_bound and the same partial-sum budget; the extra 3^{2 gamma (m-n)} of the value leg is absorbed by 8 gamma <= s.

Part C -- the two lattice J-maxima and the hbfJ discharge

def Algsuperdiff.Section4.Provider.Annular.scalarResponseSet {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (sigma : Section3.Observable.PositiveScalar) : Set ℝ

The value set of the scalar response of one cube at the normalized unit loadings (sigma^{-1/2} e, sigma^{1/2} e), |e| = 1 -- the quantity the manuscript's J-maxima are taken over.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Annular.scalarResponseMax {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (sigma : Section3.Observable.PositiveScalar) : ℝ

The one-cube scalar response maximum. It is an honest supremum: the value set is bounded above at every cube of a triadic family, because each of its elements is one of the block response values (scalarResponseSet_bddAbove below).

Equations

• Algsuperdiff.Section4.Provider.Annular.scalarResponseMax a sigma = sSup (Algsuperdiff.Section4.Provider.Annular.scalarResponseSet a sigma)

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseMax_eq_of_coeffOn_aeeq {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a b : HCPolySupport.Book.Ch02.CoeffOn U} (h : a.AEEq b) (sigma : Section3.Observable.PositiveScalar) : scalarResponseMax a sigma = scalarResponseMax b sigma

The scalar response maximum only sees the coefficient a.e. Every element of scalarResponseSet is a responseJ value, and Ch02.responseJ_eq_ofAEEq identifies those; the two value sets are therefore equal, hence so are their suprema.

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseSet_bddAbove {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) (sigma : Section3.Observable.PositiveScalar) : BddAbove (scalarResponseSet (F.coeffOn R) sigma)

The field-leg value set is bounded above, by the Section 2.4 normalized loading bridge.

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseSet_transpose_bddAbove {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) (sigma : Section3.Observable.PositiveScalar) : BddAbove (scalarResponseSet (F.coeffOn R).transpose sigma)

The transpose-leg value set is bounded above, by BlockResponse's mirror of the same bridge.

theorem Algsuperdiff.Section4.Provider.Annular.responseJ_le_scalarResponseMax {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) (sigma : Section3.Observable.PositiveScalar) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Section3.Observable.inverseSqrtLoad sigma e) (Section3.Observable.sqrtLoad sigma e) ≤ scalarResponseMax (F.coeffOn R) sigma

theorem Algsuperdiff.Section4.Provider.Annular.responseJ_transpose_le_scalarResponseMax {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) (sigma : Section3.Observable.PositiveScalar) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R).transpose (Section3.Observable.inverseSqrtLoad sigma e) (Section3.Observable.sqrtLoad sigma e) ≤ scalarResponseMax (F.coeffOn R).transpose sigma

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseMax_le_normalizedBlockResponseMax {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) (sigma : Section3.Observable.PositiveScalar) : scalarResponseMax (F.coeffOn R) sigma ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F (Section3.Observable.isotropicComparatorMatrix sigma)

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseMax_transpose_le_normalizedBlockResponseMax {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) (sigma : Section3.Observable.PositiveScalar) : scalarResponseMax (F.coeffOn R).transpose sigma ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F (Section3.Observable.isotropicComparatorMatrix sigma)

The two lattice maxima

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

The field J-maximum of the manuscript's lattice enumeration: max_{z in 3^n Z^d cap cu_m} max_{|e|=1} J(z + cu_n, a; sigma^{-1/2} e, sigma^{1/2} e), 0-floored (which changes nothing -- the entries are nonnegative responses).

Equations

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

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

The transposed-leg J-maximum.

Equations

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

theorem Algsuperdiff.Section4.Provider.Annular.jLegField_nonneg {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (n : ℤ) : 0 ≤ jLegField M L m omega n

theorem Algsuperdiff.Section4.Provider.Annular.jLegTranspose_nonneg {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (n : ℤ) : 0 ≤ jLegTranspose M L m omega n

theorem Algsuperdiff.Section4.Provider.Annular.responseJ_le_jLegField {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {n : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube n v)) ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube n v)) (Section3.Observable.inverseSqrtLoad (Section3.Annealed.sigmaBar M m) e) (Section3.Observable.sqrtLoad (Section3.Annealed.sigmaBar M m) e) ≤ jLegField M L m omega n

The hfld slot of ClauseOne.hbfJ_of_lattice_bounds, by definition of the lattice maximum.

theorem Algsuperdiff.Section4.Provider.Annular.responseJ_transpose_le_jLegTranspose {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {n : ℤ} (hnm : n ≤ m) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (latticeCube n v)) ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube n v)).transpose (Section3.Observable.inverseSqrtLoad (Section3.Annealed.sigmaBar M m) e) (Section3.Observable.sqrtLoad (Section3.Annealed.sigmaBar M m) e) ≤ jLegTranspose M L m omega n

The htrn slot of ClauseOne.hbfJ_of_lattice_bounds.

theorem Algsuperdiff.Section4.Provider.Annular.hbfJ_latticeMax {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {Cbf : ℝ} (hCbf : 1 ≤ Cbf) (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 * (jLegField M L m omega (m - ↑l) + jLegTranspose M L m omega (m - ↑l))

The hbfJ binder of ClauseOne.clauseOne_bound, discharged. With the two J-legs defined as the lattice maxima, A4a's producer applies with no remaining hypothesis beyond the manuscript's C >= 1.

The two J-sums are unconditionally summable

theorem Algsuperdiff.Section4.Provider.Annular.jLegField_le_uniform {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {n : ℤ} (hnm : n ≤ m) : jLegField M L m omega n ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseUniformBound (HCPolySupport.originCube d m) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m))

Both lattice maxima are bounded by ONE cube-cu_m ellipticity constant, uniformly in the scale: CoarseGraining's maxDescendantNormalizedBlockResponseAtScale_le_uniform is scale free.

theorem Algsuperdiff.Section4.Provider.Annular.jLegTranspose_le_uniform {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {n : ℤ} (hnm : n ≤ m) : jLegTranspose M L m omega n ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseUniformBound (HCPolySupport.originCube d m) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m))

theorem Algsuperdiff.Section4.Provider.Annular.summable_jLegField {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {s : ℝ} (hs0 : 0 < s) : Summable fun (l : ℕ) => 3 ^ (-(2 * s) * ↑l) * jLegField M L m omega (m - ↑l)

The hsumFl binder, unconditional.

theorem Algsuperdiff.Section4.Provider.Annular.summable_jLegTranspose {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {s : ℝ} (hs0 : 0 < s) : Summable fun (l : ℕ) => 3 ^ (-(2 * s) * ↑l) * jLegTranspose M L m omega (m - ↑l)

The hsumTl binder, unconditional.