Provedattentionresidual-seriesexternal-review-4
Residual series: exact finite-history key, value and completion counts
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 → ℝ) - ∑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
- ρ and 1 are different. (
ρ ≠ 1) - ∀For all
- The statement after the comma holds for every L. (
∀ L : ℕ, (∑ f : Fin L → J × Bool, (∏ i,…) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - 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 · ρ if f(i).2, else 1 − ρ for every i. (
∏ i, r (f i).1 * (if (f i).2 then ρ els…) - p₁Component
- Component 1 of r(f(i)) (the first). (
r (f i).1) - ·Multiplication
- r(f(i)).1 times ρ if f(i).2, else 1 − ρ. (
r (f i).1 * (if (f i).2 then ρ else 1 -…) - { a if c; b otherwiseCases (if … then … else)
- ρ when f(i).2, and 1 − ρ otherwise. (
if (f i).2 then ρ else 1 - ρ) - -Subtraction
- 1 minus ρ. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - ρ) - 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 1 + tail if z.2, else 0. Lean writes fun x => …; papers write x ↦ …. (
fun z (tail : ℝ) => 1 + if z.2 then tai…) - +Addition
- 1 plus tail if z.2, else 0. (
1 + if z.2 then tail else 0) - a/bDivision
- 1 − ρ^L divided by 1 − ρ. In Lean, dividing by 0 gives 0. (
(1 - ρ ^ L) / (1 - ρ)) - aᵇPower
- ρ raised to the power L. (
ρ ^ L) - ∧And
- Both hold: (∑ f, (∏ i, r(f(i)).1 · ρ if f(i).2, else 1 − ρ) · foldr(o…, and (∑ f, (∏ i, r(f(i)).1 · ρ if f(i).2, else 1 − ρ) · foldr(o…. (
(∑ f : Fin L → J × Bool, (∏ i, r (f i).…)
theorem residual-series-finite-access-counts {J : Type} [Fintype J] (r : J → ℝ) (ρ : ℝ) (hrs : ∑ j, r j = 1) (hρ : ρ ≠ 1) :
∀ L : ℕ, (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) * (List.ofFn f).foldr (fun z (tail : ℝ) => 1 + if z.2 then tail else 0) 0) = (1 - ρ ^ L) / (1 - ρ) ∧ (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) * (List.ofFn f).foldr (fun z (tail : ℝ) => if z.2 then tail else 1) 0) = 1 - ρ ^ L ∧ (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) * (List.ofFn f).foldr (fun z (tail : ℝ) => if z.2 then tail else 0) 1) = ρ ^ LDefines folds counting sampled keys, terminal sampled values and dense completion on the same finite product paths. Derives their exact weighted expectations; normalization is assumed through sum r=1. Probability nonnegativity and variance are established by the separate history target. No hardware traffic or latency claim.
How it was proved
- Proved
- 6 October 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
- 57 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.