Provednlightninglightningpr-14deep-formalization

A quiescence STFU is never owed after local STFU was sent

For all $\htmlData{mx=1}{\mathit{pending}, \mathit{received} \in \htmlData{mx=0}{\operatorname{Bool}}}$ :

\htmlData{mx=2}{(\htmlData{mx=1}{\mathtt{!}(\htmlData{mx=0}{\operatorname{true}})})(\mathtt{\&\&\ (pending\ ||\ received))\ =\ false})}

What the notation means · or point at any symbol

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)
x ∈ TVariables: pending, received range over Bool: the statement must hold for every choice. ((pending received : Bool))
f(x)Function application: ! applied to true. Lean writes f x; papers write f(x). (!true)
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)

theorem nlightning-stfu-not-owed-after-send (pending received : Bool) :
    (!true && (pending || received)) = false

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: propext
Proof: 6 lines of Lean

A quiescence STFU is never owed after local STFU was sent

How it was proved

More proved statements