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)
320theorem fibonacci_mass_recursion (y : ℝ) (n : ℕ) :
321 y * phi ^ (n + 2) = y * phi ^ (n + 1) + y * phi ^ n := by
proof body
Term-mode proof.
322 rw [phi_fibonacci_recursion]; ring
323
324/-- The ratio of consecutive masses = φ. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
-
fibonacci_triple_sum
in IndisputableMonolith.Unification.QuantumGravityOctaveDuality
decl_use
-
qg_octave_cert
in IndisputableMonolith.Unification.QuantumGravityOctaveDuality
decl_use
depends on (6)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
phi_fibonacci_recursion
in IndisputableMonolith.Unification.QuantumGravityOctaveDuality
decl_use