Constants Alpha Exponential Form Deriv Alpha Inv Of Gap

The exponential form and its rate

The inverse fine-structure constant, written α⁻¹, is a pure number near 137.036 that sets the strength of electromagnetic interactions. The Recognition Science framework proposes a specific exponential formula for it: α⁻¹ = α_seed · exp(−f_gap / α_seed), where α_seed = 4π¹¹ and f_gap is a framework-internal quantity built from the golden ratio. The declaration deriv_alphaInv_of_gap establishes a precise fact about this formula: if you treat α⁻¹ as a function of the gap f_gap, its instantaneous rate of change equals −α⁻¹ / α_seed. In plain terms, the value decreases at a rate proportional to its own size, which is the signature of exponential decay.

This derivative statement is a proved theorem in the framework's machine-checked library of formal theorems. It follows directly from the definition of the exponential function and carries no additional assumptions. The same library also proves that the logarithmic derivative is constant: d ln(α⁻¹)/d(f_gap) = −1/α_seed. That constancy means the relative rate of change is the same at every value of the gap, a property sometimes called scale-free running. At f_gap = 0 the function returns exactly α_seed, and its first derivative there is −1, matching a naive linear approximation α_seed − f_gap.

What the declaration does not claim is more important than what it proves. The exponential form itself is a definition, not a derived consequence. The framework's own documentation states plainly that the formula is a structural choice inherited from the log-coordinate behavior of the J-cost function, not a unique outcome forced by first principles. The integer 44 in α_seed = 4π¹¹ is proved as a combinatorial identity, but its identification as the seed coupling is not forced. The exponential form is distinguished from alternatives like α_seed / (1 + f_gap/α_seed) by higher-order structure, but the library does not prove that the exponential Taylor coefficients are uniquely required.

The genuine open question is why the logarithmic derivative should be constant at all. A candidate uniqueness statement exists as an unproved proposition: if a smooth positive function g satisfies g(0) = α_seed, g′(0) = −1, and has constant logarithmic derivative −1/α_seed, then g must be the exponential form. This follows from standard ODE theory and is provable in principle, but the physical justification for the constant-log-derivative assumption remains a bridge claim between the formalism and physics. The exact value α⁻¹(0) = 137.035999 stays a boundary datum, closed by a separate no-go result, not derived from the exponential structure.

/-- The derivative of alphaInv with respect to f_gap. -/
theorem deriv_alphaInv_of_gap (g : ℝ) :
    deriv alphaInv_of_gap g = -(alphaInv_of_gap g / alpha_seed) := by
  unfold alphaInv_of_gap
  -- h1: derivative of g → -(g/alpha_seed) is -(1/alpha_seed)
  have h_id : HasDerivAt (fun g : ℝ => g) 1 g := hasDerivAt_id g
  have h_div : HasDerivAt (fun g : ℝ => g / alpha_seed) (1 / alpha_seed) g :=
    h_id.div_const alpha_seed
  have h1 : HasDerivAt (fun g : ℝ => -(g / alpha_seed)) (-(1 / alpha_seed)) g :=
    h_div.neg
  -- h2: derivative of exp(-(g/alpha_seed))
  have h2 : HasDerivAt (fun g : ℝ => Real.exp (-(g / alpha_seed)))
      (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed))) g :=
    (Real.hasDerivAt_exp _).comp g h1
  -- h3: scale by alpha_seed
  have h3 : HasDerivAt (fun g : ℝ => alpha_seed * Real.exp (-(g / alpha_seed)))
      (alpha_seed * (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed)))) g :=
    h2.const_mul alpha_seed
  -- Simplify the derivative expression
  have heq : alpha_seed * (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed)))
       = -(alpha_seed * Real.exp (-(g / alpha_seed)) / alpha_seed) := by
    field_simp
  rw [← heq]
  exact h3.deriv

/-- The logarithmic derivative: d ln(α⁻¹)/d(f_gap) = -1/α_seed (constant). -/
theorem logarithmic_derivative_constant (g : ℝ) :
    deriv (fun g => Real.log (alphaInv_of_gap g)) g = -(1 / alpha_seed) := by
  have hpos : 0 < alphaInv_of_gap g := by
    unfold alphaInv_of_gap
    exact mul_pos alpha_seed_positive (Real.exp_pos _)
  have h_log_eq : ∀ g, Real.log (alphaInv_of_gap g) =
      Real.log alpha_seed + (-(g / alpha_seed)) := by
    intro g
    unfold alphaInv_of_gap
    rw [Real.log_mul (ne_of_gt alpha_seed_positive) (ne_of_gt (Real.exp_pos _)), Real.log_exp]
  -- deriv of (Real.log α_seed + (-(g / α_seed))) = deriv of (-(g/α_seed)) = -1/α_seed
  have h_fun_eq : (fun g => Real.log (alphaInv_of_gap g)) =
      (fun g => Real.log alpha_seed + (-(g / alpha_seed))) := by
    funext g
    exact h_log_eq g
  rw [h_fun_eq]
  have h_const_derivable : HasDerivAt (fun _ : ℝ => Real.log alpha_seed) 0 g :=
    hasDerivAt_const g _
  have h_lin_derivable : HasDerivAt (fun g => -(g / alpha_seed)) (-(1 / alpha_seed)) g := by
    have h1 : HasDerivAt (fun g : ℝ => g) 1 g := hasDerivAt_id g
    have h2 : HasDerivAt (fun g : ℝ => g / alpha_seed) (1 / alpha_seed) g :=
      h1.div_const alpha_seed
    exact h2.neg
  have : HasDerivAt (fun g => Real.log alpha_seed + (-(g / alpha_seed))) (0 + -(1 / alpha_seed)) g :=
    h_const_derivable.add h_lin_derivable
  rw [zero_add] at this
  exact this.deriv

/-- The first-order (linear) term of α⁻¹ in f_gap: matches a naive
    perturbative expansion. -/
theorem alphaInv_linear_term :
    alphaInv_of_gap 0 = alpha_seed := by
  unfold alphaInv_of_gap
  simp [Real.exp_zero]

/-- The first derivative at f_gap = 0: rate of decrease is -1 per unit
    gap (independent of α_seed at leading order). -/
theorem alphaInv_linear_rate :
    deriv alphaInv_of_gap 0 = -1 := by
  rw [deriv_alphaInv_of_gap]
  rw [alphaInv_linear_term]
  field_simp

/-- The alphaInv function parameterized by f_gap value. -/
noncomputable def alphaInv_of_gap (g : ℝ) : ℝ := alpha_seed * Real.exp (-(g / alpha_seed))

What this page does not claim

The exponential form of α⁻¹ is uniquely forced by Recognition Science structure. The exact numerical value 137.035999 is derived from the exponential formula. The identification of 44 = 4·11 as the seed coupling is forced; only the combinatorial identity 11 = passive edges of Q₃ is proved.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/AlphaExponentialForm.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: