sync_period

formal source

 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
 141  | 0 => norm_num at h
 142  | 1 => norm_num at h
 143  | 2 => norm_num at h
 144  | 3 => rfl
 145  | n + 4 =>
 146    have h16 : 2^(n+4) ≥ 16 := by