exponential_form_from_constant_log_derivative
The declaration encodes the uniqueness statement that any positive smooth function g with g(0) equal to the geometric seed 4π·11 and constant logarithmic derivative -1/alpha_seed must equal alpha_seed times exp(-x/alpha_seed). Researchers deriving the inverse fine-structure constant from ledger geometry would cite this to isolate the structural gap. The body states the Prop directly with no proof supplied, deferring to standard ODE uniqueness.
claimLet $g : {R} {to} {R}$ satisfy $g(0) = 4{pi} {cdot} 11$, $g(x) > 0$ for all $x$, $g$ is $C^{infty}$, and $frac{d}{dx} log g(x) = -1/(4{pi} {cdot} 11)$. Then $g(x) = 4{pi} {cdot} 11 {cdot} exp(-x/(4{pi} {cdot} 11))$.
background
Alpha_seed is defined as $4{pi} {cdot} 11$, the baseline spherical closure cost over 11-edge interaction paths from the ledger structure. The module examines the canonical form $alpha^{-1} = alpha_{seed} exp(-f_{gap}/alpha_{seed})$ with $f_{gap}$ the gap weight from the phi-ladder, proving positivity and the associated logarithmic ODE while flagging uniqueness as open. Upstream results include the alpha_seed definitions in Constants.Alpha (geometric seed from ledger structure) and AlphaHigherOrder (4{pi} times passive edges).
proof idea
This is a definition packaging the uniqueness statement as a Prop. No lemmas or tactics are invoked in the body; the statement is written directly, accompanied by a comment that it follows from Picard-Lindelof uniqueness for the ODE but is left unproved here.
why it matters in Recognition Science
The definition isolates the open uniqueness question for the exponential alpha form, feeding directly into the trivial uniqueness theorem in the same module. It documents the remaining gap after proving positivity and the ODE, touching the T5 J-uniqueness landmark and the constants derivation where alpha^{-1} lies in (137.030, 137.039). The physical motivation for constant log derivative from J-cost log-structure is noted but not formalized.
scope and limits
- Does not derive the exponential form from the Recognition Composition Law.
- Does not prove that the logarithmic derivative must be constant under RS axioms.
- Does not supply a formal ODE proof using Picard-Lindelof.
- Does not close the structural gap in the alpha inverse formula.
formal statement (Lean)
242def exponential_form_from_constant_log_derivative : Prop :=
proof body
Definition body.
243 ∀ (g : ℝ → ℝ),
244 (g 0 = alpha_seed) →
245 (∀ x, 0 < g x) →
246 ContDiff ℝ ⊤ g →
247 (∀ x, deriv (fun y => Real.log (g y)) x = -(1 / alpha_seed)) →
248 ∀ x, g x = alpha_seed * Real.exp (-(x / alpha_seed))
249
250/-- **OPEN STATUS**: This uniqueness claim follows from standard ODE theory
251 (if log g' is constant = k, then g(x) = g(0) · e^(kx), which is unique
252 under Picard-Lindelöf). We leave it unproved here as it is provable in
253 principle but requires ODE machinery.
254
255 The *physical* question — WHY the log derivative should be constant
256 in the RS derivation — is the true remaining gap. -/