every_distinguished_carrier_maps_uniquely_to_reality
plain-language theorem explainer
Every distinguished carrier admits a unique morphism to the terminal reality certificate, expressing that its reality content is forced and identical in the propositional sense. Constructions that assemble the universal terminal object cite this result directly. The proof is a one-line wrapper applying the packaged existence-and-uniqueness lemma for terminal arrows.
Claim. For every distinguished carrier $A$ (a type equipped with two distinct points), there exists a unique morphism $f$ from $A$ to the terminal object, where the morphism is the proposition asserting that the reality certificate of the underlying carrier of $A$ exists.
background
A distinguished carrier is a structure consisting of a carrier type together with two named points (base and witness) that are provably distinct. The terminal arrow from such a carrier is defined as the proposition RealityCertificate of its carrier type. This module records the universal property that every distinguished carrier maps uniquely into one and the same terminal reality certificate, which is the categorical packaging of the master theorem that reality follows from a single distinction.
proof idea
The proof is a one-line wrapper that applies the lemma terminalArrow_unique_exists to the given distinguished carrier A.
why it matters
This theorem supplies the universal property used to construct the reality terminal certificate in the same module. It completes the terminal-object reading of the master theorem, ensuring that all distinguished carriers share the same forced reality content. It touches the foundational step where distinction implies a unique reality certificate, consistent with the forcing chain from T0 to T8.
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."