Verification Alpha Resolution Pass2

The closure target

The fine-structure constant α is the number that sets the strength of electromagnetic interactions. Its inverse, 1/α, is measured with extraordinary precision: the CODATA 2022 adjustment gives 1/α = 137.035999177(21). Recognition Science (RS) has a symbolic expression for 1/α, built from its own geometric ingredients, but that expression does not exactly match the measured value. The module called Alpha Resolution Pass 2 does one precise thing: it defines the exact additive correction that would close the gap, and proves that with that correction the RS value lands exactly inside the CODATA error band.

The correction is not a discovery. The module defines it as the difference between the CODATA value and the RS expression: δ = 1/α_CODATA − 1/α_RS. The central theorem is then almost arithmetic: adding the correction to the RS value gives the CODATA value exactly, because the correction was defined as the difference. The module proves this identity, along with a uniqueness statement: any additive correction that aligns the RS value to CODATA must equal this one. There is exactly one such correction, and the module proves that too.

What the module does not do is derive the correction from RS geometry. That status is explicit and load-bearing. A boolean flag inside the module, closure_term_derived_from_geometry, is set to false. The docstring explains why: the forced sector of RS, the part that follows from the recognition ledger without extra input, cannot produce this residual at all. A separate theorem in the library proves that no normalization-blind condition can pin the coupling. Any future derivation would need to reference the U(1) kinetic normalization, which would be added physical input, not forced combinatorics.

The module also proves a set of uniqueness facts about the curvature term δ_κ = −103/(102·π⁵). If a correction of the form −103/(102·π^d) matches δ_κ, then d must equal 5. If the form is −103/(k·π⁵), then k must equal 102. If the form is −n/(102·π⁵), then n must equal 103. These are packaged into a bundled theorem. They confirm that the integers 103, 102, and 5 are the only ones that work, but they do not explain why those integers appear.

The honest summary is this: the module converts a numerical discrepancy into a named, unique, and formally recorded target. The target is not derived, and the module says so in its own status flag. What stands on its own is the alignment arithmetic and the uniqueness of the correction. The next step, deriving that correction from first principles, remains open, and the module marks it as such.

/-- The corrected value equals CODATA exactly, because the correction is defined
as the difference. `x + (c − x) = c` is the whole content; it is arithmetic, not
a result about α. -/
theorem alphaInv_corrected_eq_CODATA :
    alphaInv_corrected = alpha_inv_CODATA := by
  unfold alphaInv_corrected deltaAlphaInv_geometric
  simp [alphaInv]

/-- There exists a unique additive closure term producing exact CODATA alignment. -/
theorem exists_unique_exact_alignment_closure :
    ∃! δ : ℝ, alphaInv + δ = alpha_inv_CODATA := by
  refine ⟨deltaAlphaInv_geometric, ?_, ?_⟩
  · simpa [alphaInv_corrected] using alphaInv_corrected_eq_CODATA
  · intro δ hδ
    exact (additive_closure_unique_for_exact_alignment δ).1 hδ

/-- Status marker: **the closure term has not been derived from geometry.**

Flipped from `true` to `false` on 2026-07-25. It was reading "written in seed/gap
form" as "derived from geometry", but the term still has `alpha_inv_CODATA` as
its leading summand, so it is the measured residual in a different notation. The
module header always said as much; this marker contradicted it.

Deriving it is not merely open, it is closed off for the forced sector:
`Constants/AlphaGenesis/KappaGammaIrreducibility.lean` proves no
normalization-blind condition can pin the coupling. Any future derivation must
reference the U(1) kinetic normalization, which makes it added physical input
rather than forced ledger combinatorics. -/
def closure_term_derived_from_geometry : Bool := false

/-- Verification-layer lift of curvature exponent uniqueness:
if a power-family correction matches the canonical curvature term, its exponent
is forced to `5`. -/
theorem curvature_exponent_forced_in_power_family (d : ℕ) :
    (-(103 : ℝ) / (102 * Real.pi ^ d) = delta_kappa) ↔ d = 5 := by
  -- `delta_kappa` is the canonical curvature term `-(103)/(102*π^5)`.
  simpa [delta_kappa] using curvature_power_family_eq_canonical_iff d

What this page does not claim

This module does not derive the fine-structure constant from RS geometry. The uniqueness facts about the integers 103, 102, and 5 do not explain why those integers appear. The corrected value matching CODATA exactly is arithmetic, not evidence that the RS formula is correct.

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/Verification/AlphaResolutionPass2.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: