Physics Fine Structure Derivation5

A boundary datum, not a prediction

The fine-structure constant α is a dimensionless number, about 1/137.036, that sets the strength of the electromagnetic force between charged particles. It is one of the most precisely measured quantities in physics: CODATA 2022 gives 1/α = 137.035999177(21), meaning the uncertainty is in the ninth decimal place. Any theory that claims to explain α must land inside that tiny window, not merely near it.

In Recognition Science, the framework's library of machine-checked formal theorems contains a module called FineStructure_Derivation5. Its name suggests it derives the fine-structure constant. The actual content is far more modest. The module defines a cost function, a measure of the price of a recognition event, applied to the ratio m/e of two real numbers. It proves three general facts: the cost is zero when m equals e, the cost is never negative for positive inputs, and the golden ratio minus 3/2 is positive. These are true for any positive numbers m and e. The module never defines m and e in terms of the electron charge or any other physical quantity.

An earlier research note attached to the module claimed a prediction: that α⁻¹ falls in the band (137.030, 137.039), which contains the CODATA value. The framework's own later audit convicted that reading. The band is roughly 429,000 times wider than the measurement's precision, so the claim could not have failed. The construction's central value is excluded at more than 30,000 standard deviations, and a no-go theorem proves that no normalization-blind condition can pin the coupling. In plain terms: the module proves harmless facts about a generic cost function, and the specific physical prediction was an overreach.

What the module does establish, honestly, is a template. The same three facts are stated once, universally, in a shared template module, and this file instantiates them. The framework's current position is that α⁻¹ is a boundary datum, an input to the framework, not an output. The exact value of α remains an open target.

def canonicalThreshold : ℝ := phi - 3 / 2

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

noncomputable def cert : FineStruct5Cert where
  cost_at_eq := domainCost_at_eq
  cost_nonneg := domainCost_nonneg
  threshold_pos := canonicalThreshold_pos

What this page does not claim

This module does not derive the fine-structure constant. The three proved facts do not depend on any physical interpretation of m and e. The earlier band prediction is not a supported result of 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/Physics/FineStructure_Derivation5.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: