SelfBootstrapCert
plain-language theorem explainer
SelfBootstrapCert records that the meta-language distinguishes distinct propositions and that the statement asserting object-level distinguishability differs from its own negation. Researchers closing the absolute floor argument via Route A cite it as the meta-level anchor. The structure definition directly encodes these two properties as a Prop-valued record with no additional proof obligations.
Claim. A proposition asserting the existence of distinct propositions $P$ and $Q$, together with the condition that for every type $K$ the statement asserting the existence of distinct elements in $K$ is not equal to its logical negation.
background
The module implements Route A of the absolute-floor program. It records the precise meta-level facts used by the self-bootstrap argument without deriving an object-level non-singleton carrier from nothing. The structure packages two facts: the formal language already distinguishes propositions, and the proposition asserting object-level distinguishability is distinct from its denial.
proof idea
The declaration is a structure definition with two fields. It is instantiated downstream by the theorem that applies the sibling lemmas meta_language_distinguishes_props and dist_claim_self_distinguishes.
why it matters
This supplies the routeA component of AbsoluteFloorClosureCert, completing the joint closure certificate. It closes the self-bootstrap route at the meta-language floor rather than below it, consistent with the framework's separation of meta and object levels before invoking the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.