binding_energy_one_statement
plain-language theorem explainer
The recognition rung for the iron-group binding-energy peak is fixed at 26, with flanking rungs at 25 and 27 and a 22-step gap to the alpha rung. Nuclear physicists modeling the semi-empirical mass formula would cite this for its parameter-free location of the binding peak. The proof is a term-mode conjunction that packages five prior equalities and bounds.
Claim. The recognition rung of the iron-group binding-energy peak equals 26, satisfies $25 ≤ k ≤ 28$, the lower adjacent rung equals 25, the upper adjacent rung equals 27, and the iron-to-alpha rung gap equals 22.
background
In the Recognition Science treatment of nuclear binding, the binding energy per nucleon arises as the release of J-cost per nucleon on the phi-ladder. The iron peak occurs where this per-nucleon J-cost reaches its saturation value at rung k=26, computed as k_iron = consciousnessGap - configDim - holonomyShift = 45 - 5 - 14 at D=3. Upstream results establish that the iron rung is defined as 26, lies within the empirical band [25,28] from AME2020 data, the lower rung is 25, and the gap to the alpha rung is 22.
proof idea
The proof is a term-mode conjunction that directly applies the five upstream results: iron_peak_rung_eq for the equality to 26, iron_peak_rung_in_empirical_band for the interval bound, lower_adjacent_rung_eq and upper_adjacent_rung_eq for the flanks, and iron_to_alpha_gap_eq for the gap of 22.
why it matters
This declaration consolidates the key numerical predictions for the nuclear binding peak in the phi-ladder model, serving as the one-statement summary for Track E2 of Plan v7. It draws on the eight-tick octave and D=3 forcing from the UnifiedForcingChain, where the rung count derives from parityCount(D) + holonomy(D). The result supports the parameter-free explanation of the iron peak at Z=26, with the phi-step ratio f(k+1)=f(k)·φ governing adjacent binding energies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.