Provednlightninglightningpr-14deep-formalization
An even TLV type cannot be an odd extension type
For all , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
Nat) - modRemainder
- The remainder when t is divided by 2. (
t % 2) - =Equality
- t % 2 and 0 are the same. (
t % 2 = 0) - ≠Not equal
- t % 2 and 1 are different. (
t % 2 ≠ 1)
theorem nlightning-even-tlv-not-odd (t : Nat) (evenType : t % 2 = 0) :
t % 2 ≠ 1Repository-grounded Lean formalization for NLightning PR #14. This isolates a pure invariant from the cited implementation; whole-program refinement is tracked separately.
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
- Quot.sound, propext
- Proof
- 6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.