terminalArrow_unique_exists
plain-language theorem explainer
Every distinguished carrier admits a unique terminal arrow to the reality object. Workers formalizing the categorical structure of Recognition Science cite this when invoking the universal property of the terminal reality certificate. The proof is a term construction that pairs the separate existence lemma with the uniqueness lemma via refinement.
Claim. For every distinguished carrier $A$ (a type equipped with two distinct points), there exists a unique $f$ such that $f$ is a terminal arrow from $A$, meaning $f$ is a proof that the carrier of $A$ admits a reality certificate.
background
A distinguished carrier is a structure consisting of a type together with two named points (base and witness) satisfying base ≠ witness. The terminal arrow from such a carrier is defined to be the proposition RealityCertificate applied to its underlying type. The module encodes a minimal categorical reading in which objects are these carriers and morphisms to the terminal reality object are precisely the proofs that a reality certificate exists for the carrier.
proof idea
The term proof refines a triple consisting of the existence witness supplied by terminalArrow_exists, the trivial proposition, and a uniqueness argument. The uniqueness step applies terminalArrow_unique to an arbitrary arrow and the existence witness already obtained.
why it matters
This packages the existence-and-uniqueness form required by the parent theorem every_distinguished_carrier_maps_uniquely_to_reality. It realizes the terminal-object reading of the master theorem: every distinguished carrier maps uniquely into the same forced reality certificate, with uniqueness following from proof irrelevance on the propositional RealityCertificate. The construction stays within the Recognition framework without importing full category-theory machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.