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

stringTension_bounds

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

Lean usage

have hσ := stringTension_bounds

formal statement (Lean)

  57theorem stringTension_bounds :
  58    (0.08 : ℝ) < stringTension ∧ stringTension < 0.11 := by

proof body

Tactic-mode proof.

  59  unfold stringTension
  60  have h5 := phi5_bounds
  61  have hpow_pos : 0 < phi ^ 5 := pow_pos phi_pos 5
  62  rw [show (-(5 : ℤ)) = -↑(5 : ℕ) from rfl, zpow_neg, zpow_natCast]
  63  have hne : phi ^ 5 ≠ 0 := ne_of_gt hpow_pos
  64  constructor
  65  · -- 0.08 < (phi^5)⁻¹: 0.08 × phi^5 < 1, so 0.08 < 1/phi^5
  66    have hmul : (0.08 : ℝ) * phi ^ 5 < 1 := by nlinarith [h5.2]
  67    have hinv_pos : 0 < (phi ^ 5)⁻¹ := inv_pos.mpr hpow_pos
  68    nlinarith [mul_pos (by norm_num : (0:ℝ) < 0.08) hpow_pos,
  69               mul_inv_cancel₀ hne,
  70               mul_lt_mul_of_pos_right hmul hinv_pos]
  71  · -- (phi^5)⁻¹ < 0.11: 0.11 × phi^5 > 1
  72    have hmul : (1 : ℝ) < 0.11 * phi ^ 5 := by nlinarith [h5.1]
  73    have hinv_pos : 0 < (phi ^ 5)⁻¹ := inv_pos.mpr hpow_pos
  74    nlinarith [mul_pos (by norm_num : (0:ℝ) < 0.11) hpow_pos,
  75               mul_inv_cancel₀ hne,
  76               mul_lt_mul_of_pos_right hmul hinv_pos]
  77
  78/-! ## Cornell Potential -/
  79
  80/-- Cornell potential structure: V = -α_s/r + σ·r. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.