NanostructureType
plain-language theorem explainer
NanostructureType enumerates the five canonical nanoscale geometries recognized in the RS treatment of materials: nanoparticle, nanowire, nanosheet, nanotube, and quantum dot. Condensed-matter researchers mapping quantum confinement or plasmon resonance to discrete lattice scales would cite this enumeration when verifying that configuration dimension equals five. The declaration is a direct inductive definition that derives decidable equality, representation, boolean equality, and finite-type structure in one step.
Claim. The set of nanostructure types is the inductive type whose five constructors are nanoparticle, nanowire, nanosheet, nanotube, and quantum dot, equipped with decidable equality and a finite cardinality structure.
background
The NanoScienceFromRS module identifies nanoscale phenomena with recognition events at Q₃ lattice spacing, taking the recognition unit cell a₀ as the fundamental length. It equates five canonical nanostructure types to the configuration dimension D = 5, matching the five listed phenomena (quantum confinement, surface plasmon resonance, van der Waals forces, quantum tunneling, size-dependent catalysis). This inductive definition supplies the carrier type whose cardinality is asserted equal to five inside the NanoScienceCert structure.
proof idea
The declaration is an inductive definition that introduces five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances via the deriving clause.
why it matters
This definition supplies the finite carrier required by the NanoScienceCert structure, which records both five_phenomena and five_structures equal to five. It realizes the RS claim that nanoscale structure corresponds to configDim D = 5 and enables the downstream cardinality theorem nanostructureTypeCount. The construction aligns with the Recognition Science reduction of materials properties to recognition at discrete lattice scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.