DistinguishedCarrier
plain-language theorem explainer
DistinguishedCarrier packages a type together with two explicitly named distinct elements to serve as objects in the terminal reality category. Categorical formulations of the master theorem cite this structure when establishing that every such object admits a unique morphism to the terminal certificate. The declaration is a direct structure with four fields plus a derived Nonempty instance.
Claim. A distinguished carrier is a type $C$ equipped with elements $b,w : C$ such that $b ≠ w$.
background
The module records the universal property of the terminal reality certificate in categorical language. Objects are inhabited carriers that carry a named distinction; a morphism from such an object to the terminal object is exactly a proof that the carrier's RealityCertificate exists. The module imports RealityFromDistinction to obtain the underlying existence result reality_from_one_distinction.
proof idea
The declaration is a structure definition that directly introduces the four fields Carrier, base, witness and distinct together with the Nonempty instance generated from base.
why it matters
DistinguishedCarrier supplies the objects for the terminal-arrow construction used by every_distinguished_carrier_maps_uniquely_to_reality and RealityTerminalCert. These results realize the categorical reading of the master theorem: any distinguished carrier maps uniquely into the same forced reality certificate. The setup deliberately avoids the full Mathlib category-theory library and works only with the propositional content of RealityCertificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.