Constants Alpha Genesis Resummation Forcing No Additive Response

The additive form

In the Recognition Science framework, a ledger is a discrete record of events, and the framework models physical quantities as outcomes of forced accounting rules. One quantity it examines is a dressing response: the fraction of a coupling budget that survives a gap load ε. The question is what form that survival fraction can take. The simplest guess, a linear decrease, is ε ↦ 1 − ε. The theorem no_additive_response rules this guess out.

The reason is not an empirical measurement but a structural contradiction. The framework requires that independent gap loads compose multiplicatively: the survival fraction for two independent loads must equal the product of the survival fractions for each alone. For the additive form, this fails outright. Take ε₁ = 1 and ε₂ = 1. The left side gives 1 − 2 = −1, while the right side gives (1 − 1)(1 − 1) = 0. A negative survival fraction is already meaningless, and −1 ≠ 0 shows the multiplicative law cannot hold. The theorem additive_map_not_factorizing states this failure as a general fact about the additive map, independent of any response structure.

The framework's positive result is that any dressing response satisfying the multiplicative law and a unit linear response at zero load must be the exponential ε ↦ exp(−ε). This is the theorem response_forced. The additive form is then not a competing structural alternative but merely the first-order truncation of the exponential, a display that happens to match near ε = 0 and diverges everywhere else. The dressed coupling that results is seed times the forced exponential response, stated in dressedCoupling_forced.

What no_additive_response does not claim is broader than what it proves. It does not claim that the exponential form is the only function satisfying the multiplicative law; without the calibration condition, other functions exist. It does not claim that the additive form fails because of any physical measurement or experimental constraint. And it does not claim that the fine-structure constant itself is derived; the seed value 44π remains an identification, not a derived coupling.

/-- The additive map fails the factorization law outright (independent of any
response structure). -/
theorem additive_map_not_factorizing :
    ¬ (∀ x y : ℝ, (1 - (x + y)) = (1 - x) * (1 - y)) := by
  intro h
  have h11 := h 1 1
  norm_num at h11

/-- **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 exponential is the only function satisfying the multiplicative law without the calibration condition. The additive form fails because of any physical measurement. The fine-structure constant itself is derived; the seed 44π is an identification.

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: