NanoscalePhenomenon
plain-language theorem explainer
NanoscalePhenomenon enumerates the five canonical nanoscale phenomena recognized in the RS framework at Q₃ lattice spacing: quantum confinement, surface plasmon resonance, van der Waals forces, quantum tunneling, and size-dependent catalysis. Materials physicists working on configDim D = 5 effects would cite this enumeration when certifying that nanoscale recognition produces exactly these five cases. The declaration is a direct inductive construction that derives Fintype, DecidableEq, Repr, and BEq instances in one step.
Claim. Let $P$ be the inductive type whose five elements are quantum confinement, surface plasmon resonance, van der Waals forces, quantum tunneling, and size-dependent catalysis.
background
In the Recognition Science setting of Nanoscience from RS — E2 / B10 Materials, nanoscale phenomena arise at the Q₃ lattice spacing with recognition unit cell $a_0$. The module states that the five canonical effects (quantum confinement, surface plasmon resonance, van der Waals forces, quantum tunneling, size-dependent catalysis) equal configDim $D = 5$. The inductive definition supplies the Lean representation of this five-element set and equips it with the finite-type and equality structure needed for cardinality statements.
proof idea
The declaration is a direct inductive definition that lists the five phenomena as constructors and derives DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
This definition supplies the five phenomena required by the downstream NanoScienceCert structure (which records Fintype.card NanoscalePhenomenon = 5) and the nanoscalePhenomenonCount theorem. It realizes the claim that recognition at the nanoscale yields exactly five canonical effects, matching configDim $D = 5$ in the E2/B10 sector. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.