plasmonFrequency
plain-language theorem explainer
The definition sets the frequency of the k-th plasmonic mode to phi raised to k. Photonics researchers using Recognition Science phi-ladder models cite it to derive mode ratios and positivity from the self-similar fixed point. The assignment is a direct equational definition with no lemmas or tactics applied.
Claim. The characteristic frequency of the plasmonic mode indexed by rung $k$ equals $phi^k$, where $phi$ denotes the golden-ratio fixed point of the self-similar scaling.
background
The module treats five canonical plasmonic modes (surface plasmon polariton, localized surface plasmon, propagating, bulk, gap) as instances of configDim D = 5. Each mode frequency occupies one rung on the phi-ladder whose spacing is fixed by the Recognition Composition Law and the T6 forcing of phi as self-similar fixed point. The definition supplies the explicit frequency expression required by the downstream theorems that prove positivity and the constant ratio phi between consecutive rungs.
proof idea
Direct definition that equates plasmonFrequency k to the power phi ^ k; no lemmas or tactics are invoked.
why it matters
The definition realizes the module claim that each plasmonic mode frequency sits one rung up the phi-ladder and supplies the base term for PlasmonicModeCert, frequency_pos, and frequency_ratio. It connects the B15 photonics construction to the core forcing chain (T6 phi fixed point, T7 eight-tick octave) and the Recognition Composition Law. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.