Provedattentioninnovationexternal-review-3
Exact deadline completion: variance recurrence solution
For all and , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- p, ν range over real numbers: the statement must hold for every choice. (
(p ν : ℝ)) - 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.) (
ℕ → ℝ) - ≠Not equal
- p and 0 are different. (
p ≠ 0) - f(x)Function application
- V applied to 0. Lean writes f x; papers write f(x). (
V 0) - =Equality
- V(0) and 0 are the same. (
V 0 = 0) - ∀For all
- The statement after the comma holds for every L. (
∀ L, V (L + 1) = ν + (1 - p) * V L) - +Addition
- L plus 1. (
L + 1) - aᵇPower
- 1 − p raised to the power L. (
(1 - p) ^ L) - ·Multiplication
- 1 − p times V(L). (
(1 - p) * V L) - -Subtraction
- 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - p) - a/bDivision
- ν divided by p. In Lean, dividing by 0 gives 0. (
ν / p)
theorem innov-deadline-variance-recurrence (p ν : ℝ) (V : ℕ → ℝ) (hp : p ≠ 0) (h0 : V 0 = 0) (hstep : ∀ L, V (L + 1) = ν + (1 - p) * V L) :
∀ L, V L = (1 - (1 - p) ^ L) * (ν / p)Solves the finite-deadline variance recurrence when its base and step are assumed; the separate finite-history theorem derives those moments from actual probability weights.
How it was proved
- Proved
- 6 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- 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
- 15 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.