deriv_alphaInv_of_gap
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.
claimLet α⁻¹(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 in Recognition Science
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.
scope and limits
- Does not derive the exponential form from a variational principle.
- Does not prove uniqueness of the exponential among other functional candidates.
- Does not connect the derivative to the full T0–T8 forcing chain.
- Does not produce numerical predictions or experimental comparisons.
Lean usage
rw [deriv_alphaInv_of_gap]formal statement (Lean)
130theorem deriv_alphaInv_of_gap (g : ℝ) :
131 deriv alphaInv_of_gap g = -(alphaInv_of_gap g / alpha_seed) := by
proof body
Tactic-mode proof.
132 unfold alphaInv_of_gap
133 -- h1: derivative of g → -(g/alpha_seed) is -(1/alpha_seed)
134 have h_id : HasDerivAt (fun g : ℝ => g) 1 g := hasDerivAt_id g
135 have h_div : HasDerivAt (fun g : ℝ => g / alpha_seed) (1 / alpha_seed) g :=
136 h_id.div_const alpha_seed
137 have h1 : HasDerivAt (fun g : ℝ => -(g / alpha_seed)) (-(1 / alpha_seed)) g :=
138 h_div.neg
139 -- h2: derivative of exp(-(g/alpha_seed))
140 have h2 : HasDerivAt (fun g : ℝ => Real.exp (-(g / alpha_seed)))
141 (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed))) g :=
142 (Real.hasDerivAt_exp _).comp g h1
143 -- h3: scale by alpha_seed
144 have h3 : HasDerivAt (fun g : ℝ => alpha_seed * Real.exp (-(g / alpha_seed)))
145 (alpha_seed * (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed)))) g :=
146 h2.const_mul alpha_seed
147 -- Simplify the derivative expression
148 have heq : alpha_seed * (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed)))
149 = -(alpha_seed * Real.exp (-(g / alpha_seed)) / alpha_seed) := by
150 field_simp
151 rw [← heq]
152 exact h3.deriv
153
154/-- The logarithmic derivative: d ln(α⁻¹)/d(f_gap) = -1/α_seed (constant). -/