SpecifiabilityClosureCert
plain-language theorem explainer
SpecifiabilityClosureCert packages the biconditional that a nonempty type K contains distinct elements precisely when a nontrivial specification exists on K. Researchers tracing Route B of the absolute-floor program cite it to anchor specifiability at the same level as a non-singleton carrier. The declaration is a structure definition whose single field directly records the equivalence proved by the sibling lemma distinguishability_iff_nontrivial_specifiability.
Claim. Let $K$ be a nonempty type. The specifiability closure certificate for $K$ is the proposition that there exist distinct $x,y:K$ if and only if there exists a nontrivial specification on $K$, where a nontrivial specification is a predicate on $K$ that holds for at least one element and fails for at least one element.
background
The module DistinguishabilityFromSpecifiability develops Route B of the absolute-floor program. Its central observation is that a non-trivial specification is equivalent to a non-singleton carrier: any framework that can specify an ontology with something inside and something outside already possesses the distinction required by the Law-of-Logic chain. NontrivialSpecification K is the structure that encodes this requirement via a predicate inOntology : K → Prop together with existence witnesses for an element inside and an element outside the predicate.
proof idea
SpecifiabilityClosureCert is a structure definition whose sole field is the named equivalence biconditional. The companion theorem specifiabilityClosureCert constructs an instance by supplying the lemma distinguishability_iff_nontrivial_specifiability as the witness for that field.
why it matters
The declaration supplies the Route B certificate that closes the specifiability-distinguishability loop inside the absolute-floor program. It is consumed by the theorem specifiabilityClosureCert, which packages the result for use in the foundation layer. The equivalence directly supports the claim that a non-singleton universe already encodes the minimal distinction needed for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.