theorem proved term proof

`absoluteFloorClosureCert`

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

formal statement (Lean)

  75theorem absoluteFloorClosureCert : AbsoluteFloorClosureCert where
  76  routeA := selfBootstrapCert

proof body

Term-mode proof.

  77  routeB := fun K _ => distinguishability_iff_nontrivial_specifiability (K := K)
  78  bool_witness := bool_absolute_floor
  79
  80end AbsoluteFloorClosure
  81end Foundation
  82end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
AbsoluteFloorClosureCert in IndisputableMonolith.Foundation.AbsoluteFloorClosure decl_use
bool_absolute_floor in IndisputableMonolith.Foundation.AbsoluteFloorClosure decl_use
distinguishability_iff_nontrivial_specifiability in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
selfBootstrapCert in IndisputableMonolith.Foundation.SelfBootstrapDistinguishability decl_use