pith. machine review for the scientific record. sign in
theorem proved term proof high

coulombCoeff_consistent

show as:
view Lean formalization →

Verification establishes that the Coulomb coefficient in nuclear binding energy calculations differs from its electromagnetic prediction by less than 0.2. Modelers applying the semi-empirical mass formula cite the bound to confirm parameter alignment between QCD inputs and observed nuclear scales. The proof is a one-line wrapper that unfolds the two coefficient definitions then applies numerical normalization.

claim$|C - C_p| < 0.2$, where $C$ denotes the Coulomb coefficient appearing in nuclear binding energy expressions and $C_p = (3/5) (1/137.036) (197.3 / 1.2)$ is the value predicted from electromagnetic considerations.

background

The module converts QCD-level inputs alpha_strong = 2/17 and string tension sigma = phi^{-5} into the coefficients of the semi-empirical mass formula. The predicted Coulomb coefficient is defined directly as (3/5) times the inverse fine-structure constant times a length-scale ratio. Upstream, r_min is the saturation radius given by sqrt(alpha_strong / stringTension), while the cellular-automata radius supplies a unit neighborhood size that remains peripheral to this numerical check.

proof idea

The proof is a one-line wrapper that unfolds the definitions of coulombCoeff and coulombCoeff_predicted, then applies norm_num to discharge the numerical inequality.

why it matters in Recognition Science

The result supplies a terminal consistency check inside the QCD-to-nuclear bridge, confirming that the electromagnetic term in binding energies stays within 0.2 of the value computed from the Recognition Science alpha band. It closes the numerical link between the string-tension and alpha_strong parameters and the semi-empirical mass formula without introducing further hypotheses.

scope and limits

formal statement (Lean)

 107theorem coulombCoeff_consistent : |coulombCoeff - coulombCoeff_predicted| < 0.2 := by

proof body

Term-mode proof.

 108  unfold coulombCoeff coulombCoeff_predicted; norm_num
 109
 110/-! ## Saturation Properties -/
 111
 112/-- Nuclear saturation radius r_min = √(α_s/σ). -/

depends on (3)

Lean names referenced from this declaration's body.