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

alpha_bounds

show as:
view Lean formalization →

The theorem establishes that the fine-structure constant satisfies 0 < α < 0.1 in RS-native units. Researchers deriving mass ladders or bounding radiative corrections cite it to constrain electromagnetic terms in the phi-ladder. The proof is a direct conjunction of the positivity lemma and the upper-bound lemma.

claimThe fine-structure constant satisfies $0 < α < 0.1$.

background

This declaration appears in the Constants Predictions Proved module, which supplies calculated bounds for registry items including C-001. The quantity α is supplied by the definition alpha := 1/alphaInv from the Alpha module. Upstream structures from LedgerFactorization, PhiForcingDerived, and SpectralEmergence supply the J-cost minimization and discrete tier setting in which constants arise.

proof idea

The term proof applies the constructor tactic to split the conjunction, then invokes the lemmas alpha_positive and alpha_lt_0_1 directly.

why it matters in Recognition Science

The bound fills the C-001 registry item and is invoked by downstream theorems in JCostPerturbation such as radiative_cubic_coeff_forced (forcing the cubic coefficient to 12) and step_mu_tau_linear_coeff_forced (forcing the linear coefficient to 37/2). It anchors the electromagnetic scale for the phi-ladder mass formulas and the alpha band (137.030, 137.039) within the T5–T8 forcing chain.

scope and limits

formal statement (Lean)

  94theorem alpha_bounds : alpha > 0 ∧ alpha < (0.1 : ℝ) := by

proof body

Term-mode proof.

  95  constructor
  96  · exact alpha_positive
  97  · exact alpha_lt_0_1
  98
  99/-! ## Section C-005: Speed of Light c -/
 100
 101/-- **CALCULATED**: c = 1 (RS-native units). -/

used by (15)

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

depends on (9)

Lean names referenced from this declaration's body.