lemma
proved
term proof
phi5_mul_phi5
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
165private lemma phi5_mul_phi5 : phi ^ (5 : ℝ) * phi ^ (5 : ℝ) = phi ^ (10 : ℝ) := by
proof body
Term-mode proof.
166 rw [← Real.rpow_add phi_pos]; norm_num
167
168/-- Fibonacci form of κ: κ = 8(5φ + 3).
169
170 Via φ⁵ = 5φ + 3 (Fibonacci identity: F₅=5, F₄=3, F₆=8):
171 κ = F₆ · (F₅ · φ + F₄) = 8 · (5φ + 3). -/
depends on (7)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use