GammaTenInteriorArithmetic

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

The depth fold closes: the linear factor of the depth endpoints is summable

ABK26, Step 2 of l.approximate.recurrence.formula, e.lower.bound.oscillations.

The one inequality that has to be honest

The depth-indexed endpoints of Closure.GammaTenDepthOscillation carry the decay factor (1 + i) 3^{-i}, not the bare 3^{-i}: the linear factor of the buffer N_i = Ngap + i is genuinely there. At the fourth power the per-depth input of the Besov fold is therefore

  D i  =  cgamma^{64} (1+i)^4 3^{-4i}  =  cgamma^{64} (1+i)^4 81^{-i} ,

while the fold's own weights are 2^{i+1} 3^{4 s i} = 2^{i+1} 9^i at the closure's exponent s = gammaTenBesovExponent = 1/2. The ratio gate of Closure.GammaTenEnvelopeInputGrid.sum_two_pow_mul_rpow_pow_four_geometric_le is 2 . 9 . r <= 1/2, i.e. r <= 1/36, so what must be true is

  (1 + i)^4 81^{-i}  <=  25 . 36^{-i}   for every i ,

equivalently the integer inequality (1+i)^4 4^i <= 25 . 9^i. That is succ_pow_four_mul_four_pow_le, and it is tight: at i = 4 the two sides are 625 . 256 = 160000 and 25 . 6561 = 164025. It is proved here by induction from i = 4 --- the four smaller cases are checked directly, because the induction step 4 (i+2)^4 <= 9 (i+1)^4 is false for i <= 3.

Everything downstream is bookkeeping: with the refinement cost 2 of Closure.GammaTenInteriorGeometry the fold input is A r^i at A = 50 cgamma^{64} and r = 1/36, the fold sum is below 4 A = 200 cgamma^{64}, and 200 cgamma^{64} <= cgamma^{60} because 200 (1/4)^4 = 200/256 < 1. The resulting envelope's grid fourth-moment root is therefore below (cgamma^{60})^{1/4} = cgamma^{15}, which is exactly the threshold Closure.GammaTenCloserAssembly.ClosureBesovEnvelopeInput demands.

What is proved

• succ_pow_four_mul_four_pow_le --- the integer inequality.
• depth_decay_pow_four_le --- its real form, at the depth endpoints' own decay factor.
• gridFourthMoment_le_pow_four_of_root_le --- the fourth moment from its root.

The composite --- the fold sum of the depth endpoints' fourth powers, with the refinement cost included --- is assembled on top of these in Closure.GammaTenStripEnvelopeConst.sum_depth_fold_const_le, which stops at 200 A^4 cgamma^{64} and leaves the closing numerical step in cgamma to its caller.

Binders

Elementary arithmetic and 0 < cgamma <= 1/4. No smallness gate beyond that quarter bound, nothing about the mesh, the corrector or the sample space.

Scope

Internal Provider infrastructure for the Step-2 fluctuation estimate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2, e.lower.bound.oscillations.

The tight integer inequality

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.succ_pow_four_mul_four_pow_le (i : ℕ) : (1 + i) ^ 4 * 4 ^ i ≤ 25 * 9 ^ i

(1+i)^4 4^i <= 25 . 9^i. The induction step 4 (i+2)^4 <= 9 (i+1)^4 holds only from i = 4 on, so the four smaller cases are checked directly. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.depth_decay_pow_four_le (i : ℕ) : ((1 + ↑i) * 3 ^ (-↑i)) ^ 4 ≤ 25 * (1 / 36) ^ i

The depth endpoints' decay factor at the fourth power. The linear factor (1 + i) costs the absolute constant 25 and nothing else: the ratio stays at the fold's own gate 1/36. Unconditional.

The fourth moment from its root

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gridFourthMoment_le_pow_four_of_root_le {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → Omega → ℝ) {c : ℝ} (h : gridFourthMomentRoot mu I F ≤ c) : gridFourthMoment mu I F ≤ c ^ 4

The grid fourth moment from its fourth root. Unconditional.