FlowGates #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Parameter gates for the diffusivity-flow recurrence integration #
This module is deterministic parameter-gate infrastructure. It performs the
scalar bookkeeping that turns a calibration inequality on a flow constant
Cflow, together with the two smallness conditions Cflow c⋆⁻¹ ≤ E and
γ ≤ (E⁻¹)¹⁰, into the three numerical facts that a Section 3.4 assembly needs
when it substitutes the recurrence parameters
Eint = Cshell E² |log γ|², Fint = Cshell
into integrate_approx_recurrence:
- the
γ-threshold demanded by that lemma at the substituted parameters; - the absorption of the reported rate into
Cflow c⋆⁻¹ E √γ |log γ|; - the bound
Cflow c⋆⁻¹ E √γ |log γ| ≤ 1/4on that amplitude.
Every hypothesis below is an explicit input binder. In particular hcstar32: cstar ≤ 3/2, hcc: cstar ≤ cstarPlus, hCshell: 1 ≤ Cshell and the
calibration hcal are assumed here, never derived; no model, probability
space, or analytic producer is referenced.
The calibration hypothesis #
All gates share one input inequality on the flow constant,
256 * recurrenceIntegrationConstant² * (Cshell (1 + Cshell + cstarPlus)) ≤ Cflow².
It is the squared form of the two separate requirements that the arithmetic
actually has: a cube bound 16 C_int Cshell(1+Cshell+cstarPlus) ≤ Cflow³ for the
threshold and the amplitude, and a square bound
C_int² Cshell(1+Cshell+cstarPlus) ≤ Cflow² for the rate. The squared form
above implies both, so a single input suffices.
Elementary consequences of the calibration hypothesis #
The pure-algebra core of the threshold gate #
The three gates #
Gate (i): the γ-threshold at the substituted recurrence parameters.
At Eint = Cshell E² |log γ|² and Fint = Cshell the smallness condition
demanded by integrate_approx_recurrence follows from the calibration
hypothesis together with Cflow cstar⁻¹ ≤ E and γ ≤ (E⁻¹)¹⁰. This is where
the tenth inverse power of E is spent: √γ ≤ (E⁻¹)⁵ converts the E²|log γ|²
inflation of Eint into a decaying factor E⁻³.
Gate (ii): absorption of the reported rate.
The rate reported by integrate_approx_recurrence at the substituted
parameters is at most Cflow cstar⁻¹ E √γ |log γ|. Only the square form of the
calibration hypothesis is used here; no γ-smallness is needed.
Gate (iii): the amplitude is at most 1/4.
The squeeze that converts the relative-error estimate into a two-sided bound
needs the deviation coefficient below 1/4. Here √γ |log γ| ≤ 4 √(√γ) and
√γ ≤ (E⁻¹)⁵ give √γ|log γ| ≤ (E⁻¹)²/4 once E ≥ 256, and one factor E
is returned by the regime condition.
Companion gate: the substituted recurrence parameters are at least 1.
integrate_approx_recurrence additionally asks for 1 ≤ Eint and 1 ≤ Fint.
At the substitution Eint = Cshell E² |log γ|², Fint = Cshell both hold under
the same regime conditions.