pith. machine review for the scientific record. sign in
theorem proved term proof high

magic_28_from_cube

show as:
view Lean formalization →

The equality 28 = 8 + 12 + 8 holds as an arithmetic identity that encodes the double 8-tick closure for the nuclear magic number 28. Nuclear physicists building binding-energy models from the phi-ladder would cite this when assembling the semi-empirical mass formula. The proof is a one-line norm_num reduction that confirms the arithmetic without invoking further lemmas.

claimThe nuclear magic number 28 satisfies $28 = 2^3 + 3·2^2 + 2^3$.

background

Recognition Science derives nuclear shell structure from the 8-tick periodicity on the phi-ladder. One tick is the fundamental RS time quantum; one octave comprises exactly 8 ticks. The module states that magic numbers arise directly from this geometry: 28 equals 20 plus 8, a double 8-tick closure. Upstream structures supply the J-cost functional on the phi-lattice and the tiered nuclear densities expressed as powers of phi.

proof idea

The proof is a one-line wrapper that applies norm_num to the arithmetic identity.

why it matters in Recognition Science

This identity supplies the explicit count for the magic number 28 inside the 8-tick shell model that precedes the Weizsacker-like binding-energy formula. It closes one step in the module's derivation of volume, surface, Coulomb, asymmetry and pairing terms from J-cost and 8-tick phase alignment, linking directly to the eight-tick octave landmark. No downstream uses are recorded yet.

scope and limits

formal statement (Lean)

  66theorem magic_28_from_cube : (28 : ℕ) = 2 ^ 3 + 3 * 2 ^ 2 + 2 ^ 3 := by norm_num

proof body

Term-mode proof.

  67
  68/-! ## Weizsacker-like Binding Energy Formula
  69
  70The semi-empirical mass formula with RS-motivated structure.
  71All coefficients are functions of φ and the 8-tick geometry. -/
  72

depends on (9)

Lean names referenced from this declaration's body.