`Dimension`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.DimensionForcing
domain: Foundation
line: 107 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 107.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 104/-! ## Basic Dimension Theory -/
 105
 106/-- Spatial dimension. -/
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.