alpha_lt_0_1
plain-language theorem explainer
The theorem establishes that the fine-structure constant α satisfies α < 0.1. Researchers deriving fundamental constants from the Recognition Science forcing chain would reference this result to bound the electromagnetic coupling. The tactic proof first secures α_seed > 132 and f_gap < α_seed − 10 via nlinarith and explicit comparisons on w8, log φ, and sqrt(2), then applies the exponential inequality to obtain α_inv > 10 before inverting the relation.
Claim. Let α be the fine-structure constant given by α = 1/α_inv with α_inv = α_seed ⋅ exp(−f_gap / α_seed) and α_seed = 4π ⋅ 11. Then α < 0.1.
background
The ConstantsPredictionsProved module supplies calculated proofs for registry constants, including the fine-structure constant under item C-001. Here α is constructed from the geometric seed α_seed = 4π × 11 (baseline spherical closure over 11-edge paths) damped by the first-order gap correction exp(−f_gap / α_seed), where f_gap = w8 log φ and w8 is the eight-tick weight. The upstream lemma phi_lt_onePointSixTwo supplies the concrete bound φ < 1.62 that controls the size of the gap term.
proof idea
The tactic proof begins with positivity of α_seed and the lower bound α_seed > 132 obtained by nlinarith with Real.pi_gt_three. It next invokes Real.add_one_le_exp to bound the exponential from below, then proves f_gap < α_seed − 10 by chaining f_gap < w8_from_eight_tick < 5 (using separate bounds on sqrt(2), φ > 1.618, and log φ < 1) and linarith. These combine to give α_inv > 10; the final steps unfold α = 1/α_inv and apply div_lt_iff₀ followed by nlinarith.
why it matters
This bound completes the upper half of registry item C-001 and is invoked directly by the sibling theorem alpha_bounds to assemble the full statement 0 < α < 0.1. It is also packaged inside constants_predictions_cert_exists to certify the set of structural predictions. Within the Recognition Science framework the result confirms that the phi-ladder and eight-tick octave place α inside the observed interval near 1/137, consistent with the alpha precision band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.