Constants Alpha Genesis Residual Target Residual Bounds

The residual band

The fine-structure constant α measures the strength of the electromagnetic force between charged particles. Its inverse, about 137.036, is one of the most precisely measured numbers in physics. The Recognition Science framework derives a candidate value for this inverse from its own axioms. The declaration residual_bounds is a machine-checked theorem stating that the difference between the framework's first-order value and the measured value, the residual, lies strictly between −0.006 and 0.0031. This is a proven bound, not a guess: the framework's library of formal theorems verifies it.

The framework's first-order derivation is blind to the measured value by design. The comparison happens only in this quarantine module, which states the residual band and the open target. The band is narrow: relative to 137, a residual of 0.006 is about 44 parts per million. The theorem does not say the derivation is exact. It says the first-order value is close, and it quantifies how close.

The same module proves a sharper structural fact. If a second-order correction is forced to enter as additional spectral load, multiplicatively in the exponent, then there is exactly one such load that makes the dressed value equal the measured value. The framework writes this unique load in closed form and calls it the closing load. The theorem existsUnique_closingLoad proves this uniqueness: the dressed value is strictly decreasing in the load, so exactly one value closes the residual.

In Recognition Science, this is the sharply localized open problem. The closing load is a single number. The open target is to derive that number from the seam topology of the D=3 voxel lattice, using a procedure that never references the measured value. If a blind derivation lands on the closing load, the α program closes at experimental precision. If it lands elsewhere, the channel-budget bridge is wrong and the assembly is falsified at that layer.

The declaration does not claim the closing load is derived. It is defined, and its uniqueness is proved, but its origin from lattice geometry is OPEN. The anti-epicycle rule is binding: no candidate may be admitted on numerical proximity alone. The candidate catalogue is a search record, not a derivation. The residual band is a theorem; the seam derivation is a target.

/-- 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

What this page does not claim

The closing load is derived from lattice geometry. The residual band is a prediction that the framework's value is correct within experimental error. The candidate catalogue in Verification/AlphaCorrectionAnalysis.lean is a derivation.

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: