deriv_alphaInv_of_gap
plain-language theorem explainer
The derivative of the inverse fine-structure constant with respect to the gap weight g satisfies d(α⁻¹)/dg = -(α⁻¹ / α_seed). Researchers analyzing the scale dependence of couplings in Recognition Science would cite this when working with the exponential parametrization of α⁻¹. The proof is a direct differentiation that unfolds the explicit form and applies the chain rule to the scaled exponential.
Claim. Let α⁻¹(g) := α_seed ⋅ exp(−g / α_seed). Then dα⁻¹(g)/dg = −(α⁻¹(g) / α_seed).
background
In the AlphaExponentialForm module the inverse fine-structure constant is written α⁻¹ = α_seed ⋅ exp(−f_gap / α_seed), where α_seed = 4π ⋅ 11 is the geometric seed from ledger structure and f_gap is the gap weight w₈ ln(φ) drawn from the eight-tick octave. The function alphaInv_of_gap simply parametrizes this expression by the real variable g standing for f_gap. Upstream, alpha_seed supplies the baseline spherical-closure cost while the definition of alphaInv_of_gap records the explicit exponential.
proof idea
The tactic proof unfolds alphaInv_of_gap, then builds HasDerivAt facts for the identity, its division by the constant α_seed, negation, composition with the exponential, and final multiplication by α_seed. A field_simp step aligns the resulting expression with the target form, after which the derivative is extracted directly.
why it matters
The result feeds the linear-rate theorem at g = 0 and the ODE-uniqueness principle that follows it, both inside the same module. It therefore contributes to the documented structural analysis of the exponential form as a candidate for the canonical α⁻¹ expression, linking the constant logarithmic derivative to the J-cost log-coordinate structure and running-coupling behavior. The module leaves open whether RS principles uniquely force the exponential Taylor coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.