PlasmonicMode
plain-language theorem explainer
PlasmonicMode enumerates the five canonical plasmonic modes required by the phi-ladder photonics construction. A researcher classifying mode frequencies or proving cardinality in Recognition Science would cite this enumeration when establishing the configDim D=5 structure. It is introduced as a direct inductive definition that derives Fintype to enable immediate cardinality and finiteness results.
Claim. Let $P$ be the inductive type whose elements are the five plasmonic modes: surface plasmon polariton, localized surface plasmon, propagating mode, bulk mode, and gap plasmon.
background
The module defines plasmonic modes from the phi-ladder in Recognition Science, positing five canonical types that correspond to configuration dimension D=5. These modes are surface plasmon polariton, localized surface plasmon, propagating, bulk, and gap plasmon, with each mode frequency placed one rung higher on the phi-ladder. The local setting follows the Recognition Composition Law and the self-similar fixed point phi, extending the eight-tick octave to photonic configurations.
proof idea
The declaration is a direct inductive definition listing the five constructors and deriving DecidableEq, Repr, BEq, and Fintype. No lemmas or tactics are invoked; the Fintype instance is obtained automatically from the finite enumeration.
why it matters
This definition supplies the enumeration required by PlasmonicModeCert, which asserts Fintype.card PlasmonicMode = 5 together with the phi-ratio property for successive frequencies. It fills the B15 photonics depth by linking the five modes to the phi-ladder, consistent with T7 eight-tick octave and the spatial dimension D=3 of the forcing chain. It enables downstream proofs of positive frequencies without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.