simplicial_loop_tick_lower_bound

formal source

 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
 147      have : 2^n ≥ 1 := Nat.one_le_pow n 2 (by norm_num)
 148      calc 2^(n+4) = 2^n * 2^4 := by ring
 149        _ ≥ 1 * 16 := by nlinarith
 150        _ = 16 := by ring
 151    rw [h] at h16
 152    norm_num at h16
 153
 154/-- The eight-tick cycle forces D = 3. -/
 155theorem eight_tick_forces_D3 (D : Dimension) :
 156    EightTickFromDimension D = eight_tick → D = 3 := by
 157  intro h
 158  unfold EightTickFromDimension eight_tick at h