row_adjacent_rungs
plain-language theorem explainer
The theorem fixes the nuclear rungs immediately below and above the iron binding-energy peak at 25 and 27 on the phi-ladder. Nuclear modelers using Recognition Science to locate the AME2020 iron-group maximum would cite this to anchor the central rung at 26. The proof is a direct term that pairs the two reflexivity equalities already established for the lower and upper adjacent rungs.
Claim. The lower rung adjacent to the iron peak equals 25 and the upper rung adjacent to the iron peak equals 27: $k_5 = 25$ and $k_7 = 27$.
background
Recognition Science places nuclear binding energies on a discrete phi-ladder whose rungs are indexed by integers k. The iron-group peak is assigned to rung 26; the flanking rungs are obtained by subtracting or adding one, yielding manganese at 25 and cobalt at 27. The module P3-binding-peak scorecard records this assignment together with the empirical AME2020 band 25 ≤ Z ≤ 28. Upstream lemmas in BindingEnergyFromPhiLadder supply the definitions lower_adjacent_rung := iron_peak_rung - 1 and upper_adjacent_rung := iron_peak_rung + 1 together with their equality theorems proved by reflexivity.
proof idea
The proof is a one-line term wrapper that applies the pair constructor to the two upstream equality theorems lower_adjacent_rung_eq and upper_adjacent_rung_eq.
why it matters
The result supplies the adjacent-rungs field required by bindingEnergyPeakScoreCardCert_holds, which assembles the complete P3-binding-peak certificate (peak rung, empirical band, adjacent rungs, iron-alpha gap). It thereby closes the rung-assignment portion of the nuclear scorecard while leaving the 50-nucleus RMS benchmark as a Phase 3 residual. The assignment is consistent with the phi-ladder mass formula and the eight-tick octave structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.