exp_factor_bounded
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.