`F5`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.EightTickPeriodicityFromD
domain: Physics
line: 40 · 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 40.

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

  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
  55def eightTickCert : EightTickCert where
  56  period_8 := ledgerPeriod_eq_8
  57  fibonacci_D := both_fibonacci_at_D3
  58  fibonacci_rec := fibonacci_recurrence
  59
  60end IndisputableMonolith.Physics.EightTickPeriodicityFromD

papers checked against this theorem

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