reality_forced_by_any_distinction
plain-language theorem explainer
From the existence of any inhabited type admitting at least one distinction, the framework derives nonemptiness of the spacetime emergence certificate, nonemptiness of the time-as-orbit certificate, and equality of the derived reality constant to one. Researchers tracing the single-hypothesis forcing chain from distinction to physical structure would cite this master theorem. The proof is a direct term refinement to three pre-established nonemptiness and equality results from upstream modules.
Claim. If there exists a type $K$ that is nonempty and contains distinct elements $x,y$ with $x≠y$, then the spacetime emergence certificate is nonempty, the time-as-orbit certificate is nonempty, and the derived constant $c_{rs}$ equals 1.
background
The RealityFromDistinction module supplies the master forcing-chain theorem: from the bare proposition that some inhabited carrier $K$ admits a distinction, the chain reaches spacetime, the light cone, time as canonical orbit, and the φ-derived constants. It threads the absolute-floor closure theorem, the K-native instantiation theorem, the time-as-orbit theorem, the spacetime-emergence theorem, and the constant-derivation theorem. The module documentation states that every link is already proved elsewhere and that this module is pure glue making the chain visible at one named place.
proof idea
The term proof introspects the existential hypothesis on the carrier and distinction. It then refines directly to the triple of spacetime_emergence_cert_nonempty, timeAsOrbitCert_inhabited, and ConstantDerivations.c_rs_eq_one. The comment in the body notes that the target claims are realisation-free and require no further use of the specific carrier K.
why it matters
This theorem is the explicit Lean witness for the master forcing theorem that records a single named object whose statement is 'from one distinction, all of reality is forced.' It fills the propositional form of the chain described in the module documentation and connects absolute-floor closure through spacetime emergence and constant derivations. The proof body lists open follow-ups: wiring the CompleteForcingChain from UnifiedForcingChain and extending the result with the Recognition Composition Law to produce the full physics tower.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.