|
|
|
|
|
|
by trissim
163 days ago
|
|
|
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. |
|
|