reality_from_bool
plain-language theorem explainer
The theorem shows that the Boolean type satisfies the full Reality-from-One-Distinction Certificate, so a single definitional distinction between false and true forces the absolute-floor witness, logic realization, spacetime emergence with Lorentzian signature, and the derived constants. Researchers tracing the Recognition Science forcing chain from bare distinguishability to physics would cite this as the smallest explicit model. The proof is a direct one-line application of the master theorem to Bool equipped with its definitional inequality.
Claim. The type $Bool$ satisfies the Reality-from-One-Distinction Certificate: there exist distinct elements $false, true$ in $Bool$, the absolute-floor witness exists on $Bool$, $Bool$ instantiates the logic-realization interface, and spacetime emerges with Lorentzian signature $(1,3)$.
background
The module RealityFromDistinction supplies the master forcing-chain theorem: from the bare proposition that an inhabited carrier $K$ admits at least one non-trivial distinction, the entire chain to the absolute floor, time as orbit, spacetime emergence, and the phi-derived constants follows. RealityCertificate is the structure that packages these deliverables: a distinction witness, the absolute-floor witness on $K$, the native logic-realization interface, the unconditional Bool floor, and the Lorentzian spacetime certificate. The upstream master theorem reality_from_one_distinction states that any inhabited $K$ with a distinction forces the absolute-floor witness on $K$, the canonical Bool floor, and the spacetime-emergence certificate.
proof idea
The proof is a one-line term wrapper that applies the master theorem reality_from_one_distinction to the carrier Bool, supplying the required distinction witness via the upstream result bool_distinguishable that false ≠ true.
why it matters
This declaration supplies the minimal concrete instance of the forcing chain, confirming that the Boolean carrier alone suffices to derive the full Recognition Science structure from distinction to spacetime and constants. It directly instantiates the master theorem in the RealityFromDistinction module and closes the base case of the T0-T8 chain. No open scaffolding remains at this leaf; downstream results in SpacetimeEmergence and ConstantDerivations inherit the certificate without further hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.