ProfileClose

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

The collar and the constant pricing of p.cg.ellipticity.bounds at q = 2

Provider/CoarseEllipticity/PayloadSandwich.lean composes the two legs' payload conjunctions out of GridDomination's on-grid dominations and BlockPayload's per-scale block payload. What its two producers deliver is a deterministic slot (ctop Cdet + Cdet) (mass rho^{-1}) and an exceptional amplitude foldedBlockPole d sigma A mass rho ctop p, at the raw pole rho = 2s. What the frozen displays require is the priced form: the deterministic slot inside lowerEllipticityProfile Clow gamma s q (lower) resp. inside Cup (upper), and the exceptional amplitude below the frozen rare scale exp(-Clow^{-1} E^{-2} gamma^{-1}). This module is that pricing, and nothing else: every declaration below is an inequality between real numbers, no observable, no measure and no source step enters.

The four items, and what each of them is

1. The collar, rho = 2s -> 2s - gamma (/ 6185 / 6212). e.slstar.multiscale normalizes by 3^{-gamma(m-n)} on its left, so the lifted per-scale display carries 3^{gamma(k+1)} on its right. A k-dependent factor cannot sit in the consumers' Cdet; BlockPayload.{forall_le_tsum_gridWeight_collar, le_tsum_gridWeight_collar} absorbs it into the weight, which is exactly the passage from the pole 2s to the pole 2s - gamma. §5 runs that absorption through the lower summation. Its three-term twin is generic algebra, but the faithful upper source route applies the collar only to its two random lanes and keeps the deterministic slot at the raw pole, as Item 2 records.

2. The deterministic slot. detSlot_le_lowerEllipticityProfile prices (ctop Cdet + Cdet)(c_{s,2} (2s-gamma)^{-1}) into lowerEllipticityProfile Clow gamma s (finite r) on the printed branch 2 <= r, through c_{s,2} <= 4s (Book.Ch02.geometricDiscount_le_two_mul, the bound behind LambdaGridBridge.gridSumConst_two_le) and LowerLegProfile.lowerEllipticityProfile_finite_of_two_le. The output gate is 4 (ctop + 1) Cdet <= Clow. The upper leg's deterministic slot must not take the collar. On the frozen window c_{s,2} (2s - gamma)^{-1} is unbounded (at s = gamma/2 + eps it is ~ gamma log 3 / (2 eps) with eps = exp(-C^{-1}E^{-2}gamma^{-1})), so no dimension-only Cup majorizes it; and it need not, because the printed per-cube upper display has the deterministic C and carries 3^{gamma(m-n)} only on the two random lanes. detSlot_le_upperConst therefore prices the upper slot at the uncollared pole (2s)^{-1}, where c_{s,2} (2s)^{-1} <= 2 is a genuine dimension-only bound --- which is exactly the slot PayloadSandwich.threeTermSplit_cutoffUpperEllipticity already produces. The upper output gate is 2 (ctop + 1) Cdet <= Cup.

3. The exceptional amplitude, and the absorption gate. foldedBlockPole_eq puts the folded pole in closed form Gamma_tri(sigma)^2 (mass (gridNetConst A)) (ctop rho^{-1} + p! (1+rho^{-1})^{p+1}); poleBracket_le collapses the bracket against the window's own 2 eps <= 2s - gamma; and foldedBlockPole_le_of_gate proves foldedBlockPole <= eps.

4. The upper Gamma_1 lane. tsum_gridWeight_mul_foldedOrdinaryAmp_le sums the folded ordinary amplitudes at the source's own degree (e.bL.multiscale's per-cube C gamma (m-n+1) lifted by e.maxy.bound's (m-n+1)^{1/sigma} at sigma = 1, i.e. degree 2) against gridWeight rho, producing the pole order 3 --- the printed (2s-gamma)^{-3} of e.cg.ellip.upper, not an over-bound. hB1_le_frozenUpperOrdinary then proves the frozen amplitude Cup cstar^{-1} s gamma (2s-gamma)^{-3} verbatim, using c_{s,2} <= 4s and cstar <= 3/2 (two_thirds_le_cstar_inv).

What is NOT proved here

Nothing analytic. No per-cube block estimate (p.bfA.multiscalebound), no L-uniformity, no base case, no observable and no measure occurs in any statement of §1--§4 and §6; §5's two theorems are the model-free summations of LowerLeg / ScaleSummation with the collar inserted, and they carry their hgrid and hsplit binders exactly as those consumers do. No node is closed by this module, and no theorem below asserts that any leg's payload is satisfiable.

References

• ABK26, p.cg.ellipticity.bounds, statement (e.cg.ellip.lower, e.cg.ellip.upper); proof, with e.cg.ellip.lower.pre, e.cg.ellip.upper.pre and the absorption gate ("the assumption 2s - gamma > exp(-c E^{-2} gamma^{-1}) allows us to absorb the factors of (2s - gamma) into the exponential").
• ABK26, p.bfA.multiscalebound, e.slstar.multiscale label, e.bL.multiscale label; l.maximums.Gamma.s label.
• Provider/CoarseEllipticity/{PayloadSandwich, BlockPayload, LowerLeg, LowerLegProfile, ScaleSummation, GridWeights, LambdaGridBridge}.lean (the consumers whose slots are priced here).

1. Abstract-real cores

Every core of this module is stated over abstract reals: no Real.exp and no Real.rpow occurs in §1, so no nonlinear arithmetic step ever meets a transcendental.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.one_le_inv_of_le_one {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) : 1 ≤ eps⁻¹

On (0, 1] the reciprocal is at least one.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.one_add_inv_le_two_mul_inv {eps rho : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) (hrho : 2 * eps ≤ rho) : 1 + rho⁻¹ ≤ 2 * eps⁻¹

