Provedattentioninnovationexternal-review-3
Surrogate innovation: full finite-deadline history moments
For all , and , if , , , , , and (given ), then
What the notation means · or point at any symbol
- Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to J. Lean writes f x; papers write f(x). (
Fintype J) - ⟹Implies
- If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (
J → ℝ) - x : TVariables
- r, a, g range over J → ℝ: the statement must hold for every choice. (
(r a g : J → ℝ)) - x ∈ TVariables
- p, d, ν range over real numbers: the statement must hold for every choice. (
(p d ν : ℝ)) - ∀For all
- The statement after the comma holds for every j. (
∀ j, 0 ≤ r j) - ∑Summation
- Add up r(j) for every j. (
∑ j, r j) - =Equality
- ∑ j, r(j) and 1 are the same. (
∑ j, r j = 1) - ≠Not equal
- p and 0 are different. (
p ≠ 0) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to r(j). (
0 ≤ r j) - ∧And
- Both hold: 0 ≤ a(j), and a(j) ≤ 1. (
0 ≤ a j ∧ a j ≤ 1) - ·Multiplication
- r(j) times a(j). (
r j * a j) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - aᵇPower
- g(j) raised to the power 2. (
g j ^ 2) - -Subtraction
- g(j)^2 minus 2 · a(j) · d · g(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
g j ^ 2 - 2 * a j * d * g j) - +Addition
- g(j)^2 − 2 · a(j) · d · g(j) plus a(j) · d^2. (
g j ^ 2 - 2 * a j * d * g j + a j * d ^…) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - ×Product
- Pairs of an element of J and an element of Bool. (
J × Bool) - Bool
- Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Bool) - ∏Product
- Multiply together r(f(i)).1 · a(f(i)).1 if f(i).2, else 1 − a(f(i)).1 for every i. (
∏ i, r (f i).1 * (if (f i).2 then a (f …) - p₁Component
- Component 1 of r(f(i)) (the first). (
r (f i).1) - { a if c; b otherwiseCases (if … then … else)
- a(f(i)).1 when f(i).2, and 1 − a(f(i)).1 otherwise. (
if (f i).2 then a (f i).1 else 1 - a (f…) - e.ffoldr
- foldr of ofFn(f): Lean's dot notation e.foldr means foldr applied to e. (
(List.ofFn f).foldr) - ofFn
- List.ofFn: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
List.ofFn) - x ↦ f(x)Function (λ-abstraction)
- The function sending z, tail to g(z.1) + 0 if z.2, else tail. Lean writes fun x => …; papers write x ↦ …. (
fun z tail => g z.1 + if z.2 then 0 els…) - a/bDivision
- ν divided by p. In Lean, dividing by 0 gives 0. (
ν / p)
theorem innov-finite-deadline-history {J : Type} [Fintype J] (r a g : J → ℝ) (p d ν : ℝ) (hr : ∀ j, 0 ≤ r j) (hrs : ∑ j, r j = 1) (ha : ∀ j, 0 ≤ a j ∧ a j ≤ 1) (hp : ∑ j, r j * a j = p) (hp0 : p ≠ 0) (hg : ∑ j, r j * g j = p * d) (hν : ∑ j, r j * (g j ^ 2 - 2 * a j * d * g j + a j * d ^ 2) = ν) :
∀ L : ℕ, (∀ f : Fin L → J × Bool, 0 ≤ ∏ i, r (f i).1 * (if (f i).2 then a (f i).1 else 1 - a (f i).1)) ∧ (∑ f : Fin L → J × Bool, ∏ i, r (f i).1 * (if (f i).2 then a (f i).1 else 1 - a (f i).1)) = 1 ∧ (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then a (f i).1 else 1 - a (f i).1)) * (List.ofFn f).foldr (fun z tail => g z.1 + if z.2 then 0 else tail) d) = d ∧ (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then a (f i).1 else 1 - a (f i).1)) * ((List.ofFn f).foldr (fun z tail => g z.1 + if z.2 then 0 else tail) d - d) ^ 2) = (1 - (1 - p) ^ L) * (ν / p)Defines finite independent key/acceptance path probabilities and the stopped reward fold with exact dense continuation at deadline; proves nonnegative normalized weights, exact mean and centered second moment for every finite deadline. No infinite-horizon measure-theoretic claim.
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
- 90 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.