nanoscalePhenomenonCount
plain-language theorem explainer
The theorem fixes the number of canonical nanoscale phenomena at five within the Recognition Science model. Researchers modeling material behavior at the Q3 lattice scale would cite this cardinality when confirming the configDim D equals five. The proof is a direct decision procedure on the finite inductive type whose five constructors enumerate the effects.
Claim. The set of nanoscale phenomena has cardinality five: $|$ {quantum confinement, surface plasmon resonance, van der Waals forces, quantum tunneling, size-dependent catalysis} $| = 5$.
background
The Nanoscience from RS module treats nanoscale effects as recognition events at Q3 lattice spacing, with a0 the recognition unit cell. The inductive type NanoscalePhenomenon enumerates the five canonical phenomena (quantum confinement, surface plasmon resonance, van der Waals forces, quantum tunneling, size-dependent catalysis) and derives Fintype, DecidableEq, and Repr instances. Module documentation states that this count equals configDim D = 5, matching the parallel count of five nanostructure types.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the inductive type with exactly five constructors.
why it matters
This cardinality supplies the five_phenomena field inside the nanoScienceCert definition that certifies the nanoscale layer of the framework. It directly realizes the module claim that five phenomena equal configDim D = 5 and anchors the E2 / B10 materials section. The result sits downstream of the inductive definition of NanoscalePhenomenon and feeds the certification object used for framework validation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.