ClosureFinalArithmetic #

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

The closure node's parameter arithmetic #

ABK26, l.approximate.recurrence.formula, (the standing hypotheses and the quantifier range) and e.cgamma.constraints.

Closure.NodeContract.TwoSidedClosure quantifies its constant C outside the model and uses it twice: as the largeness threshold C c⋆^{-1} <= E of the standing hypothesis, and as the constant of the two printed displays. The two uses pull in opposite directions --- a larger C strengthens the hypothesis and weakens the conclusion --- so the node's proof is free to enlarge C. This module carries the four pieces of bookkeeping that enlargement needs.

What is supplied #

inductionState_mono --- the induction state is downward closed in its scale parameter. Frozen.Section3.inductionState is literally two forall m <= m0 clauses, so this is immediate; the closure node needs it to feed the state at m0 - 1 into producers that ask for it at n + h - 1.
recurrenceUpperDisplay_mono, recurrenceLowerDisplay_mono --- both printed displays are monotone in the constant C. This is what lets the closure merge the upper display's closureConstant with the lower display's max closureConstant (2 F).
closureRegimeConst and the two regime facts gamma_le_exp_neg_one_of_regime, three_mul_switchBudget_le_one_of_regime: at a large enough absolute threshold C, the manuscript's own standing hypotheses C c⋆^{-1} <= E and cgamma <= E^{-5} already give the two smallness facts grants, namely cgamma <= e^{-1} and 3 * principalResponseSwitchBudget M <= 1. Neither is assumed anywhere below: both are derived from the contract's own antecedents.

The two regime derivations #

Write K0 = principalResponseBudgetConst * 3^128, so that principalResponseSwitchBudget M = K0 E^2 (log cgamma)^2 cgamma.

c⋆ <= 3/2 (Disorder.cstar_le_three_halves), so C c⋆^{-1} <= E gives E >= 2C/3; and E >= 1 with cgamma <= E^{-5} gives cgamma <= E^{-1}. Hence cgamma <= 3/(2C) <= 1/3 <= e^{-1} as soon as C >= 9/2.

For the budget, put t = sqrt (sqrt cgamma), so t^4 = cgamma and log cgamma = 4 log t. From log u <= u - 1 at u = t^{-1}, -log t <= t^{-1}, so (log cgamma)^2 <= 16 t^{-2} and

  cgamma (log cgamma)^2 <= t^4 . 16 t^{-2} = 16 t^2 = 16 sqrt cgamma .

With cgamma <= E^{-5} and sqrt (E^5) = E^2 sqrt E, E^2 sqrt cgamma <= (sqrt E)^{-1}, so

  3 principalResponseSwitchBudget M E 64 <= 48 K0 (sqrt E)^{-1} <= 1

as soon as sqrt E >= 48 K0, which E >= 2C/3 >= (48 K0)^2 gives. closureRegimeConst is 9 + (3/2)(48 K0)^2, which covers both.

References #

ABK26, l.approximate.recurrence.formula.

The induction state is downward closed #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.inductionState_mono {d : ℕ} {M : ABKModel d} {m0 m1 : ℤ} {Ec : { E : ℝ // 1 ≤ E }} (hle : m1 ≤ m0) (hstate : Frozen.Section3.inductionState M m0 Ec) :

Frozen.Section3.inductionState M m1 Ec

Frozen.Section3.inductionState is downward closed in its scale.

The frozen definition is two clauses of the form forall m, m <= m0 -> ..., so lowering m0 only shrinks the range of both.

The two displays are monotone in the constant #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.recurrenceFlatError_mono {d : ℕ} (M : ABKModel d) {C C' E : ℝ} (hCC : C ≤ C') :

recurrenceFlatError M C E ≤ recurrenceFlatError M C' E

The flat error is monotone in the constant.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.recurrenceUpperDisplay_mono {d : ℕ} (M : ABKModel d) {C C' E : ℝ} {n : ℤ} {h : ℕ} (hCC : C ≤ C') (hup : RecurrenceUpperDisplay M C E n h) :

RecurrenceUpperDisplay M C' E n h

The upper display is monotone in the constant.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.recurrenceLowerDisplay_mono {d : ℕ} (M : ABKModel d) {C C' E : ℝ} {n : ℤ} {h : ℕ} (hCC : C ≤ C') (hlo : RecurrenceLowerDisplay M C E n h) :

RecurrenceLowerDisplay M C' E n h

The lower display is monotone in the constant.

The regime threshold #

source

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureRegimeConst :

ℝ

The absolute threshold at which the manuscript's standing hypotheses C c⋆^{-1} <= E and cgamma <= E^{-5} already deliver the two smallness facts grants. It depends on nothing.

Equations