distinguishability_forced_given_object_witness
plain-language theorem explainer
Object-level distinguishability in a carrier type K is asserted exactly when the meta-language distinguishes propositions and the carrier is supplied as non-singleton. Researchers on the absolute-floor program cite it to close Route A at the meta level without deriving a non-singleton carrier from nothing. The proof is a one-line term that returns the supplied hypothesis verbatim.
Claim. Let $K$ be any type. Given that there exist distinct propositions $P$ and $Q$, and given that there exist distinct elements $x,y$ in $K$, it follows that there exist distinct elements $x,y$ in $K$.
background
The declaration lives in SelfBootstrapDistinguishability, the module that records the Lean-checkable fragment of Route A for the absolute-floor program. The module establishes meta-level facts used by the self-bootstrap argument: the formal language already distinguishes propositions, and the proposition asserting object-level distinguishability is distinct from its denial. The local setting explicitly names but does not derive the object-level non-singleton condition on the carrier.
proof idea
The proof is a one-line term that directly returns the hypothesis h_at_least_two_in_carrier. No lemmas from the depends_on list (K, A, self) are invoked; the term is an identity on the supplied witness.
why it matters
The result supplies the honest form of the Route A certificate, closing the self-bootstrap loop at the meta-language floor. It supports the SelfBootstrapCert construction recorded in the same module. Within the Recognition Science framework it secures the base non-singleton carrier required by the forcing chain T0-T8 without invoking the Recognition Composition Law, the phi-ladder, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.