The window collapse. If the rare scale eps sits at most halfway to the pole parameter rho --- which on the frozen window is exactly 2 exp(-C^{-1}E^{-2}gamma^{-1}) <= 2s - gamma --- then the printed algebraic pole 1 + rho^{-1} is at most 2 eps^{-1}.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.mul_le_of_pow_inv_gate {K A P eps : ℝ} {n : ℕ} (hKA : 0 ≤ K * A) (heps : 0 < eps) (hP : P ≤ eps⁻¹ ^ n) (hgate : K * A ≤ eps ^ (n + 1)) : K * A * P ≤ eps

The absorption step, abstractly. A nonnegative product K A bounded by eps^{n+1} absorbs a pole of order n in eps and proves at eps. This is the whole arithmetic.

2. The folded pole in closed form, and its gate

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridBlockAmp_zero (d : ℕ) (sigma A : ℝ) : gridBlockAmp d sigma A 0 = gridNetConst d sigma * A

The folded amplitude's head: at gap 1 the e.maxy.bound polynomial is trivial.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedBlockPole_eq (d : ℕ) (sigma A mass rho ctop : ℝ) (p : ℕ) : foldedBlockPole d sigma A mass rho ctop p = HCPolySupport.IndependentSums.gammaTriangleConst sigma ^ 2 * (mass * (gridNetConst d sigma * A)) * (ctop * rho⁻¹ + ↑p.factorial * (1 + rho⁻¹) ^ (p + 1))

The folded pole in closed form. foldedBlockPole factors as a dimension-only head times the bracket ctop rho^{-1} + p! (1+rho^{-1})^{p+1}, which is the only place the pole lives.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.poleBracket_le {rho eps ctop : ℝ} (p : ℕ) (heps : 0 < eps) (heps1 : eps ≤ 1) (hrho : 2 * eps ≤ rho) (hctop : 0 ≤ ctop) : ctop * rho⁻¹ + ↑p.factorial * (1 + rho⁻¹) ^ (p + 1) ≤ 2 ^ (p + 1) * (ctop + ↑p.factorial) * eps⁻¹ ^ (p + 1)

The bracket of foldedBlockPole_eq, collapsed against the window.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedBlockPole_le_of_gate {d : ℕ} {sigma A mass rho ctop eps : ℝ} {p : ℕ} (hmass : 0 ≤ mass) (hA : 0 ≤ A) (hctop : 0 ≤ ctop) (heps : 0 < eps) (heps1 : eps ≤ 1) (hrho : 2 * eps ≤ rho) (hgate : HCPolySupport.IndependentSums.gammaTriangleConst sigma ^ 2 * (mass * gridNetConst d sigma) * (2 ^ (p + 1) * (ctop + ↑p.factorial)) * A ≤ eps ^ (p + 2)) : foldedBlockPole d sigma A mass rho ctop p ≤ eps

The exceptional amplitude, priced below the rare scale.

hgate is the definition of the output constant: it fixes how small the per-cube amplitude A of p.bfA.multiscalebound must be against the leg's own rare scale eps, and gate_of_perCubeExponential below discharges it from the source's own exp(-c E^{-2} gamma^{-1}) shape.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedBlockPole_le_of_window {d : ℕ} {sigma A mass ctop gamma s eps : ℝ} {p : ℕ} (hmass : 0 ≤ mass) (hA : 0 ≤ A) (hctop : 0 ≤ ctop) (heps : 0 < eps) (heps1 : eps ≤ 1) (hwin : gamma / 2 + eps ≤ s) (hgate : HCPolySupport.IndependentSums.gammaTriangleConst sigma ^ 2 * (mass * gridNetConst d sigma) * (2 ^ (p + 1) * (ctop + ↑p.factorial)) * A ≤ eps ^ (p + 2)) : foldedBlockPole d sigma A mass (2 * s - gamma) ctop p ≤ eps

The same, with the window hypothesis in the frozen statement's own shape gamma/2 + eps <= s (i.e. hsWindow.1) and the collar-absorbed pole rho = 2s - gamma.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedBlockPole_frozenUpper_le {d : ℕ} {sigma A mass ctop gamma s eps : ℝ} (hmass : 0 ≤ mass) (hA : 0 ≤ A) (hctop : 0 ≤ ctop) (heps : 0 < eps) (heps1 : eps ≤ 1) (hwin : gamma / 2 + eps ≤ s) (hgate : HCPolySupport.IndependentSums.gammaTriangleConst sigma ^ 2 * (mass * gridNetConst d sigma) * (128 * (ctop + 720)) * A ≤ eps ^ 8) : foldedBlockPole d sigma A mass (2 * s - gamma) ctop 6 ≤ eps

The upper leg's exceptional amplitude at p = 6 --- the rounding integer of the frozen index (1-sigma)/3 (frozenUpperIndex_inv_le_natSix), so the pole order is p + 1 = 7, an over-bound of the printed (2s-gamma)^{-(4+sigma)}.

3. The frozen rounding integers, and the absorption gate

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.frozenUpperIndex_inv_le_natSix {sigma : ℝ} (h1 : sigma ≤ 1 / 2) : ((1 - sigma) / 3)⁻¹ ≤ ↑6

p = 6 is admissible at the frozen upper index (1-sigma)/3.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exp_neg_frozen_le_one {Clow E gamma : ℝ} (hClow : 0 < Clow) (hgamma : 0 < gamma) : Real.exp (-(Clow⁻¹ * E⁻¹ ^ 2 * gamma⁻¹)) ≤ 1

The frozen rare scale is at most one, which is the eps ≤ 1 binder of §2.