terminalReality
terminalReality supplies the terminal arrow from the minimal Boolean carrier into the reality certificate. Researchers formalizing the categorical master theorem cite it to witness that every distinguished carrier maps uniquely to the same proposition-shaped reality object. The definition is a direct one-line application of the existence lemma for terminal arrows.
claimLet $B$ be the distinguished carrier given by the Boolean type with its two distinct elements. There exists a morphism from $B$ to the terminal reality object, which is the proposition that $B$ admits a reality certificate.
background
This module records the universal property that every distinguished carrier maps uniquely to a single reality certificate. A distinguished carrier consists of an inhabited type together with a named distinction between two elements. TerminalArrow from such a carrier is defined to be exactly the proof that the carrier possesses a reality certificate.
proof idea
This is a one-line wrapper that applies the terminalArrow_exists lemma directly to boolObject.
why it matters in Recognition Science
It supplies the concrete terminal arrow required to build the RealityTerminalCert record, which packages the object, the terminal map, and the universal property. This completes the terminal-object reading of the master theorem, showing that forced reality content is independent of the choice of distinguished carrier. The construction relies on reality_from_one_distinction for existence and proof irrelevance for uniqueness.
scope and limits
- Does not construct a full Mathlib-style category theory interface.
- Does not prove existence of reality certificates from scratch.
- Does not address non-propositional aspects of reality certificates.
Lean usage
def exampleCert : RealityTerminalCert := realityTerminalCertformal statement (Lean)
77def terminalReality : TerminalArrow boolObject :=
proof body
Definition body.
78 terminalArrow_exists boolObject
79
80/-- Any distinguished carrier has the same forced reality content, in the
81categorical/propositional sense: there is a unique morphism from it to the
82terminal certificate. -/