RealityCertificate
plain-language theorem explainer
RealityCertificate packages the forcing chain from one non-trivial distinction in any inhabited carrier K into a single Prop structure. Physicists tracing spacetime and constants back to logic would cite it as the central bundled deliverable. The definition enumerates witnesses for absolute floor, spacetime emergence with Lorentzian signature and light cone, time orbit, and phi-powered constants, each drawn from prior theorems.
Claim. A structure certifying reality emergence on an inhabited carrier $K$ requires: existence of distinct elements $x,y$ in $K$; a nonempty absolute-floor witness on $K$; a nonempty logic-realization interface; the absolute-floor witness on Bool; a nonempty spacetime-emergence certificate with Lorentzian signature; the light-cone null condition (interval $v=0$ iff spatial norm squared equals temporal squared); a nonempty time-as-orbit certificate; causal speed $c=1$; and both Planck's constant and Newton's constant as integer powers of the golden ratio on the recognition ladder.
background
The module assembles the master forcing chain that begins with the bare hypothesis of a non-trivial distinction and terminates in spacetime, time as orbit, and the physical constants. AbsoluteFloorWitness supplies the minimal non-empty floor on any distinguished carrier; SpacetimeEmergenceCert encodes Lorentzian signature together with the light-cone classification; TimeAsOrbitCert identifies Tick with the Lawvere natural-number object. ConstantDerivations records the derivations of $c$, $hbar$, and $G$ as phi-powers. The local setting is pure glue: every field is already proved in an upstream module and is merely threaded here.
proof idea
The declaration is a structure definition whose fields are populated by direct reference to upstream theorems. No tactics or reductions occur inside the structure itself; each witness is supplied by the corresponding theorem in AbsoluteFloorClosure, UniversalInstantiationFromDistinction, TimeAsOrbit, SpacetimeEmergence, or ConstantDerivations.
why it matters
RealityCertificate is the single named object that collects every conclusion of the T0-T8 forcing chain once a distinction is granted. It is used directly by reality_from_one_distinction to construct the certificate on an arbitrary carrier, by reality_from_bool on the minimal Bool carrier, and by reality_forced_by_any_distinction in propositional form. The structure therefore realizes the Recognition Science claim that spacetime, the light cone, unit causal speed, and the phi-ladder constants follow from the Recognition Composition Law and the eight-tick octave without additional physical postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.