Provednlightninglightningpr-14deep-formalization
A reply to received STFU clears the initiator flag
What the notation means · or point at any symbol
- f(x)Function application
- ! applied to true. Lean writes f x; papers write f(x). (
!true) - =Equality
- !(true) and false are the same. (
!true = false) - true
- true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
true) - false
- false: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
false)
theorem nlightning-stfu-reply-noninitiator :
!true = falseRepository-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
- None
- Proof
- 6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.