distinguishability_iff_nontrivial_specifiability
plain-language theorem explainer
Non-trivial specifiability of a sub-ontology inside an inhabited carrier K is equivalent to K containing at least two distinct elements. Researchers closing the absolute-floor certificate cite this biconditional to equate Route B with bare distinguishability. The proof splits the iff via constructor, builds the specification structure forward from any pair of distinct elements, and applies the one-way upstream lemma in reverse.
Claim. For a nonempty type $K$, there exist distinct $x,y$ in $K$ if and only if there exists a nontrivial specification of a sub-ontology in $K$, i.e., a predicate on $K$ that holds for at least one element and fails for at least one other element.
background
The module DistinguishabilityFromSpecifiability supplies Route B for the absolute-floor program. A NontrivialSpecification on carrier $K$ is the structure consisting of a predicate inOntology : $K$ → Prop together with existential witnesses that the predicate holds for some element and fails for another. The module doc states that the ability to specify an ontology with something inside and something outside already supplies the distinction required by the Law-of-Logic chain.
proof idea
The tactic proof opens with constructor to split the biconditional. Forward, given distinct x and y, it builds the structure by setting inOntology to equality with x, using x for the inside witness and y for the outside witness after a short symmetry step. Reverse, it directly invokes the upstream lemma distinguishability_from_specification on the supplied specification structure.
why it matters
The theorem supplies the equivalence used inside absoluteFloorClosureCert to witness the absolute-floor closure via Route B. It is also invoked by absolute_floor_of_bare_distinguishability and bare_distinguishability_of_absolute_floor. It completes the Route B step that links object-level distinguishability to the foundational chain, directly supporting the absolute-floor closure certificate in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.