[hanslub42]

All the heavy lifting is done by the comments. For example: theorem dof_gt_one_inconsistent (dof : Nat) (h : dof > 1) dof ≠ 1 (in Basic.lean) is the well-known fact that any number > 1 is unequal to 1.

But the comment states: DOF > 1 implies potential inconsistency. Inconsistency of what? Lean doesn't know, or care....

[trissim]

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.