exp_factor_bounded
The theorem shows that the factor exp(-f_gap / alpha_seed) is positive and at most 1 whenever the gap weight f_gap is nonnegative. Workers deriving the fine-structure constant from the Recognition Science ledger structure cite this bound to guarantee alpha inverse remains positive and physically sensible. The argument is a direct term-mode split that invokes the exponential positivity lemma together with the sign-reversing monotonicity of exp.
claimLet $f_ {gap} geq 0$ and let $alpha_ {seed} > 0$. Then $0 < exp(-f_ {gap} / alpha_ {seed}) leq 1$.
background
In the Alpha Exponential Form module the canonical expression for the inverse fine-structure constant is defined as alphaInv = alpha_seed * exp(-f_gap / alpha_seed), where alpha_seed = 4 pi * 11 is the geometric seed from ledger closure and f_gap = w8 * ln(phi) is the gap weight supplied by the GapWeight module. The upstream theorem alpha_seed_positive establishes that this seed is strictly positive. The module document states that the exponential form itself remains a structural hypothesis rather than a first-principles derivation, and the present bound is the minimal positivity statement needed before the logarithmic ODE analysis can proceed.
proof idea
The term proof opens with constructor to split the conjunction. The left conjunct is discharged by the library lemma Real.exp_pos. The right conjunct applies Real.exp_le_one_iff.mpr, which reduces the claim to nonpositivity of the exponent; this follows from div_nonneg applied to the hypothesis 0 leq f_gap together with the already-proved positivity of alpha_seed.
why it matters in Recognition Science
The result supplies the elementary positivity fact required by the downstream theorem exponential_form_uniqueness_ode_principle, which records the open question whether the exponential form is the unique solution to the logarithmic derivative condition. Within the Recognition Science chain it closes the immediate consistency check for the alpha exponential resummation before higher-order uniqueness arguments are attempted. The module document explicitly flags the remaining gap as the physical motivation for constant logarithmic derivative rather than a formal uniqueness theorem.
scope and limits
- Does not derive the exponential form from a variational principle.
- Does not prove that the exponential is the unique solution to the ODE.
- Does not address higher-order corrections beyond the first gap term.
- Assumes only nonnegativity of f_gap and positivity of alpha_seed.
formal statement (Lean)
71theorem exp_factor_bounded (hfg : 0 ≤ f_gap) :
72 0 < Real.exp (-(f_gap / alpha_seed)) ∧ Real.exp (-(f_gap / alpha_seed)) ≤ 1 := by
proof body
Term-mode proof.
73 constructor
74 · exact Real.exp_pos _
75 · apply Real.exp_le_one_iff.mpr
76 apply neg_nonpos_of_nonneg
77 exact div_nonneg hfg (le_of_lt alpha_seed_positive)
78
79/-- The ratio alphaInv/alpha_seed equals the exponential factor. -/