NuclearMagicCert
plain-language theorem explainer
The structure packages four arithmetic facts about the nuclear magic numbers set: cardinality exactly 7, membership of 2 and 8, and the identity 8 = 2 cubed. Nuclear physicists working on shell closures cite it to embed the observed sequence into the Recognition Science lattice. The definition is realized by direct appeal to the explicit enumeration of the set together with elementary facts on powers and membership.
Claim. Let $M = {2, 8, 20, 28, 50, 82, 126}$ be the set of nuclear magic numbers. The structure asserts that the cardinality of $M$ equals 7, that 8 belongs to $M$, that 2 belongs to $M$, and that $8 = 2^3$.
background
In Recognition Science, nuclear magic numbers arise as gaps in the shell-model energy spectrum at minima of the J-cost function on the nuclear recognition lattice. The set is given explicitly as $M = {2, 8, 20, 28, 50, 82, 126}$, where 2 = 2^1 marks the minimum and 8 = 2^3 corresponds to the eight-tick octave period required by the forcing chain for three spatial dimensions. This structure certifies the basic arithmetic properties of that set. It depends on the definition of the magicNumbers set and on the analogous certificate in the chemistry module that counts five doubly magic nuclides.
proof idea
The declaration is a structure definition whose four fields are populated by sibling lemmas: magicNumbersCard supplies the cardinality, magic_8_eq_2cubed supplies the power identity, and the two membership facts supply the inclusions of 8 and 2. The downstream constructor simply assembles these four facts into an instance of the structure.
why it matters
This certificate supplies the nuclear-side input to the chemistry module's nuclearMagicCert, which asserts that exactly five doubly magic nuclides exist. It directly encodes the eight-tick period (T7) and the emergence of three dimensions (T8) from the UnifiedForcingChain. The module thereby embeds the empirical sequence 2, 8, 20, 28, 50, 82, 126 into the Recognition Science framework without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.