alphaInv_linear_rate
plain-language theorem explainer
The declaration establishes that the derivative of the gap-parameterized inverse fine-structure constant at zero gap equals exactly -1. Researchers analyzing running couplings or renormalization flows in Recognition Science would cite this for the leading perturbative rate of alpha inverse. The proof is a term-mode reduction that invokes the general derivative formula, substitutes the zero-gap value, and simplifies algebraically.
Claim. Let $a(g) := a_s e^{-g/a_s}$ with $a_s = 4pi cdot 11$. Then $a'(0) = -1$.
background
In the AlphaExponentialForm module the inverse fine-structure constant is parameterized by the gap function as $a(g) = a_s exp(-g/a_s)$, where $a_s$ is the seed value fixed at $4pi cdot 11$ and $g$ stands for $f_gap = w_8 ln phi$. This form is introduced to examine positivity, differential behavior, and the open uniqueness question left after the integer seed is derived elsewhere. The module sits inside the constants layer and records motivations from J-cost logarithmic structure and renormalization-group improvement without closing the forcing argument for the exponential ansatz itself.
proof idea
The term proof first rewrites the target using the general derivative identity deriv_alphaInv_of_gap, which states that the derivative of $a(g)$ at any $g$ equals $-a(g)/a_s$. It then substitutes the zero-gap evaluation $a(0) = a_s$ supplied by alphaInv_linear_term and finishes with field_simp to reach the constant -1.
why it matters
The result supplies the leading-order rate required by the structural analysis of the exponential form and is used directly by the downstream uniqueness-ODE principle. It addresses the documented Gap B by confirming that the logarithmic derivative is constant at leading order, consistent with the J-cost cosh expansion and the eight-tick octave structure. The module explicitly flags that the physical justification for constancy of the log derivative remains an open forcing question in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.