Provedadcgssupportingrestart-induction
A stage-wise halving inequality implies the geometric restart error bound
For all and , if and , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - ⟹Implies
- If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (
ℕ → ℝ) - f(x)Function application
- e applied to 0. Lean writes f x; papers write f(x). (
e 0) - ≤At most
- e(0) is less than or equal to phi. (
e 0 ≤ phi) - ∀For all
- The statement after the comma holds for every s. (
∀ s : ℕ, e (s + 1) ≤ e s / 2) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - +Addition
- s plus 1. (
s + 1) - a/bDivision
- e(s) divided by 2. In Lean, dividing by 0 gives 0. (
e s / 2) - (x : T)As real numbers
- 2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(2 : ℝ)) - aᵇPower
- 2 raised to the power s. (
(2 : ℝ) ^ s)
theorem adcgs-geometric-restart-induction (e : ℕ → ℝ) (phi : ℝ) (h0 : e 0 ≤ phi) (hstep : ∀ s : ℕ, e (s + 1) ≤ e s / 2) :
∀ s : ℕ, e s ≤ phi / (2 : ℝ) ^ sInduction component of the argument in Theorem 4.1 and Appendix A.7 of uploaded arXiv:2601.20443v2. This standalone scalar supporting lemma explicitly assumes halving and only proves its iteration. It must NOT be presented as the complete restart theorem, whose separate main target uses actual AdCGS stages and must establish the stage-wise improvement from the algorithmic assumptions.
How it was proved
- Proved
- 30 September 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 17 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.