AsymptoticsAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The diffusivity asymptotics, assembled from the two printed recurrence displays #
This module is a conditional Provider A. It wires the already-proved deterministic flow spine
DisplayBridge -> SubLandmarkDisplays -> FlowGates -> EndpointSandwich
into the exact conclusion carried by
Algsuperdiff.Frozen.Section3.diffusivity_asymptotics, taking the two printed
displays e.what.do.we.have of l.approximate.recurrence.formula as the
single disclosed pair of hypotheses hforward/hreverse.
What is NOT supplied here #
hforward and hreverse are the printed conclusion of the source node
l.approximate.recurrence.formula, two-sided closure (delivering
e.what.do.we.have). Their whole analytic content -- fresh-shell Dirichlet
and Neumann correctors, the Calderon--Zygmund L^8 bounds, the mesoscopic
oscillation estimate, the localized variational split, the good-event
coefficient switch and the two one-sided Jensen legs -- is untouched.
The display constant is a parameter, and it must be #
This module takes the second option, and that choice is its central design
decision. The flow constant that the assembly can offer necessarily grows with
that C: the calibration hypothesis of FlowGates is quadratic in the
substituted shell constant, so no single Cflow serves every C. The display
constant is therefore carried as the leading parameter Crec of this theorem,
ahead of the existential, and the disclosed binders are stated at the
manuscript's own reading
Erec = Crec * E^2 * |log gamma|^2 , Frec = Crec .
This is the only structural addition to the frozen premise list; every premise
of the frozen statement is carried verbatim, and no premise of it is weakened,
strengthened, reordered or dropped. The parameter does not survive into the
frozen conclusion: a consumer holding the two displays at the manuscript's own
constant C(d) instantiates Crec := C(d) (or max (C(d)) 1) and thereby
recovers the frozen ∃ Cflow statement exactly, so Crec is discharged at the
point of consumption.
The flow constant is derived here, at the current integration constant #
FlowGates assumes its calibration
256 * recurrenceIntegrationConstant ^ 2 * (Cshell * (1 + Cshell + cstarPlus))
<= Cflow ^ 2
rather than proving it. The witness is
Cflow = 16 * recurrenceIntegrationConstant *
(1 + Cshell * (1 + Cshell + cstarPlusUpperBound d)) ,
Cshell = 974 * Crec ,
a function of the dimension d and of the display constant Crec only. The
model-dependent cstarPlus M is replaced, before M is quantified, by the
dimension-only envelope
Provider.Disorder.cstarPlus_le_cstarPlusUpperBound, and the calibration is
monotone in that slot, so the calibration is available at the genuine
Disorder.cstarPlus M for every standing model.
Where the shell factor 974 comes from #
DisplayBridge.sigmaBar_le_thirtySix_mul_sigmaBar produces K = 36, but only
from an induction state valid at the upper endpoint m, and the frozen
premise supplies S(m_0 - 1, E) only. The resulting absolute constant is 974 = 1 + 972 + 1, where 972 is 324 * cstar * log 3 under cstar <= 3/2 and
log 3 <= 2, and the last 1 is the display error Crec E^2 |log gamma|^2 gamma <= 1 in the regime.
The m_star_star floor and the shell budget #
The disclosed binders quantify over mStarStar M <= n only -- exactly the
range delivers. The scale window bound is the consumer's narrow (m: real) <= (n: real) + cstar gamma^{-1}, not the source's wider h <= 6 cstar gamma^{-1}; the narrower window is the weaker hypothesis here, and it is what
the integration engine demands.
The regime premises #
The frozen premise M.gamma <= ((E : real)^{-1})^10 is stronger than the
printed cgamma <= E^{-5}; the weaker forms the spine needs are derived from
it where required, never assumed separately. The landmark premise on m0 is
carried and is not consumed by this route.
The scale gate on m0 (-bin statement change) #
That landmark premise is mStarStar M < m0, not the printed m0 in (mstar, infty) cap Z.
References #
- ABK26,
l.approximate.recurrence.formula, statement,e.what.do.we.have. - ABK26,
l.integrate.approx.recurrence. - ABK26,
e.mstarstar;d.mathcalS.def.
Axiom provenance #
#print axioms Algsuperdiff.Section3.Provider.Diffusivity.diffusivity_asymptotics_of_recurrence_displays
reports [propext, Classical.choice, Quot.sound] and nothing else -- the three
kernel axioms only, with no incomplete-proof axiom in the list.
The derived flow constant #
The flow constant offered by the assembly, at dimension d and display
constant Crec. It is computed fresh against the current
recurrenceIntegrationConstant (see the module header, finding), and it
depends on no model datum: the model-dependent cstarPlus M is replaced by the
dimension-only Provider.Disorder.cstarPlusUpperBound d.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scalar arithmetic for the quotient bound #
The two lemmas of this section are pure real algebra: no rpow, exp or log
occurs in their statements, so the nonlinear arithmetic used to prove them never
meets a transcendental atom.
The geometric ratio on the admissible window #
The quotient bound from the forward display #
The assembled statement #
The diffusivity asymptotics, from the two printed recurrence displays.
hforward and hreverse are disclosed hypotheses, not results. They are
the printed conclusion of l.approximate.recurrence.formula, which this
repository does not prove; see the module header for what is and is not supplied
here, for the reason the display constant must be a parameter, and for the
freshly derived calibration behind Cflow.