doublyMagic_count
plain-language theorem explainer
The theorem establishes that the finite type of doubly-magic nuclides has exactly five elements. Researchers in nuclear physics would cite this result to confirm that the Recognition Science model reproduces the standard list of closed-shell nuclides. The proof applies the decide tactic to enumerate the constructors of the inductive definition.
Claim. $|$${He-4 (2,2), O-16 (8,8), Ca-40 (20,20), Ca-48 (20,28), Ni-56 (28,28)}$$| = 5$
background
The module NuclearMagicIsotopesFromRS defines doubly-magic nuclides via an inductive type with five constructors corresponding to the nuclides He-4, O-16, Ca-40, Ca-48 and Ni-56. These satisfy the condition that both proton and neutron numbers are magic numbers from the set {2, 8, 20, 28, 50, 82, 126}. The upstream inductive definition provides the enumeration without further hypotheses, setting the local context for counting in the chemistry module.
proof idea
The proof is a one-line wrapper invoking the decide tactic on the cardinality statement. The tactic succeeds by computing the Fintype instance derived from the five constructors of the DoublyMagicNuclide inductive type.
why it matters
This theorem provides the value assigned to five_nuclides in the nuclearMagicCert definition. It completes the module's claim that Recognition Science yields precisely these five doubly-magic nuclides. The result ties into the framework's discrete predictions for nuclear structure arising from the phi-ladder and T7 eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.