metamaterialTypeCount
plain-language theorem explainer
metamaterialTypeCount establishes that the finite set of canonical metamaterial response classes contains exactly five elements. Researchers classifying photonic bandgaps in phi-lattice geometries would cite this cardinality result when enumerating epsilon-near-zero through topological responses. The proof is a direct computational check via the decide tactic on the derived Fintype instance.
Claim. The finite type whose elements are the five metamaterial responses (epsilon-near-zero, mu-near-zero, double-negative, hyperbolic, topological) has cardinality 5.
background
The module PhotonicsMetamaterialFromPhi introduces the phi-lattice metamaterial under RS_PAT_018, where five canonical responses (epsilon-near-zero, mu-near-zero, double-negative, hyperbolic, topological) are identified with configDim D = 5. Bandgap positions are stated to lie at phi-ladder frequencies set by the lattice periodicity. The inductive type MetamaterialType enumerates precisely these five constructors and derives Fintype, DecidableEq, Repr, and BEq instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card MetamaterialType = 5. The tactic succeeds because the inductive definition supplies an explicit Fintype instance whose cardinality is the number of constructors.
why it matters
This result supplies the five_types component of the downstream photonicsMetamaterialCert definition. It directly realizes the five-response count asserted in the module documentation for RS_PAT_018, anchoring the phi-lattice geometry to the enumerated classes without invoking the spatial-dimension result D = 3 from the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.