PlasmonicModeCert
plain-language theorem explainer
PlasmonicModeCert is a structure that certifies exactly five plasmonic modes whose frequencies form a geometric sequence with common ratio phi and remain strictly positive at every rung. A researcher modeling surface or gap plasmons within Recognition Science would cite the certificate to lock in the ladder scaling for mode counting and frequency ratios. The declaration is a pure structure definition that aggregates the three assertions with no derivation steps.
Claim. A certificate for plasmonic modes from the phi-ladder is a structure asserting that the set of modes has cardinality five, that the ratio of the frequency at rung $k+1$ to the frequency at rung $k$ equals the golden ratio, and that the frequency at every rung is strictly positive.
background
The module defines five canonical plasmonic mode types (surface plasmon polariton, localized surface plasmon, propagating, bulk, and gap plasmon) as the constructors of the inductive type PlasmonicMode. Each mode frequency is placed on the phi-ladder via the upstream definition plasmonFrequency(k) := phi^k. The local setting treats these modes as the five-dimensional configuration space for photonics depth B15, with frequencies scaling self-similarly under the golden ratio.
proof idea
PlasmonicModeCert is a structure definition with no proof body. It declares three fields that any instance must satisfy: the Fintype cardinality equality, the universal quantification on consecutive frequency ratios, and the positivity condition for all rungs.
why it matters
The structure supplies the type for the concrete instance constructed downstream in plasmonicModeCert, which populates the fields from the mode count, frequency ratio, and positivity lemmas. It anchors the photonics application by tying the five modes directly to the phi-ladder scaling that follows from the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.