theorem proved term proof

`five_three_lt_two_seven`

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

formal statement (Lean)

  50theorem five_three_lt_two_seven : (5 : ℕ)^3 < 2^7 := by decide

Term-mode proof.

  51
  52/-- The information-bound theorem: 5^k < 2^(⌈k·log_2 5⌉ + 1) for small k. -/

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

productRecognitionLatticeCert in IndisputableMonolith.CrossDomain.ProductRecognitionLattice decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use