NuclearMagicCert
plain-language theorem explainer
NuclearMagicCert packages a structure asserting that the finite set of doubly magic nuclides has cardinality exactly 5. Nuclear physicists citing RS-derived shell closures would reference it when mapping the seven magic numbers to the observed stable isotopes He-4, O-16, Ca-40, Ca-48 and Ni-56. The declaration is a direct structure definition that records the Fintype.card fact computed from the inductive enumeration of those five nuclides.
Claim. A structure certifying that the finite type of doubly magic nuclides (He-4, O-16, Ca-40, Ca-48, Ni-56) has cardinality 5, where each nuclide has both proton and neutron numbers belonging to the magic set derived from the eight-tick octave.
background
The module Chemistry.NuclearMagicIsotopesFromRS enumerates the five canonical doubly-magic nuclides via the inductive type DoublyMagicNuclide with constructors he4, o16, ca40, ca48, ni56. Each satisfies proton number = neutron number equal to one of the magic numbers {2, 8, 20, 28, 50, 82, 126}. The module imports Constants and depends on the upstream Physics.NuclearMagicNumbersFromRS.NuclearMagicCert, whose doc-comment records the seven magic numbers together with the relation (8 : ℕ) = 2^3.
proof idea
The declaration is a structure definition introducing the single field five_nuclides : Fintype.card DoublyMagicNuclide = 5. It functions as a direct packaging of the cardinality computed from the inductive type; no tactics or lemmas are applied beyond the Fintype instance derived for DoublyMagicNuclide.
why it matters
NuclearMagicCert supplies the chemistry-side certificate that is instantiated by the downstream nuclearMagicCert definition in the same module and cross-referenced by the Physics.NuclearMagicNumbersFromRS counterpart. It closes the link from the T7 eight-tick octave (period 2^3) that forces the initial magic numbers to the concrete count of five doubly-magic nuclides. The declaration touches the open question of whether RS will later predict additional magic numbers beyond the initial seven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.