nuclearMagicCert
plain-language theorem explainer
nuclearMagicCert packages the count of five doubly-magic nuclides into the NuclearMagicCert structure for downstream use in physics derivations. Researchers modeling nuclear stability via the Recognition Science phi-ladder would cite this to confirm the canonical set matches the eight-tick predictions. The construction is a direct field assignment from the decidable theorem doublyMagic_count.
Claim. Let DoublyMagicNuclide be the finite type of nuclides with equal magic proton and neutron numbers. The certificate NuclearMagicCert is instantiated by setting its field five_nuclides to the proof that the cardinality of DoublyMagicNuclide equals 5.
background
Recognition Science derives nuclear magic numbers from the eight-tick octave (T7) in the forcing chain, where the period 2^3 produces the sequence 2, 8, 20, 28, 50, 82, 126. DoublyMagicNuclide collects the five nuclides satisfying the doubly-magic condition: He-4 (2,2), O-16 (8,8), Ca-40 (20,20), Ca-48 (20,28), Ni-56 (28,28). The module NuclearMagicIsotopesFromRS supplies the chemistry-side certificate that exactly five such nuclides exist.
proof idea
This is a one-line wrapper that constructs the NuclearMagicCert structure by assigning the five_nuclides field directly to the result of the theorem doublyMagic_count.
why it matters
This definition supplies the chemistry certificate referenced by the physics nuclearMagicCert, which extends it with the seven-magic count and the relation 8 = 2^3. It anchors the nuclear magic numbers to the T7 eight-tick octave landmark and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.