TerminalArrow
The terminal arrow from a distinguished carrier to the terminal reality object is defined as the proposition that the carrier admits a reality certificate. Researchers formalizing the categorical packaging of the master theorem cite this when proving that all distinguished carriers share a unique mapping to the same terminal proposition. The definition reduces directly to the reality certificate structure via field projection on the carrier type.
claimFor a distinguished carrier $A$ (a type $K$ equipped with two distinct elements), the terminal arrow from $A$ is the proposition that $K$ admits a reality certificate.
background
A distinguished carrier is the structure consisting of a type together with two named distinct elements (base and witness) that model the minimal objects carrying a named distinction. The reality certificate on a nonempty type packages the existence of a non-trivial distinction, an absolute floor witness, and the law-of-logic realization interface. This module records the universal property that a morphism from any such carrier to the terminal reality object is precisely the proof that its reality certificate exists, following directly from the upstream result that every carrier with one distinction yields a reality certificate.
proof idea
This is a one-line definition that aliases the terminal arrow for a distinguished carrier to the reality certificate of its underlying carrier type. It performs only field projection from the distinguished carrier structure with no additional lemmas or tactics.
why it matters in Recognition Science
The definition supplies the morphism type used by the existence, uniqueness, and combined existence-uniqueness theorems that establish every distinguished carrier maps uniquely to the terminal reality certificate. It realizes the terminal-object reading of the master theorem by packaging the universal property that all carriers share the same forced reality content. The construction closes the categorical form of the chain without invoking full category-theory infrastructure.
scope and limits
- Does not define composition, identities, or other category operations.
- Does not prove existence of the terminal arrow.
- Does not apply to carriers lacking a named distinction.
- Does not reference the forcing chain, phi-ladder, or specific constants.
formal statement (Lean)
51def TerminalArrow (A : DistinguishedCarrier) : Prop :=
proof body
Definition body.
52 RealityCertificate A.Carrier
53
54/-- Every distinguished carrier has a terminal arrow. -/