Constants Alpha Genesis Resummation Forcing G Zero

The zero-load condition

The declaration g_zero is a small, precise statement inside a larger argument about how a coupling constant changes when a system pays a cost. In plain language, it says: when the cost, or gap load, is zero, the fraction of the coupling that survives is exactly one. Nothing is lost, nothing is gained. The statement is a theorem, not an assumption, and it follows from two conditions the framework imposes on any dressing response.

A dressing response is the framework's term for a function that tells you what fraction of a coupling budget survives after a gap load ε is paid. The first condition is factorization: if two independent loads are paid, the survival fractions multiply. The second is calibration: the response has unit linear response at zero load, meaning its derivative at zero is minus one. The theorem g_zero proves that these two conditions force g(0) = 1. The alternative, g(0) = 0, would make the entire response identically zero, which contradicts the calibration condition. So the zero-load case is settled: no load, no dressing.

This result is the first rung of a longer proof. The same two premises, factorization and calibration, force the entire response to be the exponential function, g(ε) = exp(−ε). That forcing result, response_forced, is what removes any freedom in how the framework dresses its seed coupling. The additive approximation 1 − ε, which could look like a simpler alternative, fails the factorization law outright, as the theorem no_additive_response shows with the witness ε₁ = ε₂ = 1. The exponential is not one choice among many; it is the only choice the premises allow.

What g_zero does not claim is just as important. It does not by itself establish the exponential form; that requires the full forcing theorem. It does not say anything about the numerical value of the fine-structure constant or any other physical constant. It is a statement about a function's behavior at a single point, derived from structural conditions, not a measurement or a claim about the empirical world. The theorem is a piece of the framework's internal machinery, a lemma that makes the later, larger claims possible.

/-- Zero load means no dressing: `g(0) = 1`. (The alternative `g(0) = 0`
forces `g ≡ 0`, contradicting the unit response.) -/
theorem g_zero : R.g 0 = 1 := by
  have h : R.g 0 = R.g 0 * R.g 0 := by
    have h0 := R.factorizes 0 0
    simpa using h0
  have hz : R.g 0 * (R.g 0 - 1) = 0 := by
    rw [mul_sub, mul_one, ← h, sub_self]
  rcases mul_eq_zero.mp hz with h0 | h1
  · exfalso
    have hall : ∀ x, R.g x = 0 := by
      intro x
      have hx := R.factorizes x 0
      simpa [h0] using hx
    have hconst : R.g = fun _ => (0 : ℝ) := funext hall
    have hd : HasDerivAt (fun _ : ℝ => (0 : ℝ)) (-1) 0 := by
      have hur := R.unit_response
      rw [hconst] at hur
      exact hur
    have hzero : ((-1 : ℝ)) = 0 := hd.unique (hasDerivAt_const 0 0)
    norm_num at hzero
  · linarith [sub_eq_zero.mp h1]

/-- **RESUMMATION FORCING.** Any factorizing dressing response with unit
linear response is exactly the exponential: `g(ε) = exp(−ε)`. There is no
resummation freedom. -/
theorem response_forced : ∀ ε : ℝ, R.g ε = Real.exp (-ε) := by
  -- h(x) = g(x)·exp(x) has zero derivative everywhere, hence is constant 1.
  have hd : ∀ x : ℝ, HasDerivAt (fun y : ℝ => R.g y * Real.exp y) 0 x := by
    intro x
    have hmul := (R.hasDerivAt_neg_self x).mul (Real.hasDerivAt_exp x)
    convert hmul using 1
    ring
  have hdiff : Differentiable ℝ (fun y : ℝ => R.g y * Real.exp y) :=
    fun x => (hd x).differentiableAt
  have hderiv : ∀ x : ℝ, deriv (fun y : ℝ => R.g y * Real.exp y) x = 0 :=
    fun x => (hd x).deriv
  have hconst : ∀ x : ℝ, R.g x * Real.exp x = R.g 0 * Real.exp 0 := by
    intro x
    exact is_const_of_deriv_eq_zero hdiff hderiv x 0
  intro ε
  have hε : R.g ε * Real.exp ε = 1 := by
    have hx := hconst ε
    simpa [R.g_zero] using hx
  have hexp : Real.exp ε ≠ 0 := (Real.exp_pos ε).ne'
  have hgε : R.g ε = (Real.exp ε)⁻¹ := by
    have h2 := congrArg (· * (Real.exp ε)⁻¹) hε
    simpa [mul_assoc, mul_inv_cancel₀ hexp] using h2
  rw [hgε, ← Real.exp_neg]

/-- **ADDITIVE FORM EXCLUDED.** No dressing response is the additive display
`ε ↦ 1 − ε`: it fails factorization (witness ε₁ = ε₂ = 1). Form (A) is a
truncation of form (E), not a structural alternative. -/
theorem no_additive_response : R.g ≠ fun ε => 1 - ε := by
  intro hcontra
  have h := R.factorizes 1 1
  rw [hcontra] at h
  norm_num at h

What this page does not claim

The theorem g_zero does not by itself establish the exponential form of the dressing response. The theorem g_zero does not make any claim about the numerical value of the fine-structure constant or any other physical constant. The theorem g_zero is not a measurement and does not depend on any empirical data.

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/AlphaGenesis/ResummationForcing.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: