logarithmic_derivative_constant
plain-language theorem explainer
The derivative of the logarithm of the inverse fine-structure constant with respect to the gap parameter equals the negative reciprocal of the geometric seed. Researchers modeling running couplings in Recognition Science cite this when confirming the differential structure of the exponential expression. The proof rewrites the logarithm as an affine function and differentiates the constant and linear pieces separately before adding the results.
Claim. $d/dg$ of $ln(alpha^{-1}(g))$ equals $-1/alpha_{seed}$, where $alpha^{-1}(g)$ is the seed times $exp(-g/alpha_{seed})$ and the seed equals $4 pi times 11$.
background
The module studies the exponential expression for the inverse fine-structure constant, written as the seed multiplied by an exponential decay linear in the gap weight. The seed itself is the geometric quantity $4 pi times 11$ that encodes baseline spherical closure cost over eleven-edge ledger paths. Positivity of both the seed and the full expression is established upstream, permitting the logarithm to be taken without qualification.
proof idea
The tactic sequence first confirms positivity of the parameterized inverse to justify the logarithm. It then proves the logarithm identity by unfolding the definition and applying the logarithm-of-product and logarithm-of-exponential rules. Function extensionality equates the original and rewritten expressions. Separate HasDerivAt facts are obtained for the constant term (derivative zero) and the linear term (identity rule, constant division, negation). These are added and the derivative is extracted.
why it matters
The result supplies the constant logarithmic derivative required by the downstream uniqueness principle for the exponential form. It realizes the differential-equation property listed in the module documentation as one of the structural facts established for the alpha expression. In the broader Recognition framework the constant slope connects the form to the log-coordinate Taylor expansion of the J-cost, whose factorial coefficients are inherited by the exponential series. The physical origin of the constancy remains an open question noted in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.