def definition def or abbrev

`derivation_status`

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

formal statement (Lean)

 255def derivation_status : String :=

proof body

Definition body.

 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

depends on (8)

Lean names referenced from this declaration's body.

G_relation_satisfied in IndisputableMonolith.Constants.Derivation decl_use
planck_relation_satisfied in IndisputableMonolith.Constants.Derivation decl_use
tau0_planck_relation in IndisputableMonolith.Constants.Derivation decl_use
tau0_sq_eq in IndisputableMonolith.Constants.Derivation decl_use
units_self_consistent in IndisputableMonolith.Constants.Derivation decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
eval in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge decl_use
eval in IndisputableMonolith.Relativity.Fields.Scalar decl_use