bool_distinguishable
plain-language theorem explainer
Bool distinguishes its two values definitionally. Absolute-floor arguments in the Recognition Science foundation cite this to fix the minimal carrier. A decide tactic confirms the inequality by direct computation.
Claim. In the Boolean type, the elements false and true are distinct: $false ≠ true$.
background
SelfBootstrapDistinguishability records the Lean-checkable meta-level facts for the self-bootstrap argument. The module establishes that the formal language distinguishes propositions and that the proposition asserting object-level distinguishability differs from its denial. The two-element Boolean type serves as the minimal carrier with a definitional distinction between its elements.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the decidable proposition false ≠ true.
why it matters
This theorem supplies the witness for the absolute floor in bool_absolute_floor and enables the reality certificate in reality_from_bool. It grounds the self-bootstrap distinguishability route, providing the smallest distinguished carrier Bool for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.