DistinguishedCarrier
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not build the full Mathlib category-theory interface.
- Does not prove existence of RealityCertificate; that is supplied by an upstream lemma.
- Does not constrain the internal algebraic structure of the carrier type beyond the named distinction.
formal statement (Lean)
32structure DistinguishedCarrier where
33 Carrier : Type
34 base : Carrier
35 witness : Carrier
36 distinct : base ≠ witness
37
38instance (A : DistinguishedCarrier) : Nonempty A.Carrier := ⟨A.base⟩
proof body
Definition body.
39
40/-- The minimal distinguished carrier: `Bool`, with `false ≠ true`. -/