RealityTerminalCert
RealityTerminalCert bundles a distinguished carrier with its terminal morphism to the reality certificate and the universal property that every distinguished carrier admits a unique such morphism. A physicist invoking the categorical master theorem would cite it to assert that all distinctions collapse to one forced reality content. The declaration is a structure definition that directly assembles the three fields from sibling definitions without a separate proof body.
claimA structure consisting of a distinguished carrier $A$, a terminal arrow from $A$ (defined as the proposition that the reality certificate exists for the underlying type of $A$), and the universal property that for every distinguished carrier $B$ there exists a unique terminal arrow from $B$.
background
The RealityTerminalCategory module records the terminal-object reading of the master theorem. DistinguishedCarrier is the structure with a type, two distinct points (base and witness), and the inequality base ≠ witness. TerminalArrow A is the proposition RealityCertificate A.Carrier, i.e., the existence of the forced reality content for that carrier. The module states that a morphism to the terminal reality certificate is precisely such a proof, that the morphism exists for every distinguished carrier by reality_from_one_distinction, and that it is unique by proof irrelevance since RealityCertificate is a proposition.
proof idea
This is a structure definition with an empty proof body. The object field is supplied by any DistinguishedCarrier, the terminal field by the definition of TerminalArrow, and the universal field by the sibling lemma that proves terminalArrow_unique_exists for every distinguished carrier.
why it matters in Recognition Science
The structure supplies the terminal certificate that feeds the downstream construction realityTerminalCert, which instantiates it on the boolean object. It completes the categorical form of the master theorem described in the module documentation, confirming that every distinguished carrier maps uniquely into the same forced reality. In the Recognition framework this supports the forcing chain by establishing uniqueness of the reality terminal, consistent with J-uniqueness and the self-similar fixed point.
scope and limits
- Does not construct a full category-theory interface.
- Does not prove existence of reality certificates.
- Does not apply to carriers without a named distinction.
- Does not derive numerical values or physical constants.
Lean usage
def realityTerminalCert : RealityTerminalCert where object := boolObject terminal := terminalReality universal := every_distinguished_carrier_maps_uniquely_to_realityformal statement (Lean)
90structure RealityTerminalCert where
91 object : DistinguishedCarrier
92 terminal : TerminalArrow object
93 universal :
94 ∀ A : DistinguishedCarrier, ∃! f : TerminalArrow A, True
95