`absoluteFloorClosureCert`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.AbsoluteFloorClosure
domain: Foundation
line: 75 · github
papers citing: 3 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.AbsoluteFloorClosure on GitHub at line 75.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  72  bool_witness : AbsoluteFloorWitness Bool
  73
  74/-- The absolute-floor closure certificate is theorem-backed. -/
  75theorem absoluteFloorClosureCert : AbsoluteFloorClosureCert where
  76  routeA := selfBootstrapCert
  77  routeB := fun K _ => distinguishability_iff_nontrivial_specifiability (K := K)
  78  bool_witness := bool_absolute_floor
  79
  80end AbsoluteFloorClosure
  81end Foundation
  82end IndisputableMonolith

papers checked against this theorem (showing 3 of 3)

Dynamically generated Xi(1690) fits J/psi decay data
unclear · 2603.16640

"We employ the chiral unitary approach with the coupled channels πΞ, K̄Λ, K̄Σ, and ηΞ... cutoff method with q_max=630 MeV"
Condensed fundamental group of Spec(Z) is non-trivial
unclear · 2605.10358

"We extend the study of the condensed Galois category of a scheme introduced by Barwick, Glasman and Haine... provide a description in terms of w-contractible rings... compute a formula for the (underlying group of the) condensed fundamental group of a general Dedekind domain"
Integer transfer rules solve conservation laws exactly
echoes · 2604.06947

"Lemma 2.8 (Discrete Green/Stokes identity... total discrete mass is exactly conserved)"