phi_seventh_eq
plain-language theorem explainer
The lemma establishes φ^7 = 13φ + 8 as the next term in the Fibonacci recurrence for powers of the golden ratio. Researchers building the phi-ladder for RS-native constants and mass formulas cite it to advance the sequence. The proof is a short calc that multiplies the sixth-power identity by phi and reduces twice via the quadratic relation φ² = φ + 1.
Claim. $φ^7 = 13φ + 8$ where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The Constants module treats phi as the golden ratio, the positive root of x² - x - 1 = 0 forced as the self-similar fixed point in the UnifiedForcingChain (T6). It assembles a chain of power identities that obey the Fibonacci recurrence, consistent with the eight-tick octave (T7) and the fundamental RS time quantum τ₀ = 1 tick. This lemma sits after phi_sixth_eq, which records φ^6 = 8φ + 5, and draws on phi_sq_eq encoding the defining quadratic relation.
proof idea
The tactic proof uses a calc block. It rewrites φ^7 as φ times φ^6, applies phi_sixth_eq to obtain φ(8φ + 5), expands by ring, substitutes φ² = φ + 1 via phi_sq_eq, and finishes with a final ring simplification to 13φ + 8.
why it matters
The result feeds phi_eighth_eq, which continues the recurrence to φ^8 = 21φ + 13. These identities populate the phi-ladder that supplies mass formulas (yardstick times φ to a rung) and RS-native constants such as ħ = φ^{-5} and G = φ^5 / π. They support the forcing chain steps T6 through T8 that fix the eight-tick period and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.