FiniteQPresplit

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

The conditional finite-q pre-split producer

Its analytic input is pointwise and per depth: the normalized Chapter 4 descendant maximum is at most the deterministic profile Cprof * 3^(gamma n) plus a nonnegative random remainder. The split is kept inside the defining ell^(q/2) aggregate.

The total q/2-power summability needed by the aggregate comparison is proved below from the two separate lanes. It is deliberately not an interface hypothesis. The random lane is linearized only after the pre-split, and is then summed with the countable Gamma_sigma triangle inequality.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.twoTermFamilySplit_cutoffLowerEllipticityInv_of_finiteQPresplit {d : ℕ} (M : ABKModel d) (m : ℤ) (r : { r : ℝ // 1 ≤ r }) (hr : 2 ≤ ↑r) {s Cprof scaling sigmaTail B : ℝ} (hs : 0 < s) (hgap : 0 < 2 * s - M.gamma) (hCprof : 0 ≤ Cprof) (hscaling : 0 ≤ scaling) (hsigmaTail : 0 < sigmaTail) {L0 : ℤ} {U : ℕ → Cutoff.CutoffSample d → ℝ} {a : ℕ → ℝ} (hUnonneg : ∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ U n omega) (hUmeas : ∀ (n : ℕ), Measurable (U n)) (hUqsum : ∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * U n omega ^ (↑r / 2)) (hUlinsum : ∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * U n omega) (ha : ∀ (n : ℕ), 0 < a n) (hasum : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * a n) (hUO : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigmaTail) (U n) (a n)) (hbudget : 2 * HCPolySupport.IndependentSums.gammaTriangleConst sigmaTail * ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * a n ≤ B) (hdepth : ∀ (omega : Cutoff.CutoffSample d) (L : ℤ), L0 ≤ L → ∀ (n : ℕ), scaling * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ finiteQGeometricProfile Cprof M.gamma n + U n omega) : ∃ (Ydet : Cutoff.CutoffSample d → ℝ) (Y : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), L0 ≤ L → Observable.cutoffLowerEllipticityInv M m L s hs (CoarseEllipticityExponent.finite r) omega * scaling ≤ Ydet omega + Y omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Ydet omega ≤ 4 * Cprof * s * (2 * s - M.gamma)⁻¹) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigmaTail) Y B

A pointwise finite-q pre-split at every depth produces the lower coarse-ellipticity two-slot payload. Summability of the combined profile is a conclusion inside the proof, not a hypothesis of this theorem.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_lower_branchPayload_two_le_of_finiteQPresplit (d : ℕ) {Clow Cprof : ℝ} (hCprof : 0 ≤ Cprof) (habsorb : 4 * Cprof ≤ Clow) (finiteQPresplit : ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (r : { r : ℝ // 1 ≤ r }), 2 ≤ ↑r → ∀ s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1, ∃ (U : ℕ → Cutoff.CutoffSample d → ℝ) (a : ℕ → ℝ), (∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ U n omega) ∧ (∀ (n : ℕ), Measurable (U n)) ∧ (∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * U n omega ^ (↑r / 2)) ∧ (∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * U n omega) ∧ (∀ (n : ℕ), 0 < a n) ∧ (Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * a n) ∧ (∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (U n) (a n)) ∧ 2 * HCPolySupport.IndependentSums.gammaTriangleConst ((1 - sigma) / 2) * ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * a n ≤ Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) ∧ ∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → ∀ (n : ℕ), ↑(Annealed.sigmaBar M (m - 1)) * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ finiteQGeometricProfile Cprof M.gamma n + U n omega) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) : Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (r : { r : ℝ // 1 ≤ r }), 2 ≤ ↑r → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), ∃ (Ydet : Cutoff.CutoffSample d → ℝ) (Y : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → Observable.cutoffLowerEllipticityInv M m L s ⋯ (CoarseEllipticityExponent.finite r) omega * ↑(Annealed.sigmaBar M (m - 1)) ≤ Ydet omega + Y omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Ydet omega ≤ Clow * s * (2 * s - M.gamma)⁻¹) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) Y (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The finite-q pre-split interface, uniformly over the induction data, discharges exactly the payloadTwoLe argument of coarse_ellipticity_lower_payload_of_branchPayloads.

The constant gate 4 * Cprof <= Clow absorbs only the dimension-free factor two from the pre-split and the factor two in the deterministic geometric profile estimate.