Nuclear Binding Energy Iron Octave Multiple

The iron octave

Iron-56 is the nucleus that sits near the top of the nuclear binding-energy curve. Among all nuclides, it has one of the highest binding energies per nucleon, which is why nuclear fusion in stars tends to build elements up toward iron and then stop. The nucleus contains 26 protons and 30 neutrons, for a mass number A of 56. That number has a simple arithmetic shape: 56 equals 7 times 8. In the Recognition Science framework, the machine-checked library of formal theorems records this equality as a statement called iron_octave_multiple.

The framework's interest in the number 8 comes from its account of recognition cycles. In this account, a recognition event, a discrete act of registering a difference, runs through eight ticks before repeating. The framework's forcing chain derives the number 8 from the golden ratio phi, which itself emerges from the cost function J(x) = (x + 1/x)/2 - 1. Within that structure, the number 8 appears as the period of a full cycle, and powers of phi carry geometric meaning. The theorem iron_octave_multiple states only that the mass number of iron-56 is 7 times 8, a fact that ties the iron peak to the framework's octave structure.

The declaration does not claim that iron-56 is the most tightly bound nucleus. That distinction belongs to nickel-62, which has a slightly higher binding energy per nucleon. The framework's own notes place the peak region between A = 50 and A = 70, and iron-56 falls inside that band. The theorem also does not derive the binding energy itself. The framework's library contains a separate semi-empirical mass formula with coefficients built from phi, and a structural result that binding energy per nucleon peaks near A = 56, but iron_octave_multiple is only the arithmetic identity.

What the declaration does do is connect a measured nuclear fact to the framework's internal geometry. The number 56 is not just a count of nucleons; it is also an octave multiple, 7 full cycles of 8. The framework's library establishes this equality by computation, with no axioms beyond the standard three. It is a small step, but it places the iron peak inside the same numeric family as the magic numbers 2, 8, 20, 28, 50, 82, and 126, which the framework derives from its eight-tick shell structure.

/-- Iron-56 is 7 × 8 (octave multiple). -/
theorem iron_octave_multiple : iron56_A = 7 * 8 := by decide

/-- Iron-56 is in the peak region. -/
theorem iron_in_peak_region : peakRegion iron56_A := by
  constructor <;> decide

/-- The iron peak mass number is close to φ⁸: 56/φ⁸ ∈ (1, 1.2). -/
theorem iron_peak_near_phi8 :
    (iron56_A : ℝ) / phi_eighth > 1 ∧ (iron56_A : ℝ) / phi_eighth < 1.2 := by
  have hp8_pos : phi_eighth > 0 := by
    unfold phi_eighth
    exact pow_pos Constants.phi_pos 8
  have hphi_lt : Constants.phi < 1.62 := Constants.phi_lt_onePointSixTwo
  have hphi_nonneg : (0 : ℝ) ≤ Constants.phi := le_of_lt Constants.phi_pos
  have hp8_lt : phi_eighth < 1.62 ^ 8 := by
    unfold phi_eighth
    exact pow_lt_pow_left₀ hphi_lt hphi_nonneg (by norm_num : 8 ≠ 0)
  have h162_8 : (1.62 : ℝ) ^ 8 < 56 := by norm_num
  have hp8_lt_56 : phi_eighth < 56 := lt_trans hp8_lt h162_8
  constructor
  · -- 56 / φ⁸ > 1 iff 56 > φ⁸
    simp only [iron56_A]
    have h : (56 : ℝ) > phi_eighth * 1 := by linarith
    calc (56 : ℝ) / phi_eighth > phi_eighth * 1 / phi_eighth := by
          apply div_lt_div_of_pos_right h hp8_pos
       _ = 1 := by field_simp
  · -- 56 / φ⁸ < 1.2 requires φ⁸ > 46.67; use φ > 1.617 ⇒ φ⁸ > 47.4
    simp only [iron56_A]
    have hphi_gt : Constants.phi > 1.617 := by
      simp only [Constants.phi]
      have h5 : Real.sqrt 5 > 2.234 := by
        have h_sq : (2.234 : ℝ)^2 < 5 := by norm_num
        have h_pos : (0 : ℝ) ≤ 2.234 := by norm_num
        exact (Real.lt_sqrt h_pos).mpr h_sq
      linarith
    have h1617_8 : (1.617 : ℝ) ^ 8 > 46.67 := by norm_num
    have hp8_gt : phi_eighth > 46.67 := by
      unfold phi_eighth
      calc Constants.phi ^ 8 > (1.617 : ℝ) ^ 8 := by
             exact pow_lt_pow_left₀ hphi_gt (by norm_num) (by norm_num)
           _ > 46.67 := h1617_8
    have h56_lt : (56 : ℝ) < 1.2 * phi_eighth := by
      have h56 : (56 : ℝ) < 1.2 * 46.67 := by norm_num
      linarith
    calc (56 : ℝ) / phi_eighth < 1.2 * phi_eighth / phi_eighth := by
           apply div_lt_div_of_pos_right h56_lt hp8_pos
       _ = 1.2 := by field_simp

What this page does not claim

The theorem does not claim iron-56 is the most tightly bound nucleus. The theorem does not derive the binding energy of iron-56 from first principles. The theorem does not establish that the number 8 itself is forced by nuclear physics.

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/Nuclear/BindingEnergy.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: