Constants Fine Structure Constant Alpha Lock Lt One

The alphaLock bound

The fine-structure constant α is the dimensionless number, approximately 1/137.036, that sets the strength of electromagnetic interactions between charged particles. It is one of the most precisely measured quantities in physics. The Recognition Science framework does not derive this constant. Its exact value remains an open problem within the framework, treated as a free boundary datum in its internal formalism.

What the framework does prove is a statement about a different number, called alphaLock. This is defined as (1 − 1/φ)/2, where φ is the golden ratio, approximately 1.618. The number alphaLock is approximately 0.19098. A theorem in the framework's machine-checked library of formal theorems establishes that this number lies strictly between 0 and 1. The declaration alphaLock_lt_one is the specific part of this theorem stating that alphaLock is less than 1.

This bound is a structural fact about alphaLock's definition, not a physical measurement. It follows directly from the definition and the known bounds on the golden ratio. The framework's library also proves a coarse numerical bound: alphaLock is between 0.18 and 0.21. These are formal statements about a real number defined within the framework's mathematics.

In Recognition Science, alphaLock plays a role as an exponent in a kernel related to information-limited gravity. The name is historical and misleading. The framework's own documentation explicitly retracts any earlier suggestion that alphaLock determines the electromagnetic fine-structure constant. No conversion between the two exists in the framework's library. The exact value of the electromagnetic α is not derived, and a first-order construction value is excluded by measurement comparison.

/-- α_lock < 1 (re-export from Constants). -/
theorem alphaLock_lt_one : alphaLock < 1 := Constants.alphaLock_lt_one

/-- α_lock structure: `alphaLock = (1 − 1/φ)/2` with unit-interval bounds.
    This is a φ-structural fact about the ILG kernel exponent. It does NOT
    determine the EM fine-structure constant; see the module header. -/
theorem alphaLock_structure :
    0 < alphaLock ∧ alphaLock < 1 ∧
    alphaLock = (1 - 1 / phi) / 2 :=
  ⟨alphaLock_pos, alphaLock_lt_one, rfl⟩

@[deprecated alphaLock_structure (since := "2026-07-06")]
alias fine_structure_derived := alphaLock_structure

/-- α_lock lies in the open unit interval. -/
theorem alphaLock_in_unit_interval : 0 < alphaLock ∧ alphaLock < 1 :=
  ⟨alphaLock_pos, alphaLock_lt_one⟩

/-- α_lock is between 0.18 and 0.21 (coarse bound from φ ∈ (1.61, 1.62)). -/
theorem alphaLock_numerical_bounds :
    (0.18 : ℝ) < alphaLock ∧ alphaLock < (0.21 : ℝ) := by
  unfold alphaLock
  have h_phi := phi_gt_onePointSixOne
  have h_phi' := phi_lt_onePointSixTwo
  constructor
  · have h_inv : 1 / phi < 1 / 1.61 := by
      rw [div_lt_div_iff_of_pos_left (by norm_num) phi_pos (by norm_num)]
      exact h_phi
    linarith
  · have h_inv : 1 / 1.62 < 1 / phi := by
      rw [div_lt_div_iff_of_pos_left (by norm_num) (by norm_num) phi_pos]
      exact h_phi'
    linarith

What this page does not claim

alphaLock is the fine-structure constant or any approximation to it. The framework derives the exact value of the electromagnetic fine-structure constant. The bound on alphaLock has any direct physical consequence for electromagnetism.

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