boolObject
plain-language theorem explainer
The boolObject definition supplies the minimal distinguished carrier by instantiating the Boolean type with false as base and true as witness. Researchers formalizing the terminal-object reading of the master theorem cite this as the concrete base case. The construction directly populates the DistinguishedCarrier record by invoking the bool_distinguishable result for the inequality.
Claim. The minimal distinguished carrier is the type $Bool$ equipped with base element $false$, witness element $true$, and the proof that $false ≠ true$.
background
DistinguishedCarrier is the structure whose objects are types equipped with two named points base and witness satisfying base ≠ witness; the module records the terminal-object form of the master theorem in which a morphism from any such carrier to the terminal reality certificate is exactly the existence proof of its RealityCertificate. Every distinguished carrier admits a unique arrow to the same terminal object by reality_from_one_distinction together with proof irrelevance of propositions. The upstream bool_distinguishable lemma from SelfBootstrapDistinguishability supplies the concrete inequality needed for the Boolean case.
proof idea
Direct record construction that sets Carrier to Bool, base to false, witness to true, and distinct to the bool_distinguishable theorem.
why it matters
This definition supplies the concrete terminal object that feeds terminalReality and realityTerminalCert, thereby anchoring the categorical statement that every distinguished carrier maps uniquely to the forced reality certificate. It closes the terminal-object reading of the master theorem inside the Recognition Science framework and supplies the base case for the universal property used in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.