absolute_floor_of_bare_distinguishability
plain-language theorem explainer
Bare distinguishability on a nonempty type K yields the absolute-floor witness because the given distinction maps to nontrivial specifiability via the equivalence lemma while meta-distinguishability of propositions is supplied by the meta-language result. Workers closing the forcing chain from one distinction to the RealityCertificate would cite this to discharge the absolute-floor obligation. The proof is a direct term that builds the witness structure by applying the equivalence map and referencing the meta-language theorem.
Claim. Let $K$ be a nonempty type. If there exist distinct elements $x,y$ in $K$, then $K$ admits an absolute-floor witness: propositions are distinguishable in the meta-language and $K$ admits a nonempty collection of nontrivial specifications.
background
The absolute-floor witness on a nonempty type $K$ is the structure requiring two properties: meta-language distinguishability of distinct propositions, and the existence of a nonempty set of nontrivial specifications on $K$. The module shows that this witness is equivalent to bare distinguishability on an inhabited carrier, so the absolute floor reduces to a logical precondition of a non-singleton universe rather than an RS-specific physical postulate. This step rests on the upstream equivalence that non-trivial specifiability is equivalent to object-level distinguishability on an inhabited carrier, together with the meta-language result that propositions are distinguishable.
proof idea
The proof constructs the AbsoluteFloorWitness structure in a single term. It supplies the meta_distinguishes field by direct reference to the meta-language distinguishability theorem and obtains the nontrivial_specifiable field by applying the forward map of the distinguishability_iff_nontrivial_specifiability equivalence to the supplied distinction hypothesis.
why it matters
This theorem supplies one direction of the equivalence between bare distinguishability and the absolute-floor witness, feeding the iff statement, the Bool realization, and the master forcing chain in reality_from_one_distinction. The latter derives the full spacetime-emergence certificate (Lorentzian signature, light cone, etc.) from any single distinction on an inhabited carrier. In the Recognition framework the result reduces the absolute floor to meta-language proposition distinguishability plus a non-singleton universe of discourse, confirming that no additional RS-specific postulate is required at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.