ShomContinuityArithmetic #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The model-free arithmetic layer of shom_continuity #
This module is the arithmetic support of
Algsuperdiff/Section3/Provider/Localization/ShomContinuity.lean. The split
itself was pure motion: every statement and every proof arrived as the text
that stood in ShomContinuity.lean, unchanged apart from private lemma
becoming protected theorem. Nothing was strengthened, renamed, added or
dropped.
That pass rewrote proof bodies only: all twenty-nine nlinarith closers were
replaced by explicit calc chains, monotonicity lemmas
(mul_le_mul_of_nonneg_*, pow_le_pow_left₀, one_le_pow₀,
le_mul_of_one_le_right) and named factored-nonnegativity haves discharged
by linarith only, and every remaining unqualified linarith was given an
explicit hypothesis list. The twenty-three statements are byte-identical to
the pre-pass text and no declaration was added, renamed or removed; warm
own-file elaboration fell from 10.2 s to 3.6 s (interpretation 11.7 s to 2.6
s).
What is here #
Two groups, in the order they stood in the original file.
- Abstract-real arithmetic --- eighteen of the twenty-three declarations.
- The three transcendental estimates --- the remaining five declarations,
namely
rpow_three_two_mul_le, the third estimatepow_four_mul_sqrt_mul_abs_log_lewith its two helpersabs_log_le_sixteenthandsqrt_eq_pow_eight, andone_le_abs_log, isolated exactly as before so that the nonlinear arithmetic tactics never meet a transcendental atom.
No renormalization, probabilistic or geometric object occurs anywhere below; no
ABKModel, no Annealed.sigmaBar, no scale. The five model-level private
lemmas of the continuity route (near_flow_bound, near_recurrence_bound,
window_binders, slack_bounds, defect_display) stayed in
ShomContinuity.lean and are not duplicated here.
References #
- ABK26,
l.shom.continuity; proof, whose envelope computation is the arithmetic realized here.
Abstract-real arithmetic #
Every lemma in this section is over abstract reals; none of them contains a
Real.rpow, Real.exp or Real.log atom, so the arithmetic tactics never meet
a transcendental.
Two-sided ratio defect from the two one-sided caps: if a <= (1+u) b and
b <= (1+v) a with u, v >= 0, both ratio defects are at most u + v.
The short-range core of branch (B). Two positive reals a, b
approximating two reals A, B with the same relative accuracy
delta <= 1/2, whose targets are ordered B <= A <= (1 + 4x) B with
0 <= x <= 1/8, have two-sided ratio defect at most 8x + 24 delta.
This is the arithmetic read off the flow display rather than off the recurrence
display: delta is the flow's relative defect and 4x the geometric growth of
the target profile across the gap.
The two-sided defect from the two recurrence binders (branch (C)), over
abstract reals: u is the flat slack, ai the relative increment
A_{n,m} shom_n^{-2} and qq the relative quadratic remainder.
The increment leg of the computation. With P = 3^{2 cgamma n} and T = 3^{2 cgamma (m-n)} <= 27, the lower envelope shom_n^2 >= (1/4) cstar cgamma^{-1} P turns A_{n,m} <= cstar L (m-n) P T into A_{n,m} shom_n^{-2} <= 216 cgamma (m-n).
The quadratic leg of the computation. The gate cgamma (m-n) <= cstar^2 / 2 of branch (C) is what converts the quadratic remainder's (cgamma (m-n))^2 cstar^{-2} into a linear cgamma (m-n).
The delta gate. Under 32 Cflow cstar^{-1} <= E, 1 <= Cflow and the
E^4 gate, the flow's relative defect is below cstar^2 / 2. This is the
sharpening records: it is what removes the manuscript's medium band and keeps
the constant dimension-only.
Regrouping of the flow display at one scale, with the constant enlarged to max 1 Cflow.
Abstract-real core of the exponential's tangent bound. From
(1 - u) X <= 1 with 0 <= u <= 1/2, cancel the positive factor 1 - u
against (1 - u)(1 + 2u) = 1 + u - 2u^2 >= 1 (X need not be nonnegative).
Applied at X := Real.exp (4 z), u := 4 z, it keeps Real.exp out of every
nonlinear tactic goal in rpow_three_two_mul_le.
The three transcendental estimates #
Each is a consequence of Real.add_one_le_exp or Real.log_le_sub_one_of_pos;
they are isolated here so that no nlinarith ever meets a transcendental.
Since the elaboration pass this file contains no nlinarith at all, and
every linarith in it is an only-form with an explicit hypothesis list, so
no rpow-laden context is preprocessed into products anywhere below. The only
nlinarith on the route is in the consumer ShomContinuity.lean, the
only-form of near_recurrence_bound on three cstar facts. linarith in
the consumer does meet Real.exp, Real.log and Real.rpow, but only as
opaque atoms and monomials in them (the earlier unqualified claim, that no
arithmetic tactic there sees them in a nonlinear position, was false as
stated).
The cgamma-gate at the sharp exponent. Under 1 <= E and cgamma <= E^{-10}, E^4 cgamma^{1/2} |log cgamma| <= 16. Every comparison is an
integer power: v := g^{1/16} is four square roots, |log g| <= 16 v^{-1},
sqrt g = v^8, and (E^4 v^7)^{16} = E^{64} g^7 <= E^{64} E^{-70} <= 1.