theorem proved tactic proof

`phi8_fibonacci`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  39theorem phi8_fibonacci : phi ^ 8 = 21 * phi + 13 := by

proof body

Tactic-mode proof.

  40  have h2 := phi_sq_eq
  41  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  42  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  43  nlinarith [sq_nonneg (phi ^ 4)]
  44
  45/-- φ^8 > 46 (proved separately). -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

numberTheoryCert in IndisputableMonolith.Mathematics.NumberTheoryFromRS decl_use
phi8_fibonacci in IndisputableMonolith.Mathematics.NumberTheoryFromRS decl_use
coherenceTimeCert in IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost decl_use
phi12_gt_300 in IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost decl_use
phi8_gt_46 in IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost decl_use

depends on (3)

Lean names referenced from this declaration's body.

phi_sq_eq in IndisputableMonolith.Constants decl_use
phi8_fibonacci in IndisputableMonolith.Mathematics.NumberTheoryFromRS decl_use
phi_sq_eq in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use