bool_distinction
plain-language theorem explainer
There exist two unequal Boolean values: false and true. Foundation work cites this as the canonical Boolean distinction witness that discharges the Boolean slot of the T−1 floor. The proof is a one-line existential term pairing false with true and invoking Bool.noConfusion.
Claim. There exist Boolean values $x, y$ such that $x \neq y$.
background
The module T−1 Forced from a Distinction takes as primitive a distinction witness $\exists x, y : K,, x \neq y$, rather than an external admissibility package. From any such witness it constructs a marked pair, the Boolean projection generated by the distinction, the observable equivalence, the two-class quotient, uniqueness of Boolean coordinates up to automorphism, and the legacy raw floor required by RealityCertificate.
The strong thesis is that once an object-level distinction is supplied, the entire Boolean/observable floor is forced; nothing extra is assumed. The present declaration is the base Boolean instance of that witness: the type Bool itself already carries two unequal inhabitants.
Downstream, the NothingToDistinction certificate packages several distinction layers (universe population, type, Prop, object, and Bool) that together discharge the meta-precondition of the prior floor.
proof idea
Term-mode existential introduction. The witness pair is false and true; inequality is discharged by Bool.noConfusion, the standard injectivity/no-confusion principle for the Boolean constructors. No intermediate lemmas are required.
why it matters
This is the canonical Boolean distinction witness named in the module's construction list. It fills the bool_distinction field of NothingToDistinctionCert, whose doc-comment states the joint claim: from the encoding of absolute nothing, the universe is populated, type/propositional/object distinctions hold, and the prior floor's meta-precondition is discharged. The certificate theorem nothingToDistinctionCert wires an analogous Boolean witness into that structure.
In the Recognition forcing chain this sits below T0–T8: it is part of the T−1 repair that makes the Boolean/observable floor forced by distinction rather than postulated. Without a Boolean distinction there is no two-class quotient or forced Boolean projection for the later J-cost and eight-tick machinery to stand on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.