pith. sign in
module module high

IndisputableMonolith.Nuclear.BindingEnergyPeakScoreCard

show as:
view Lean formalization →

This module assembles a scorecard certifying that the nuclear binding energy per nucleon peaks at the iron group on the φ-ladder. Nuclear physicists testing discrete mass predictions against AME2020 data would cite it. The module organizes the argument through row definitions for the iron peak rung, empirical band checks, adjacent rungs, and alpha gap, ending in a certification theorem that applies the upstream ladder properties.

claimThe binding energy peak scorecard certifies that $B/A$ reaches its maximum near $Z=26$ (iron) on the φ-ladder rung, lying inside the empirical band, with BindingEnergyPeakScoreCardCert holding.

background

The module sits in the nuclear domain and imports the φ-ladder construction for binding energies. The upstream module states that the semi-empirical mass formula predicts the binding energy per nucleon peaks near the iron group, with the φ-ladder supplying the structural rung assignments for mass predictions via yardstick times φ to a power involving rung offset and gap(Z).

proof idea

This is a definition module that assembles row definitions for iron peak rung, empirical band membership, adjacent rungs, and iron-alpha gap, followed by the certification theorem. The holds statement is a one-line wrapper applying the rung uniqueness and ladder properties from the imported BindingEnergyFromPhiLadder module.

why it matters in Recognition Science

The module completes the nuclear binding energy track by supplying the scorecard certification. It provides the terminal object for the φ-ladder mass formula in the Recognition framework, aligning the iron peak with the T6 phi fixed point and T8 D=3 spatial structure. No downstream uses are listed, so it functions as the empirical contact point for this track.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)