`spatialDim`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.EightTickPeriodicityFromD
domain: Physics
line: 24 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.EightTickPeriodicityFromD on GitHub at line 24.

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

used by

formal source

  21
  22namespace IndisputableMonolith.Physics.EightTickPeriodicityFromD
  23
  24def spatialDim : ℕ := 3
  25def ledgerPeriod : ℕ := 2 ^ spatialDim
  26
  27theorem ledgerPeriod_eq_8 : ledgerPeriod = 8 := by decide
  28
  29/-- F(4) = 3 = spatialDim. -/
  30def F4 : ℕ := 3
  31theorem f4_eq_3 : F4 = 3 := rfl
  32theorem f4_eq_spatialDim : F4 = spatialDim := rfl
  33
  34/-- F(6) = 8 = ledgerPeriod. -/
  35def F6 : ℕ := 8
  36theorem f6_eq_8 : F6 = 8 := rfl
  37theorem f6_eq_ledgerPeriod : F6 = ledgerPeriod := by decide
  38
  39/-- Fibonacci recurrence: F(6) = F(5) + F(4). -/
  40def F5 : ℕ := 5
  41theorem fibonacci_recurrence : F6 = F5 + F4 := by decide
  42
  43/-- D and 2^D are both Fibonacci numbers at D=3. -/
  44theorem both_fibonacci_at_D3 : F4 = spatialDim ∧ F6 = ledgerPeriod := by
  45  exact ⟨rfl, by decide⟩
  46
  47/-- 8-tick and D=3 are connected by Fibonacci. -/
  48theorem eight_tick_fibonacci_connection : Nat.fib 6 = 8 := by decide
  49
  50structure EightTickCert where
  51  period_8 : ledgerPeriod = 8
  52  fibonacci_D : F4 = spatialDim ∧ F6 = ledgerPeriod
  53  fibonacci_rec : F6 = F5 + F4
  54

papers checked against this theorem

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