Physics Nuclear Physics Depth From Rs

Nuclear structure categories

Nuclear physics sorts the many shapes and motions of atomic nuclei into a small set of structure categories. The standard picture names five: single-particle motion, collective behavior, rotation, vibration, and clustering. Single-particle means one nucleon moves in the average field of the others; collective means many nucleons move together; rotation is the whole nucleus spinning; vibration is a periodic shape oscillation; clustering is the nucleus behaving as a few sub-blobs rather than a uniform drop. These five categories cover the main ways a nucleus can organize itself, and they are the usual starting point for describing nuclear spectra and transitions.

The framework Recognition Science models this classification with a machine-checked library of formal theorems. It defines an inductive type with exactly those five constructors and proves, by direct computation, that the number of categories is five. The proof is a theorem in the library, with no unproved axioms. This is a small but clean result: the framework takes an empirical classification and certifies that the count is exactly five, not four or six.

The module also records the nuclear magic numbers, the shell-closure values 2, 8, 20, 28, 50, 82, 126. It proves that the second magic number equals 2 cubed, a trivial identity but one that ties the shell structure to the framework's preferred power-of-two pattern. The certificate structure bundles these two facts, the five categories and the second magic number identity, into a single object that the library can carry forward.

What this establishes in plain language is modest but precise: the classification of nuclear structure into five categories is a theorem, not a convention, within the framework. The framework does not derive the binding energy peak at iron-56 or the mass formula; those are empirical annotations in the docstring, not proved statements. The value here is the formal anchor: a named, checkable proof that the five-way split is complete in the framework's sense.

theorem nuclearStructureCategoryCount : Fintype.card NuclearStructureCategory = 5 := by decide

theorem secondMagic_eq_2cubed : secondMagicNumber = 2 ^ 3 := by decide

def nuclearPhysicsDepthCert : NuclearPhysicsDepthCert where
  five_categories := nuclearStructureCategoryCount
  second_magic_cube := secondMagic_eq_2cubed

What this page does not claim

The framework does not derive nuclear binding energies or the iron-56 peak. The five categories are not proved to be exhaustive by physical measurement. The magic number identity 8 = 2³ is a formal tautology, not a derivation of shell closure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/NuclearPhysicsDepthFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: