plasmonicModeCert
plain-language theorem explainer
plasmonicModeCert assembles the certificate asserting exactly five plasmonic modes whose frequencies form a geometric sequence of common ratio phi and remain strictly positive. Photonics modelers working in the Recognition Science phi-ladder framework cite it to fix the mode count and ratio properties before deriving dispersion relations. The definition is a direct structure constructor that substitutes the enumerated count theorem together with the two frequency lemmas.
Claim. The plasmonic-mode certificate asserts that the set of plasmonic modes has cardinality five, that the frequency of mode $k+1$ divided by the frequency of mode $k$ equals the golden ratio $phi$ for every natural number $k$, and that every mode frequency is positive.
background
The module treats plasmonic modes as five canonical types (surface plasmon polariton, localized surface plasmon, propagating, bulk, gap) whose characteristic frequencies lie on successive rungs of the phi-ladder. Consecutive frequencies therefore satisfy the ratio phi by construction. The upstream frequency_ratio theorem establishes the geometric progression by unfolding the definition of plasmonFrequency and applying the power rule for exponents. frequency_pos confirms positivity via the positivity of phi raised to any natural power. The mode count is obtained by direct enumeration of the inductive type PlasmonicMode.
proof idea
The definition is a direct constructor for the PlasmonicModeCert structure. It assigns the five_modes field from the plasmonicMode_count theorem, the phi_ratio field from frequency_ratio, and the frequency_always_pos field from frequency_pos.
why it matters
This definition supplies the concrete instance of the five-mode phi-ratio certificate required by any later derivation that invokes plasmonic frequencies in the Recognition framework. It anchors the photonics depth (configDim D = 5) and is consistent with the forced emergence of three spatial dimensions and the eight-tick octave. No downstream uses are recorded in the module, leaving the certificate available for future dispersion or resonance calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.