pith. machine review for the scientific record. sign in
theorem proved term proof high

selfBootstrapCert

show as:
view Lean formalization →

The self-bootstrap certificate asserts that the meta-language distinguishes propositions and that the claim of carrier distinguishability differs from its negation. Researchers closing the absolute-floor program in Recognition Science cite it to complete Route A. The proof is a direct term construction that assembles the certificate by supplying the two required fields from prior theorems on propositional distinctions.

claimThere exists a self-bootstrap certificate consisting of the facts that the meta-language distinguishes propositions ($∃ P, Q : Prop, P ≠ Q$) and that for every type $K$, the statement $∃ x y : K, x ≠ y$ is not equal to its negation $¬(∃ x y : K, x ≠ y)$.

background

The module SelfBootstrapDistinguishability records the Lean-checkable part of the self-bootstrap argument for the absolute-floor program. It proves meta-level facts used by the argument: the formal language already distinguishes propositions, and the proposition asserting object-level distinguishability is distinct from its denial. It does not pretend to derive an object-level non-singleton carrier from nothing.

proof idea

The proof is a term-mode construction of the SelfBootstrapCert structure. It directly assigns the meta_distinguishes field to the theorem meta_language_distinguishes_props and the claim_not_its_negation field to dist_claim_self_distinguishes.

why it matters in Recognition Science

This theorem supplies the routeA field for absoluteFloorClosureCert, closing the absolute-floor program via the self-bootstrap route at the meta-language floor. It implements the module goal of recording theorem-backed meta-facts. In the Recognition framework it supports foundational closure without descending below the meta level, touching the question of how meta-distinguishability leads to object-level structure.

scope and limits

Lean usage

theorem absoluteFloorClosureCert : AbsoluteFloorClosureCert where routeA := selfBootstrapCert routeB := fun K _ => distinguishability_iff_nontrivial_specifiability (K := K) bool_witness := bool_absolute_floor

formal statement (Lean)

  81theorem selfBootstrapCert : SelfBootstrapCert where
  82  meta_distinguishes := meta_language_distinguishes_props

proof body

Term-mode proof.

  83  claim_not_its_negation := dist_claim_self_distinguishes
  84
  85end SelfBootstrap
  86end Foundation
  87end IndisputableMonolith

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.