Re:Show HN: Lean4 proof that SSOT requires definition-time h...
by trissim on Thursday January 08, 2026 @03:35AM
(#46538730)
Fair point. I've added Ssot/Inconsistency.lean (zero sorry) which formalizes inconsistency as a Lean Prop, not a comment.
It proves ssot_required: if you need to encode the fact (DOF >= 1) and guarantee all configs are consistent, then DOF = 1. Also formalizes independence and oracle necessity (valid oracles can disagree -> resolution requires external choice).
The mapping to real systems still requires interpretation,but so does every formalization. The contribution is making assumptions explicit and attackable.
It proves ssot_required: if you need to encode the fact (DOF >= 1) and guarantee all configs are consistent, then DOF = 1. Also formalizes independence and oracle necessity (valid oracles can disagree -> resolution requires external choice).
The mapping to real systems still requires interpretation,but so does every formalization. The contribution is making assumptions explicit and attackable.