RealityTerminalCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Geometry rebuilt as a quotient of what measurements can distinguish
"RG is intentionally positioned at the intersection of several measurement-first programs ... a minimal axiom system for recognition-first models, a canonical quotient construction for observable space, a finite-resolution axiom (RG3), and comparative recognizers (RG4) as a route toward emergent order and distance."