Machine-checked Lean 4 proofs for "Inconsistency Accumulation in Forward-Local Sequential Policies." Quantitative lower bound E[I_N] >= N/|U| with measure-theoretic verification via two independent proof paths, plus Proposition 1 summary sufficiency and Section 7 arithmetic witnesses.
theorem-proving lower-bounds formal-verification ai-safety mathlib measure-theory lean4 admissibility-dynamics inconsistency-accumulation delayed-constraints
-
Updated
May 19, 2026 - Lean