TwoSidedTargets #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.what.do.we.have: the two one-sided targets, and their consumption shape #
This module does two things and nothing else.
It transcribes the two displayed inequalities of
e.what.do.we.haveat the repository's own carriers: the genuine running diffusivityAnnealed.sigmaBarand the recurrence pair(n, n+h). Nothing is asserted about them here --- they areProp-valued definitions, the statements that the two-sided closure ofl.approximate.recurrence.formulahas to produce.It proves, unconditionally, that those two displays deliver exactly the two hypotheses
hupperandhlowerofRecurrenceIntegration.integrate_approx_recurrence, at the sequences = fun m => (Annealed.sigmaBar M m : ℝ). This is the carrier match the root assembly needs, and it is pure arithmetic: no measure, no corrector, no in-flight endpoint.
The printed displays #
shom_{n+h} shom_n^{-1}
<= 1 + (log 3) cstar shom_n^{-2} sum_{k=n+1}^{n+h} 3^{2 cgamma k}
+ C E^2 |log cgamma|^2 cgamma ,
shom_n shom_{n+h}^{-1}
<= 1 - (log 3) cstar shom_n^{-2} sum_{k=n+1}^{n+h} 3^{2 cgamma k}
+ C h^2 shom_n^{-4} 3^{4 cgamma (n+h)}
+ C E^2 |log cgamma|^2 cgamma .
|log cgamma|^2 is rendered Real.log M.gamma ^ 2 --- the square of the log,
which equals the square of its absolute value --- so that the shape agrees
verbatim with principalResponseSwitchBudget, the budget the principal-response
terminal produces. The drift (log 3) cstar shom_n^{-2} sum ... is
Closure.shellDrift, and it is exactly shom_n^{-2} times the A_{n,m} of
e.A.def (RecurrenceIntegration.recurrenceIncrement); shellDrift_eq records
that identity.
The asymmetry of the two bridges #
hupper follows from the upper display alone. hlower needs both: the
printed lower display carries its error flat and against the ratio, while
e.assump.lower.modified carries it against s n. Converting costs a bound
on shom_{n+h} shom_n^{-1}, and the cheapest such bound is the upper display
itself together with the absolute cap shellIncrementCap.
References #
- ABK26,
e.what.do.we.have. - ABK26,
e.assump.upper,e.assump.lower.modified,e.A.def.
The printed error budget #
The printed flat error C E^2 |log cgamma|^2 cgamma of both lines of
e.what.do.we.have.
Equations
Instances For
The two displays #
The first line of e.what.do.we.have.
shom_{n+h} shom_n^{-1}
<= 1 + (log 3) cstar shom_n^{-2} sum_{k=n+1}^{n+h} 3^{2 cgamma k}
+ C E^2 |log cgamma|^2 cgamma .
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second line of e.what.do.we.have.
shom_n shom_{n+h}^{-1}
<= 1 - (log 3) cstar shom_n^{-2} sum_{k=n+1}^{n+h} 3^{2 cgamma k}
+ C h^2 shom_n^{-4} 3^{4 cgamma (n+h)}
+ C E^2 |log cgamma|^2 cgamma .
The manuscript prints one and the same C in front of the quadratic h-error
and in front of the flat error; that is transcribed literally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The degenerate shell h = 0 #
The manuscript quantifies over h in N. At h = 0 the shell of e.def.w is
empty, both correctors vanish and both printed lines reduce to 1 <= 1 + error.
Proving that case here means the closure node's own proof may assume 0 < h
without weakening the contract.
The drift is the e.A.def increment, gauged #
shellDrift is shom_n^{-2} times the increment A_{n,m} of e.A.def, at m = n + h.
The upper bridge #
e.assump.upper from the printed upper display.
Multiplying the ratio display by shom_n > 0 converts it verbatim into the
hypothesis hupper of integrate_approx_recurrence, with
E_integration cgamma = C E^2 |log cgamma|^2 cgamma .
Unconditional: the only binder is the display itself.
The ratio cap #
The upper display, together with the absolute drift cap, bounds the
diffusivity ratio by an explicit constant. This is what the lower bridge spends
to move the flat error from the ratio onto shom_n.
The lower bridge #
e.assump.lower.modified from the two printed displays.
The conclusion is exactly the hlower hypothesis of
integrate_approx_recurrence at
s = fun m => (Annealed.sigmaBar M m : R) ,
A_{n,m} = recurrenceIncrement (cstar M) cgamma n (n+h) ,
E_integration = (2 + shellIncrementCap) C E^2 |log cgamma|^2 ,
F = C .
hup is needed only through the ratio cap: it is what turns the printed
ratio-carried error into an error carried by s n, at the cost of the single
factor 2 + shellIncrementCap. Unconditional otherwise.