exponential_form_from_constant_log_derivative
plain-language theorem explainer
The declaration defines the proposition that any positive smooth function g with g(0) equal to the alpha seed and constant logarithmic derivative equal to minus one over the seed must equal the exponential alpha seed times exp of minus x over alpha seed. A physicist deriving the fine-structure constant from Recognition Science ledger geometry would cite this when justifying the exponential gap dependence. The definition simply records the ODE uniqueness claim as an open Prop without supplying a formal proof.
Claim. Let $a = 4π·11$. Suppose $g:ℝ→ℝ$ satisfies $g(0)=a$, $g(x)>0$ for all $x$, $g$ is $C^∞$, and $(d/dx)log g(x) = -1/a$ for all $x$. Then $g(x)=a·exp(-x/a)$.
background
In Recognition Science the inverse fine-structure constant takes the form $α^{-1}=α_{seed}·exp(-f_{gap}/α_{seed})$ with $α_{seed}=4π·11$ the geometric seed from spherical closure over 11-edge paths. The module AlphaExponentialForm examines structural properties of this expression, including positivity and the logarithmic ODE it satisfies. The definition exponential_form_from_constant_log_derivative records the open uniqueness question for the exponential solution under constant log derivative.
proof idea
This is a definition that directly states the Prop. No proof is supplied; the module comment notes the claim follows from standard ODE theory (constant log derivative implies exponential solution) but leaves it unproved pending ODE machinery.
why it matters
The definition supplies the uniqueness principle invoked by the downstream theorem exponential_form_uniqueness_ode_principle. It addresses gap B in the validation program by documenting that the exponential form satisfies the logarithmic ODE of running-coupling behavior. The module doc ties the motivation to J-cost log-coordinate structure while flagging the constant-derivative step as the remaining physical gap in the RS derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.