AbsoluteFloorClosureCert
plain-language theorem explainer
The absolute floor closure certificate packages a self-bootstrap certificate for meta-distinguishability, an equivalence between distinct elements in any inhabited type and the existence of a non-trivial specification on that type, and a concrete witness on Bool. Foundational work in Recognition Science cites this to close the absolute floor without introducing an extra physical postulate. The certificate is assembled directly from the self-bootstrap route, the distinguishability equivalence lemma, and the Boolean witness.
Claim. The absolute-floor closure certificate is the proposition consisting of a self-bootstrap certificate asserting meta-level distinguishability of propositions, the statement that for every inhabited type $K$ the existence of distinct elements in $K$ is equivalent to the non-emptiness of non-trivial specifications on $K$, and an absolute-floor witness for the Boolean type.
background
Recognition Science places an absolute floor below which no further physical postulates appear. An absolute-floor witness for an inhabited type $K$ requires meta-distinguishability of propositions together with the existence of a non-trivial specification on $K$. A non-trivial specification is a predicate on $K$ that holds for at least one element and fails for at least one other element. The self-bootstrap certificate closes the meta-language route by asserting distinguishability at the level of propositions and that the claim of distinct elements is not equivalent to its negation.
proof idea
The structure is populated directly by the self-bootstrap certificate, the equivalence between distinguishability and non-trivial specifiability, and the Boolean absolute-floor witness.
why it matters
This certificate closes the absolute floor in the foundation layer and is used by the theorem absoluteFloorClosureCert to assert that the certificate is theorem-backed. In the Recognition framework it confirms that the absolute floor follows from logical preconditions rather than an RS-specific postulate, aligning with the self-bootstrap route. No open questions are directly touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.