plasmonicMode_count
plain-language theorem explainer
The Recognition Science model fixes the number of plasmonic modes at five, matching the five types obtained from the phi-ladder. Photonic researchers classifying surface and bulk modes in the framework would cite this cardinality result. The proof is a one-line decision procedure that directly evaluates the Fintype cardinality of the finite inductive enumeration.
Claim. The set of plasmonic modes has cardinality five: $|$surface plasmon polariton, localized surface plasmon, propagating, bulk, gap plasmon$| = 5$.
background
The module introduces five canonical plasmonic mode types that realize configDim D = 5. These comprise 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 is the B15 Photonics Depth section, which states that Lean status is zero sorry and zero axiom. This rests on the upstream inductive definition that equips the mode type with DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the Fintype cardinality of the inductive type enumerating the five modes.
why it matters
This supplies the five_modes field to the downstream plasmonicModeCert definition, which also records the phi ratio and frequency positivity. It anchors the photonic sector of the Recognition framework by fixing the mode count at five, consistent with the phi-ladder and the eight-tick octave. The result closes the enumeration step before frequency derivations and ties directly to the configDim D = 5 convention stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.