SpecifiabilityClosureCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any concrete nontrivial specification.
- Does not identify the type K with the physical constant K = φ^{1/2}.
- Does not address computability or empirical content of specifications.
- Does not extend the statement to continuous or measure-theoretic carriers.
Lean usage
theorem specifiabilityClosureCert (K : Type*) [Nonempty K] : SpecifiabilityClosureCert K where equivalence := distinguishability_iff_nontrivial_specifiabilityformal statement (Lean)
91structure SpecifiabilityClosureCert (K : Type*) [Nonempty K] : Prop where
92 equivalence :
93 (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K)
94
95/-- The specifiability closure certificate is theorem-backed. -/