terminalArrow_exists
plain-language theorem explainer
Every distinguished carrier admits a terminal arrow to the reality certificate. Researchers formalizing the categorical packaging of the master theorem cite this result for the existence half of the terminal-object property. The proof is a direct one-line application of reality_from_one_distinction to the carrier and its named distinction witness.
Claim. For every distinguished carrier $A$ (a type $K$ equipped with distinct elements $base$ and $witness$), the proposition $RealityCertificate(K)$ holds.
background
A DistinguishedCarrier is a structure consisting of a type Carrier together with two distinct points base and witness. TerminalArrow A is defined as the proposition RealityCertificate A.Carrier. The module records the terminal-object reading of the master theorem: objects are inhabited carriers with a named distinction, and a morphism to the terminal reality certificate is precisely a proof that RealityCertificate exists for that carrier. The key upstream result is reality_from_one_distinction, which states that any inhabited carrier K with at least one non-trivial distinction forces a RealityCertificate K containing the absolute-floor witness.
proof idea
This is a one-line term proof that applies reality_from_one_distinction directly to A.Carrier and the distinction triple formed by A.base, A.witness, and A.distinct.
why it matters
The declaration supplies the existence direction for the terminal arrow in the distinguished-carrier category. It is used by terminalArrow_unique_exists to obtain the packaged existence-and-uniqueness form and by terminalReality to define the terminal object on the minimal Bool carrier. It completes the categorical packaging of the master forcing chain from reality_from_one_distinction, where any distinction forces a reality certificate. This aligns with the framework's terminal reality certificate as the unique propositional target for all distinguished carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.