theorem
proved
gap45_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.RSCoupledAxis on GitHub at line 83.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
80/-- The gap-45 complexity ceiling. -/
81def gap45 : ℕ := 45
82
83theorem gap45_eq : gap45 = 45 := rfl
84
85end RSCoupledAxis
86end Foundation
87end IndisputableMonolith