bindingEnergyCert
plain-language theorem explainer
The bindingEnergyCert definition assembles a structure certifying the nuclear binding-energy peak properties on the phi-ladder. An RS modeler or nuclear theorist would cite it to record that the iron peak sits at rung 26 with flanks at 25 and 27, the per-nucleon factor multiplies by phi each step, and the iron-alpha gap is 22. The definition is a direct structure constructor that pulls the required equalities and positivity statements from sibling lemmas.
Claim. The certificate asserts that the iron peak rung equals 26, lies in the interval $[25,28]$, the adjacent rungs are 25 and 27, the per-nucleon recognition factor $f(k)$ satisfies $0 < f(k)$ for all natural numbers $k$ and $f(k+1) = f(k) · φ$, and the iron-to-alpha rung gap equals 22.
background
In the Recognition Science setting, nuclear binding energy is the J-cost release per nucleon on the strong-force ledger. Each nucleon occupies a recognition rung on the phi-ladder; the per-nucleon factor is the cost induced by a multiplicative recognizer. The module derives the iron peak at rung 26 from the identity $k_iron = consciousnessGap - configDim - holonomyShift = 45 - 5 - 14$ at spatial dimension $D=3$ (MODULE_DOC). Upstream, rung supplies the base counting, while cost from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost interpretation.
proof idea
One-line wrapper that constructs the BindingEnergyCert structure by direct field assignment: iron_peak_eq to iron_peak_rung_eq, iron_peak_in_band to iron_peak_rung_in_empirical_band, lower_adjacent_eq to lower_adjacent_rung_eq, upper_adjacent_eq to upper_adjacent_rung_eq, per_nucleon_pos to per_nucleon_phi_factor_pos, adjacent_ratio to per_nucleon_phi_factor_ratio, and iron_alpha_gap_eq to iron_to_alpha_gap_eq.
why it matters
The declaration supplies the bundled certificate required by the downstream theorem bindingEnergyPeakScoreCardCert_holds, which constructs a nonempty BindingEnergyPeakScoreCardCert instance. It completes the structural prediction step of Track E2, where the iron peak at Z=26 is forced by the eight-tick octave and D=3 without free parameters; the adjacent-ratio property encodes the self-similar fixed point of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.