stringTension_bounds
plain-language theorem explainer
The theorem proves that the Recognition Science string tension lies in the open interval (0.08, 0.11). Nuclear physicists deriving Cornell potential coefficients for the semi-empirical mass formula would cite this bound when constraining the linear term from the phi-ladder. The proof is a direct algebraic verification that unfolds sigma = phi^{-5} and applies the interval bounds on phi^5 via nlinarith on the reciprocals.
Claim. $0.08 < phi^{-5} < 0.11$, where $phi$ is the golden-ratio fixed point and the string tension is defined as $sigma = phi^{-5}$.
background
The QCD-to-Nuclear Bridge module parameterizes the strong force via the geometric coupling alpha_s = 2/17 together with the string tension sigma = phi^{-5}, then connects these to the semi-empirical mass formula coefficients. The upstream phi5_bounds theorem states that 10 < phi^5 < 12, obtained from the interval 1.61 < phi < 1.62. The sibling definition stringTension is given explicitly as Constants.phi ^ (-(5 : Z)). The module asserts that every theorem in the file is machine-verified with zero sorry.
proof idea
The proof unfolds stringTension to phi^{-5}. It calls phi5_bounds to obtain the interval for phi^5, then proves the lower bound by showing 0.08 * phi^5 < 1 (via nlinarith on the upper endpoint) and applying mul_inv_cancel together with positivity of the inverse. The upper bound is obtained symmetrically by showing 1 < 0.11 * phi^5 (via nlinarith on the lower endpoint) and repeating the inverse argument. The main tactics are constructor, nlinarith, pow_pos, and mul_lt_mul_of_pos_right.
why it matters
This bound is invoked directly by the downstream theorem alpha_over_sigma_gt_one, which establishes alpha_strong / stringTension > 1. It supplies the numerical interval needed inside the QCDToNuclearBridge module to pass from the Recognition Science strong-force parameters to the nuclear binding-energy coefficients. The construction is consistent with the phi self-similar fixed point that appears in the foundation forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.