NuclearStructureCategory
plain-language theorem explainer
Recognition Science models nuclear structure via an inductive enumeration of five categories: single-particle, collective, rotation, vibration, and cluster. Nuclear physicists working in the framework cite the definition to fix the configuration dimension at five for binding-energy and magic-number calculations. The inductive construction directly supplies the finite set whose cardinality is asserted in the downstream certificate.
Claim. Let $N$ be the set of nuclear structure categories. Then $N = $ {single-particle, collective, rotation, vibration, cluster}, a finite set of cardinality five.
background
The Nuclear Physics Depth from RS module introduces five nuclear structure categories to realize configuration dimension five. These categories are single-particle excitations, collective motions, rotational bands, vibrational modes, and cluster structures. The module links them to nuclear magic numbers and the binding-energy peak at iron-56, using the phi-ladder mass formula from upstream Recognition Science results.
proof idea
The declaration is an inductive definition that directly lists the five constructors. The Fintype, DecidableEq, and BEq instances are derived automatically by Lean, enabling the cardinality computation in the downstream count theorem.
why it matters
This definition supplies the five categories required by the NuclearPhysicsDepthCert structure, which asserts cardinality five and secondMagicNumber = 2^3. It fills the B7 Nuclear step where configDim equals five, paralleling the spatial dimension D = 3 obtained from forcing-chain step T8. The declaration closes the enumeration needed for the nuclear magic-number and depth certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.