`derivation_status`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.Derivation
domain: Constants
line: 255 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Derivation on GitHub at line 255.

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

 252  unfold tau0 hbar_codata G_codata c_codata
 253  rfl
 254
 255def derivation_status : String :=
 256  "✓ tau0_sq_eq PROVEN\n" ++
 257  "✓ planck_relation_satisfied PROVEN\n" ++
 258  "✓ G_relation_satisfied PROVEN\n" ++
 259  "✓ tau0_planck_relation PROVEN\n" ++
 260  "✓ units_self_consistent PROVEN\n" ++
 261  "✓ NO PROOF HOLES"
 262
 263#eval derivation_status
 264
 265end
 266
 267end Derivation
 268end Constants
 269end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.