phi_pow_11_eq
plain-language theorem explainer
The lemma establishes the exact algebraic identity for the eleventh power of the golden ratio as 89 times phi plus 55. Researchers deriving Recognition Science mass ratios would cite it to obtain the quark interval without approximation. The proof builds the result through successive calc chains that multiply prior power identities by phi and reduce via the square relation.
Claim. The golden ratio satisfies $phi^{11} = 89 phi + 55$.
background
The module proves rigorous bounds on Recognition Science predictions using only algebraic identities and rational arithmetic. The golden ratio phi obeys the defining relation phi squared equals phi plus one, quoted from upstream as the identity from the equation x squared minus x minus one equals zero. A second upstream result gives phi to the sixth equals eight phi plus five via the Fibonacci recurrence. The immediate predecessor supplies phi to the seventh equals thirteen phi plus eight.
proof idea
The proof obtains the square identity, the sixth-power identity, and the seventh-power identity. It then defines the eighth power by multiplying the seventh by phi, expanding, and reducing with the square relation to reach twenty-one phi plus thirteen. Parallel calc chains produce the ninth power as thirty-four phi plus twenty-one and the tenth as fifty-five phi plus thirty-four. The final calc multiplies the tenth by phi and reduces to obtain eighty-nine phi plus fifty-five.
why it matters
This identity is invoked directly by the downstream theorem that proves the open interval from 198 to 200 for phi to the eleventh, which the module table lists as the quark mass ratio m_c over m_u near 199. It completes one entry in the set of machine-verified numerical predictions that rely on the phi-ladder for mass formulas. The result sits inside the broader chain that derives all constants from the single functional equation without external inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.