nuclearMagicCert
plain-language theorem explainer
The certificate packages the claim that the nuclear magic numbers form a seven-element set containing both 2 and 8, with the additional equality 8 = 2 cubed. Nuclear physicists modeling shell closures under Recognition Science would cite it to connect the observed numbers to the eight-tick octave at three spatial dimensions. The definition is a direct structure constructor that supplies four decide-proved facts to the required fields.
Claim. Let $M$ be the set of nuclear magic numbers. The certificate is the structure satisfying $|M|=7$, $8=2^3$, $8∈M$, and $2∈M$.
background
Recognition Science treats nuclear magic numbers as gaps in the shell-model spectrum at J-cost minima on the nuclear recognition lattice. The module records the standard list 2, 8, 20, 28, 50, 82, 126 and isolates the exact relations 2 = 2^1 and 8 = 2^3, the latter identified with the eight-tick period forced by D = 3. The structure NuclearMagicCert collects exactly these four properties into a single object that downstream code can consume without re-proving the arithmetic facts.
proof idea
The definition constructs the structure by direct field assignment: the cardinality equality is taken from the decide proof of the seven-element count, the equality 8 = 2^3 is taken from the decide proof of the eight-tick relation, and the two membership statements are taken from the corresponding decide proofs. No tactics or reductions are applied beyond the structure constructor itself.
why it matters
The certificate is the immediate supplier for the chemistry module's count of five doubly magic nuclides. It therefore closes the A1 SM/Nuclear Depth formalization step that links the observed magic numbers to the eight-tick octave at D = 3. The construction supplies the precise arithmetic content required by any later theorem that invokes the Recognition Science derivation of nuclear shell closures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.