exp_minus_add_pos
plain-language theorem explainer
The theorem shows that when the additive approximation to α⁻¹ lies below the CODATA value and the exponential approximation lies above it, the exponential form exceeds the additive form by a positive margin. Researchers deriving higher-order voxel-seam corrections in the Recognition Science α⁻¹ series would cite this result to bound the second-order term δ₂ under an alternating-series assumption. The proof is a one-line application of linear arithmetic to the two supplied inequalities.
Claim. Let α_seed denote the geometric seed 4π times the number of passive edges, let f_gap(w_8) be the gap weight for real parameter w_8, let δ_1 be the first-order curvature correction, and let α_CODATA be the CODATA 2022 value of α⁻¹. If α_seed − f_gap(w_8) + δ_1 < α_CODATA < α_seed ⋅ exp(−f_gap(w_8)/α_seed), then 0 < α_seed ⋅ exp(−f_gap(w_8)/α_seed) − (α_seed − f_gap(w_8) + δ_1).
background
The module formalizes higher-order corrections to the RS derivation of α⁻¹. The geometric seed is defined as α_seed := 4π ⋅ passive_edges. The gap weight is f_gap(w_8) := w_8 ⋅ ln φ. The first-order correction is δ_1 := −103/(102 π^5). These enter two candidate formulas: the additive form α_seed − f_gap + δ_1 and the exponential form α_seed ⋅ exp(−f_gap/α_seed). The CODATA value is supplied as the explicit target 137.035999206. The module states that the full series is α⁻¹ = α_seed − f_gap + Σ δ_n and that the present theorem supplies a gap bound needed for the alternating-series estimate of δ_2.
proof idea
The proof is a one-line wrapper that applies the linarith tactic directly to the two hypotheses. No auxiliary lemmas are invoked; the tactic discharges the positivity claim by linear arithmetic on the supplied strict inequalities.
why it matters
The declaration supplies the concrete positivity gap required to bound δ_2 once the alternating character of the series is established. It sits inside the open δ_2 computation described in the module documentation and feeds the convergence argument for the full series α⁻¹ = α_seed − f_gap + Σ δ_n. The result is a direct instance of the framework landmarks T5 (J-uniqueness) and the Recognition Composition Law that underwrite the exponential and additive forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.