logarithmic_derivative_constant
The declaration shows that the logarithmic derivative of alpha inverse with respect to the gap parameter equals the constant negative reciprocal of the seed. Researchers deriving renormalization-group equations or verifying exponential ansatze for coupling constants in Recognition Science would cite it to confirm the differential structure of the form. The proof equates the logarithm to a linear expression via unfolding and log rules, then applies hasDerivAt to the constant and linear summands.
claimLet $a = 4π·11$ and define $α^{-1}(g) := a · exp(-g/a)$ for real $g$. Then $d/dg [ln(α^{-1}(g))] = -1/a$.
background
Alpha seed is defined as $4π·11$, the geometric baseline from ledger structure representing spherical closure cost over 11-edge paths. The function alpha inverse of gap is the noncomputable definition $a · exp(-g/a)$, which matches the canonical formula in the module for the inverse fine-structure constant parameterized by gap. The module setting treats this exponential form as a structural ansatz whose positivity and differential properties are verified before addressing uniqueness; upstream results supply the seed positivity and the gap-parameterized definition.
proof idea
The tactic proof first obtains positivity of alpha inverse of gap from seed positivity and exp positivity. It then proves the logarithm identity by unfolding the definition and applying log_mul together with log_exp. Funext equates the target function to the explicit linear form log seed minus g over seed. Separate hasDerivAt facts are constructed for the constant term (zero derivative) and the linear term (via id, division by constant, and negation), added, and the zero summand is dropped to yield the constant derivative.
why it matters in Recognition Science
This theorem supplies the constant logarithmic derivative that feeds the downstream uniqueness ODE principle, which records that a constant log derivative implies the exponential solution under standard ODE theory. It advances the module's goal of identifying the differential equation satisfied by the exponential form, linking to the J-cost log-coordinate expansion whose Taylor coefficients match those of the exponential. The open question remains why the derivative must be constant in the Recognition derivation rather than some other functional form.
scope and limits
- Does not derive the exponential ansatz from the Recognition Composition Law.
- Does not prove uniqueness of the form against other candidates such as rational or power-law alternatives.
- Does not compute or bound higher-order derivatives beyond the first.
- Does not connect the derivative result to the phi-ladder or mass formulas.
formal statement (Lean)
155theorem logarithmic_derivative_constant (g : ℝ) :
156 deriv (fun g => Real.log (alphaInv_of_gap g)) g = -(1 / alpha_seed) := by
proof body
Tactic-mode proof.
157 have hpos : 0 < alphaInv_of_gap g := by
158 unfold alphaInv_of_gap
159 exact mul_pos alpha_seed_positive (Real.exp_pos _)
160 have h_log_eq : ∀ g, Real.log (alphaInv_of_gap g) =
161 Real.log alpha_seed + (-(g / alpha_seed)) := by
162 intro g
163 unfold alphaInv_of_gap
164 rw [Real.log_mul (ne_of_gt alpha_seed_positive) (ne_of_gt (Real.exp_pos _)), Real.log_exp]
165 -- deriv of (Real.log α_seed + (-(g / α_seed))) = deriv of (-(g/α_seed)) = -1/α_seed
166 have h_fun_eq : (fun g => Real.log (alphaInv_of_gap g)) =
167 (fun g => Real.log alpha_seed + (-(g / alpha_seed))) := by
168 funext g
169 exact h_log_eq g
170 rw [h_fun_eq]
171 have h_const_derivable : HasDerivAt (fun _ : ℝ => Real.log alpha_seed) 0 g :=
172 hasDerivAt_const g _
173 have h_lin_derivable : HasDerivAt (fun g => -(g / alpha_seed)) (-(1 / alpha_seed)) g := by
174 have h1 : HasDerivAt (fun g : ℝ => g) 1 g := hasDerivAt_id g
175 have h2 : HasDerivAt (fun g : ℝ => g / alpha_seed) (1 / alpha_seed) g :=
176 h1.div_const alpha_seed
177 exact h2.neg
178 have : HasDerivAt (fun g => Real.log alpha_seed + (-(g / alpha_seed))) (0 + -(1 / alpha_seed)) g :=
179 h_const_derivable.add h_lin_derivable
180 rw [zero_add] at this
181 exact this.deriv
182
183/-! ## Part 4: Inheritance from J-Cost Log Structure
184
185The J-cost J(x) = cosh(ln x) - 1 has Taylor expansion in log coordinates:
186
187 J(e^t) = cosh(t) - 1 = Σ t^(2n)/(2n)! = t²/2 + t⁴/24 + t⁶/720 + ...
188
189The factorial coefficients 1/(2n)! come from the d'Alembert uniqueness proof
190(washburn_uniqueness_aczel). Any cost functional satisfying the RCL has these
191coefficients in its log-coordinate expansion.
192
193The exponential form α_seed · exp(-f_gap/α_seed) inherits factorial
194coefficients in its Taylor expansion around f_gap = 0, and these match the
195coefficients in the J-cost expansion.
196-/
197
198/-- The first-order (linear) term of α⁻¹ in f_gap: matches a naive
199 perturbative expansion. -/