boolObject
plain-language theorem explainer
boolObject supplies the Boolean type as the canonical minimal distinguished carrier. Researchers formalizing the terminal-object reading of the master theorem cite it as the base object from which every other distinguished carrier receives a unique morphism to the reality certificate. The definition is a direct structure instance that populates the four fields of DistinguishedCarrier using false, true, and the self-bootstrap distinguishability lemma.
Claim. Let $C$ be the category whose objects are distinguished carriers. The object $B$ is the distinguished carrier whose carrier type is the Boolean type, with base element false, witness element true, and the proof that false is distinct from true.
background
A DistinguishedCarrier is a structure consisting of a type Carrier together with two elements base and witness satisfying base ≠ witness. The module records the terminal-object reading of the master theorem: objects are inhabited carriers equipped with a named distinction, and a morphism from such an object to the terminal reality certificate is precisely the proof that its RealityCertificate exists. Such a morphism exists for every object by reality_from_one_distinction and is unique by proof irrelevance.
proof idea
This is a definition that directly instantiates the DistinguishedCarrier structure. It sets the Carrier field to Bool, the base field to false, the witness field to true, and the distinct field to the lemma SelfBootstrap.bool_distinguishable. No additional tactics or reductions are applied.
why it matters
The definition supplies the base object for terminalReality and realityTerminalCert. It realizes the universal property that every distinguished carrier maps uniquely to the same forced reality content, thereby closing the categorical formulation of the master theorem in the module. The construction anchors the claim that any distinguished carrier has the same propositional reality content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.