`phi5_fibonacci`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.NumberTheoryFromRS
domain: Mathematics
line: 34 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.NumberTheoryFromRS on GitHub at line 34.

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

depends on

used by

formal source

  31theorem phi_sq_identity : phi ^ 2 = phi + 1 := phi_sq_eq
  32
  33/-- φ^5 = 5φ+3 (Fibonacci). -/
  34theorem phi5_fibonacci : phi ^ 5 = 5 * phi + 3 := by
  35  have h2 := phi_sq_eq
  36  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  37  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  38  nlinarith
  39
  40/-- φ^8 = 21φ+13 (Fibonacci). -/
  41theorem phi8_fibonacci : phi ^ 8 = 21 * phi + 13 := by
  42  have h2 := phi_sq_eq
  43  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  44  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  45  nlinarith [sq_nonneg (phi ^ 4)]
  46
  47/-- gap45 = D²(D+2) at D=3. -/
  48theorem gap45_from_D : 3 ^ 2 * (3 + 2) = 45 := by decide
  49
  50/-- 5 key RS number-theoretic identities. -/
  51def rsKeyIdentityCount : ℕ := 5
  52theorem rsi_count_five : rsKeyIdentityCount = 5 := rfl
  53
  54structure NumberTheoryCert where
  55  phi_sq : phi ^ 2 = phi + 1
  56  phi5 : phi ^ 5 = 5 * phi + 3
  57  phi8 : phi ^ 8 = 21 * phi + 13
  58  gap45_D : 3 ^ 2 * (3 + 2) = 45
  59  five_identities : rsKeyIdentityCount = 5
  60
  61noncomputable def numberTheoryCert : NumberTheoryCert where
  62  phi_sq := phi_sq_identity
  63  phi5 := phi5_fibonacci
  64  phi8 := phi8_fibonacci

papers checked against this theorem

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