exp_factor_bounded
plain-language theorem explainer
The result shows that the factor exp(−f_gap/α_seed) lies in (0,1] whenever the gap weight satisfies f_gap ≥ 0. Workers deriving the fine-structure constant inside the Recognition Science constants layer cite it to confirm the exponential resummation stays positive and bounded. The argument splits the conjunction and invokes the standard positivity and monotonicity properties of the real exponential.
Claim. If $0 ≤ f_{gap}$ and $α_{seed} > 0$, then $0 < exp(−f_{gap}/α_{seed}) ≤ 1$.
background
The module AlphaExponentialForm examines the canonical expression for the inverse fine-structure constant α⁻¹ := α_seed · exp(−f_gap/α_seed). Here α_seed is the geometric seed 4π·11 and f_gap is the gap weight w₈ ln φ drawn from the DFT-8 projection. The upstream theorem alpha_seed_positive establishes α_seed > 0, while alphaInv is defined directly as the product of seed and exponential factor. The local setting records that the exponential ansatz is motivated by the log-coordinate structure of the J-cost but remains a structural hypothesis rather than a derived uniqueness theorem.
proof idea
The term proof opens with constructor to separate the two conjuncts. The left side is discharged by Real.exp_pos. The right side applies Real.exp_le_one_iff after neg_nonpos_of_nonneg reduces the exponent to a nonpositive quantity, using div_nonneg together with the positivity of α_seed.
why it matters
The lemma supplies a basic positivity check that the downstream theorem exponential_form_uniqueness_ode_principle relies upon. It sits inside the constants layer that prepares the exponential form of α⁻¹ for the Recognition Science forcing chain (T5 J-uniqueness through T8). The module doc flags that the exponential Taylor coefficients are motivated by the cosh expansion of J but that uniqueness from the Recognition Composition Law is left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.