No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
28def KB : Kinematics α := { step := B.step }
proof body
Definition body.
29
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
Lean names referenced from this declaration's body.
-
Kinematics
in IndisputableMonolith.Causality.Basic
decl_use
-
Kinematics
in IndisputableMonolith.Causality.ConeBound
decl_use
-
Kinematics
in IndisputableMonolith.Causality.Reach
decl_use
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
Kinematics
in IndisputableMonolith.LedgerUniqueness
decl_use
-
Kinematics
in IndisputableMonolith.LightCone.StepBounds
decl_use