def definition def or abbrev

`dimensions_status`

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

formal statement (Lean)

 117def dimensions_status : String :=

proof body

Definition body.

 118  "✓ Dimension structure [L, T, M] defined\n" ++
 119  "✓ Physical constant dimensions (c, ℏ, G) specified\n" ++
 120  "✓ Planck unit dimensions documented\n" ++
 121  "✓ τ₀ dimension documented as [T]\n" ++
 122  "✓ DimensionedQuantity algebra defined"
 123
 124#eval dimensions_status
 125
 126end Dimensions
 127end Constants
 128end IndisputableMonolith

depends on (19)

Lean names referenced from this declaration's body.

Physical in IndisputableMonolith.Bridge.DataCore decl_use
G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
Dimension in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
Dimension in IndisputableMonolith.Foundation.DimensionForcing decl_use
eval in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use
eval in IndisputableMonolith.Relativity.Fields.Scalar decl_use