pith. sign in
module module high

IndisputableMonolith.Physics.NuclearPhysicsDepthFromRS

show as:
view Lean formalization →

The module enumerates the nuclear magic numbers 2, 8, 20, 28, 50, 82, 126 and records their elementary relations to powers of two and gap multiples inside the Recognition Science framework. Nuclear model builders who want an RS-native account of shell closures would cite these values. The module consists of direct definitions and arithmetic checks with no deeper derivations.

claimThe nuclear magic numbers are the sequence $2, 8, 20, 28, 50, 82, 126$, satisfying $8 = 2^3$ and $82 < g_{45} · 2 = 90$.

background

The module sits inside the nuclear-physics extension of Recognition Science, which obtains all scales from the single functional equation and the T0–T8 forcing chain. It introduces NuclearStructureCategory as the classification of closed shells together with the associated count function and the first two magic numbers as explicit constants. The upstream Constants module supplies the base time quantum τ₀ = 1 tick that fixes the absolute scale for every derived nuclear quantity.

proof idea

This is a definition module with no proofs. It simply states the magic-number list and verifies the two arithmetic relations by direct substitution.

why it matters in Recognition Science

The module supplies the concrete magic numbers that feed NuclearPhysicsDepthCert and the subsequent depth calculations. It directly records the doc-comment facts 8 = 2³ and 82 < gap45 × 2 = 90, thereby linking the eight-tick octave (T7) to nuclear shell structure.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)