theorem proved term proof

`selfBootstrapCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  81theorem selfBootstrapCert : SelfBootstrapCert where
  82  meta_distinguishes := meta_language_distinguishes_props

Term-mode proof.

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

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

absoluteFloorClosureCert in IndisputableMonolith.Foundation.AbsoluteFloorClosure decl_use

Lean names referenced from this declaration's body.

dist_claim_self_distinguishes in IndisputableMonolith.Foundation.SelfBootstrapDistinguishability decl_use
meta_language_distinguishes_props in IndisputableMonolith.Foundation.SelfBootstrapDistinguishability decl_use
SelfBootstrapCert in IndisputableMonolith.Foundation.SelfBootstrapDistinguishability decl_use