module module high

`IndisputableMonolith.Nuclear.BindingEnergyFromPhiLadder`

This module supplies the recognition rungs that locate the iron-group binding-energy peak on the phi-ladder. It sets the central rung at 26 with stable neighbors at 25 and 27, matching the observed Z band 25-28. Nuclear physicists comparing RS mass predictions to measured binding energies would cite these definitions. The module is built entirely from definitions and elementary properties of the ladder.

claimThe iron-group binding-energy peak occurs at recognition rung $k=26$ on the phi-ladder, with adjacent stable rungs $k=25$ and $k=27$; the empirical iron band satisfies $25leq Zleq 28$.

background

The module imports the RS time quantum $tau_0=1$ tick from Constants and places nuclear binding energies on the phi-ladder whose spacing is governed by the Recognition Composition Law. Key objects introduced are iron_peak_rung (the central rung), lower_adjacent_rung and upper_adjacent_rung (its immediate neighbors), per_nucleon_phi_factor (the multiplicative correction per nucleon), and alpha_rung (the electromagnetic rung). These sit inside the broader mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)).

proof idea

This is a definition module, no proofs. It consists of direct assignments of integer rungs together with elementary lemmas establishing positivity, successor relations, and containment inside the empirical band.

why it matters in Recognition Science

The module supplies the concrete rung values required by the downstream BindingEnergyPeakScoreCard for the P3-binding-peak scorecard. That scorecard states the predicted peak sits at rung 26 with neighbors 25 and 27 inside the band 25 to 28, thereby linking the phi-ladder mass formula to the observed iron-group maximum.

scope and limits

Does not derive the binding-energy formula itself.
Does not compute numerical values of binding energies.
Does not treat other nuclear mass peaks or the valley of beta stability.
Does not address finite-temperature or density corrections.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Nuclear.BindingEnergyPeakScoreCard module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (18)

def iron_peak_rung L78
def lower_adjacent_rung L81
def upper_adjacent_rung L83
theorem iron_peak_rung_eq L85
theorem lower_adjacent_rung_eq L87
theorem upper_adjacent_rung_eq L89
theorem iron_peak_rung_in_empirical_band L92
def per_nucleon_phi_factor L100
theorem per_nucleon_phi_factor_pos L102
theorem per_nucleon_phi_factor_succ L107
theorem per_nucleon_phi_factor_ratio L113
def alpha_rung L122
def iron_to_alpha_gap L127
theorem iron_to_alpha_gap_eq L129
theorem iron_to_alpha_factor_pos L131
structure BindingEnergyCert L137
def bindingEnergyCert L147
theorem binding_energy_one_statement L162