frequency_ratio
plain-language theorem explainer
The theorem proves that consecutive plasmon frequencies on the phi-ladder stand in the exact ratio phi. Researchers modeling plasmonic modes inside Recognition Science would cite it to confirm the geometric progression of the five canonical mode frequencies. The proof is a short algebraic reduction that unfolds the exponential definition, invokes positivity of powers, rewrites the quotient, and cancels via ring.
Claim. Let $f(k) := phi^k$ for $k : ℕ$. Then $f(k+1) / f(k) = phi$.
background
The module treats five plasmonic mode types (surface plasmon polariton, localized surface plasmon, propagating, bulk, gap) whose frequencies occupy successive rungs of the phi-ladder. The supporting definition states that plasmonFrequency(k) equals phi raised to k, supplying the exponential scaling required by the Recognition Science self-similar fixed point. This construction sits inside the broader forcing chain in which phi is forced as the unique positive solution greater than one to the fixed-point equation.
proof idea
Unfold plasmonFrequency to replace both occurrences by powers of phi. Introduce the positivity fact (0 < phi^k) to license division rewriting. Apply the successor power rule to obtain phi * phi^k / phi^k. The ring tactic then cancels the common factor and yields phi.
why it matters
The result populates the phi_ratio field of PlasmonicModeCert, the structure that certifies the five modes together with their count and positivity. It thereby anchors the frequency scaling to the same phi that appears in the mass formula on the phi-ladder and in the eight-tick octave of the forcing chain. The module records zero sorry, closing the algebraic consistency check for this layer of the plasmonic construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.