Provednlightninglightningpr-14deep-formalization
BOLT 12 signature fields are disjoint from offer fields
For all :
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
Nat) - ⟹Implies
- If 240 ≤ t ∧ t ≤ 1000, then ¬(1 ≤ t ∧ t ≤ 79 ∨ 1000000000 ≤ t ∧ t ≤ 1999999999). (Between types, A → B is the type of functions from A to B.) (
(240 ≤ t ∧ t ≤ 1000) → ¬ ((1 ≤ t ∧ t ≤ …) - ≤At most
- 240 is less than or equal to t. (
240 ≤ t) - ∧And
- Both hold: 240 ≤ t, and t ≤ 1000. (
240 ≤ t ∧ t ≤ 1000) - ¬Not
- It is not the case that 1 ≤ t ∧ t ≤ 79 ∨ 1000000000 ≤ t ∧ t ≤ 1999999999. (
¬ ((1 ≤ t ∧ t ≤ 79) ∨ (1000000000 ≤ t ∧…) - ∨Or
- At least one holds: 1 ≤ t ∧ t ≤ 79, or 1000000000 ≤ t ∧ t ≤ 1999999999. (
(1 ≤ t ∧ t ≤ 79) ∨ (1000000000 ≤ t ∧ t …)
theorem nlightning-signature-range-disjoint-offer (t : Nat) :
((240 ≤ t ∧ t ≤ 1000) → ¬ ((1 ≤ t ∧ t ≤ 79) ∨ (1000000000 ≤ t ∧ t ≤ 1999999999)))Repository-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.