pith. machine review for the scientific record. sign in
def

eight_tick

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.DimensionForcing
domain
Foundation
line
110 · github
papers citing
1 paper (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 107abbrev Dimension := ℕ
 108
 109/-- The eight-tick period. -/
 110def eight_tick : ℕ := 8
 111
 112/-- Gap-45: the integration gap parameter D²(D+2) at D = 3. -/
 113def gap_45 : ℕ := 45
 114
 115/-- The synchronization period: lcm(8, 45) = 360. -/
 116def sync_period : ℕ := Nat.lcm eight_tick gap_45
 117
 118/-- Verify: lcm(8, 45) = 360. -/
 119theorem sync_period_eq_360 : sync_period = 360 := by
 120  unfold sync_period eight_tick gap_45; rfl
 121
 122/-! ## The 8-Tick Argument (Core Definition) -/
 123
 124/-- The eight-tick cycle is 2^D for dimension D. -/
 125def EightTickFromDimension (D : Dimension) : ℕ := 2^D
 126
 127/-- Derived ledger lower bound: every simplicial recognition loop has at least 8 ticks. -/
 128theorem simplicial_loop_tick_lower_bound
 129    (L : SimplicialLedger.SimplicialLedger)
 130    (cycle : List SimplicialLedger.Simplex3)
 131    (hloop : SimplicialLedger.is_recognition_loop cycle) :
 132    eight_tick ≤ cycle.length := by
 133  simpa [eight_tick] using SimplicialLedger.eight_tick_uniqueness L cycle hloop
 134
 135/-- 8 = 2^3, so eight-tick forces D = 3. -/
 136theorem eight_tick_is_2_cubed : eight_tick = 2^3 := rfl
 137
 138/-- If 2^D = 8, then D = 3. -/
 139theorem power_of_2_forces_D3 (D : Dimension) (h : 2^D = 8) : D = 3 := by
 140  match D with

papers checked against this theorem (showing 1 of 1)