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)
310theorem rung_offset_is_two_8tick_cycles : rung_offset = 2 * 8 := by native_decide
proof body
Term-mode proof.
311
312/-- The conjectured galactic radius rung.
313 N_r = N_τ - 16 = 142 - 16 = 126 -/
depends on (7)
Lean names referenced from this declaration's body.
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
radius
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
rung_offset
in IndisputableMonolith.Gravity.GravityParameters
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use