deriv_alphaInv_of_gap
plain-language theorem explainer
The result establishes that the derivative of the inverse fine-structure constant with respect to the gap parameter equals minus the function value divided by the seed constant. Researchers analyzing the differential structure of couplings in Recognition Science cite this when confirming the ODE satisfied by the exponential ansatz. The proof proceeds by direct construction of the derivative using the chain rule on the explicit form.
Claim. Let $a(g) = a_s e^{-g/a_s}$ with seed $a_s = 4π·11$. Then $a'(g) = -a(g)/a_s$.
background
The module examines the exponential representation of the inverse fine structure constant. Here the seed denotes the geometric baseline $4π·11$, drawn from ledger closure over 11-edge paths. The function of the gap is defined as the seed times the exponential of minus the gap divided by the seed, with the gap the weight $f_{gap}$ from the DFT-8 projection.
proof idea
The tactic proof unfolds the definition to the explicit product of the seed and exp of the scaled gap. It assembles HasDerivAt facts for the identity, constant division, negation, composition with the exponential, and constant multiplication. A field_simp step aligns the scaled derivative expression before the final deriv application.
why it matters
This derivative identity supplies the key step used by the linear rate theorem at zero gap and by the ODE uniqueness principle. It fills the structural analysis step in the AlphaExponentialForm module, confirming the logarithmic derivative remains constant. The module notes that physical motivations from J-cost log-structure remain unformalized as uniqueness theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.