Constants Alpha Genesis Residual Target Seam Derivation Closes

The seam test

The fine-structure constant α measures the strength of the electromagnetic force between charged particles, roughly 1/137. It is one of the most precisely measured numbers in physics, yet no theory explains why it has that value. In the Recognition Science framework, a first-order derivation from a few structural principles lands close to the measured value, but not exactly on it. The residual, the difference between the framework's value for 1/α and the measured value, is confined to the interval (−0.006, 0.0031), a theorem in the framework's machine-checked library of formal theorems.

The framework models the gap as a second-order correction that must enter as additional spectral load, a multiplicative factor inside an exponent, never as an additive patch to the displayed value. The legacy additive correction is retired. The framework proves that exactly one value of this load, written in closed form as closingLoad, makes the dressed value equal to the measured one. The proof shows the corrected value is strictly decreasing in the load, so the matching value is unique.

In Recognition Science, the declaration SeamDerivationCloses establishes the test for finishing the program. It is a definition, not a proof: for any candidate load δ₂, SeamDerivationCloses δ₂ holds if and only if δ₂ equals closingLoad. The theorem seam_closes_iff proves this equivalence. The open problem is to derive that one number from the seam topology of a three-dimensional voxel lattice, using a procedure that never references the measured value. If a blind derivation lands on closingLoad, the α derivation closes at experimental precision. If it lands elsewhere, the channel-budget bridge, the one named input of the derivation, is wrong and the assembly is falsified at that layer.

The declaration does not claim that the closing load has been derived. It does not claim that the fine-structure constant has been explained. It states the precise condition under which a future derivation would succeed or fail, and it binds the framework to an anti-epicycle rule: no candidate load may be admitted to the certified surface on the basis of numerical proximity to closingLoad. Admission requires a forced derivation from lattice geometry. The candidate catalogue in the verification files is a search record, not a derivation, and must not be cited as one.

/-- The certified band confines the residual to `(−0.006, 0.0031)`. -/
theorem residual_bounds : (-0.006 : ℝ) < residual ∧ residual < (0.0031 : ℝ) := by
  unfold residual
  have hgt := Numerics.alphaInv_gt
  have hlt := Numerics.alphaInv_lt
  have hC : alpha_inv_CODATA = (137.035999177 : ℝ) := rfl
  constructor
  · rw [hC]; linarith
  · rw [hC]; linarith

/-- There is exactly one closing load. -/
theorem existsUnique_closingLoad :
    ∃! δ₂ : ℝ, correctedAlphaInv δ₂ = alpha_inv_CODATA := by
  refine ⟨closingLoad, corrected_at_closingLoad, ?_⟩
  intro δ h
  exact (corrected_eq_codata_iff δ).mp h

theorem seam_closes_iff (δ₂ : ℝ) : SeamDerivationCloses δ₂ ↔ δ₂ = closingLoad :=
  corrected_eq_codata_iff δ₂

What this page does not claim

The closing load has been derived from seam geometry. The fine-structure constant has been explained. The value 1/α = 137.035999177 is derived by the framework.

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/ResidualTarget.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: