pith. sign in
module module high

IndisputableMonolith.Foundation.RealityTerminalCategory

show as:
view Lean formalization →

RealityTerminalCategory constructs the terminal object in the category of distinguished carriers, each equipped with two named distinguishable points. It supplies the categorical endpoint that closes the forcing chain begun in RealityFromDistinction. Researchers tracing the Recognition Science derivation from a single distinction to spacetime would cite this module for its terminal-reality construction. The module proceeds via successive definitions of the carrier type, terminal arrows, and uniqueness certificates.

claimLet $\mathcal{C}$ be the category whose objects are carriers $K$ equipped with two distinct points $x,y\in K$. Then $\mathcal{C}$ admits a terminal object $\text{reality}$ together with a unique arrow from every object of $\mathcal{C}$ to $\text{reality}$.

background

The module imports RealityFromDistinction, whose doc-comment states that the master forcing-chain theorem follows from the bare proposition $\exists x y : K, x \neq y$ on any inhabited carrier $K$. It introduces the distinguished-carrier category whose objects are carriers with two named distinguishable points. Terminal arrows and the terminal reality object are defined inside this category, with existence and uniqueness lemmas establishing the terminal property.

proof idea

This is a definition module, no proofs. Successive definitions introduce DistinguishedCarrier, boolObject, TerminalArrow, terminalReality and RealityTerminalCert; the lemmas terminalArrow_exists, terminalArrow_unique and every_distinguished_carrier_maps_uniquely_to_reality then certify the terminal arrows.

why it matters in Recognition Science

The module feeds the root IndisputableMonolith, whose doc-comment describes the umbrella exposing the master forcing-chain theorem plus T-1 and foundation-repair surfaces. It supplies the terminal category that completes the chain from one distinction to a canonical reality object inside the Recognition Science framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)