IterationLemmaProviderBudget #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The C(d) witness of the iteration anchor and its two prefactor budgets #
The frozen iteration anchor is existential in C: ∃ C : ℝ, 0 < C ∧ …. This
module proves an explicit C = iterConst d, a closed-form function of d
alone, and proves the two budget inequalities the provider consumes:
iterBudgetOne--- conclusion (i)'s prefactor9 · Ci² · (goodConst · badConst)^{3|B|+3} ≤ exp(C (h+1)(|B|+1));iterBudgetTwo--- conclusion (ii)'s prefactor(2 κ^{h+2})^{|B|+1} · (1 + (45/2) Ci) · (goodConst · badConst)^{3|B|+3} ≤ exp(C (h+1)(|B|+1)).
Both reduce to one master product bound (iterMaster) at |B| = 0, because every
factor is ≥ 1 and the per-level factor is raised to the power |B|+1 (pow_succ_mul_le).
The master is closed by a single logarithm computation whose only non-elementary input is
log (goodConst h κ Cstab) ≤ (h+1)(1 + log κ + log (5/2 + 35 Cstab/2 + 6 + 35 Cstab)) ,
i.e. log_goodConst_le: the good-run constant grows like h κ^h, so its
logarithm is O(h log κ + log h) and dividing by h+1 leaves a d-only
bound.
The witness versus the review's recorded floor (disclosed) #
The freeze review recorded a sufficient floor for C(d), built from the
one-sided slope constant oneSidedSlopeConstTriadic d and asking for
2·goodRate. iterConst d below is not that expression: it is an
independently machine-verified witness built from the two-sided constant
slopeStabilityConst d (1/9) κ, which is the constant the proved engine's
hstab slot actually consumes (and which is ≤ the one-sided one, since the
latter is the former times 1 + κ), and it asks for goodRate once, because
the route below pays the ∑ε exponential exactly once. Every other summand is
the same shape as the review's: 3(1 + log κ + log(a+b) + log badConst) plus
explicit numeric slack. The recorded floor is therefore not adopted verbatim;
what is proved is that this C(d) works, and C is existential in the
frozen statement.
Tactic discipline #
Every numeric closure here is an exp/log statement, so no numeric tactic is ever
applied to a transcendental atom: the polynomial content is isolated in the private
abstract-real lemma budget_arith (opaque variables only), the transcendental content is
Real.log_le_iff_le_exp, Real.log_mul, Real.log_pow, Real.log_le_sub_one_of_pos and
Real.exp_nat_mul, and no nlinarith occurs anywhere.
References #
- ABK26,
l.iteration.lemmaconclusions (i) and (ii).
The constants of the consumption class #
The quasi-monotonicity constant of the anchor's window family: κ(d) = 3^{3+3d/2}.
Equations
Instances For
The gradient-stability constant of the anchor's window family (the two-sided producer's
own constant, at the printed aspect ratio 1/9).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The endpoint-comparison constant of the anchor's window family, at the printed aspect
ratio 1/9.
Equations
Instances For
The C(d) witness of the frozen iteration anchor: an explicit function of d
alone. Every summand is nonnegative, the leading 2 covers the θ-payback exponent
(h+2)(|B|+1) ≤ C(h+1)(|B|+1), the goodRate summand covers the ∑ε exponent, and the
remaining summands are the master budget's logarithmic pieces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The elementary properties of the witness #
The logarithm of the good-run constant #
The budget fact. goodConst h κ Cstab grows like h κ^h, so its logarithm is at
most (h+1) times a quantity depending on κ and Cstab only. This is what makes a
d-only C possible in the frozen statement, and it is why the frozen exponent carries
the product (h+1)(|B|+1) rather than the printed sum.
The master budget #
The master budget (the |B| = 0 level of both prefactors): the whole per-level
product of the two conclusions is below exp(C(h+1)).
The two prefactor budgets #
Conclusion (i)'s prefactor budget.
Conclusion (ii)'s prefactor budget.
The two prefactors in the exact shape the provider consumes #
Conclusion (ii)'s prefactor, in the exact shape the weighted assembly produces:
the θ-payback (κθ^{-1})^{h+2} per level is split into the κ-part, absorbed by the
exp factor, and the θ-part, absorbed by the frozen statement's θ^{-C(h+1)(|B|+1)}
(legitimate because C ≥ 2 and (h+2)(c+1) ≤ 2(h+1)(c+1)).