Constants Fine Structure Constant Alpha Lock Pos

The kernel exponent

The fine-structure constant α is a dimensionless number near 1/137 that sets the strength of electromagnetic interactions. In the Recognition Science framework, a separate quantity called alphaLock (α_lock) appears, and its name has caused confusion. The machine-checked library of formal theorems contains a declaration, alphaLock_pos, that proves α_lock is greater than zero. This is a narrow, precise claim: the number is positive, and that is all the declaration itself establishes.

The framework defines α_lock as (1 − 1/φ)/2, where φ is the golden ratio. Because φ is approximately 1.618, this expression evaluates to roughly 0.19. The library also proves α_lock is less than 1, and therefore lies in the open unit interval between 0 and 1. A further theorem gives coarse numerical bounds: α_lock is between 0.18 and 0.21. These facts follow from the definition and the known bounds on φ; they are formal results in the library, not measurements or empirical fits.

In Recognition Science, α_lock is the information-limited-gravity kernel exponent. It is a structural constant that emerges from the framework's forcing chain, which derives physical structure from a discrete record of recognition events. The number 0.19 appears in the framework's account of gravity, not in electromagnetism. The framework's own documentation is explicit on this point: α_lock is NOT the electromagnetic fine-structure constant, which is about 0.0073, and no conversion between the two exists in the repository.

What alphaLock_pos does not do is as important as what it does. It does not derive, predict, or explain the fine-structure constant. The exact value of the fine-structure constant remains an open target within the framework, treated as a free boundary datum rather than a forced consequence. An earlier claim that α_lock resolved the question of what determines α has been formally retracted. The declaration is a theorem about a defined quantity's positivity, and nothing more.

/-- α_lock > 0 (re-export from Constants). -/
theorem alphaLock_pos : 0 < alphaLock := Constants.alphaLock_pos

/-- α_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 < 1 (re-export from Constants). -/
theorem alphaLock_lt_one : alphaLock < 1 := Constants.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

This answer does not claim alphaLock is the fine-structure constant or that it determines it. This answer does not claim the fine-structure constant is derived within the framework. This answer does not claim alphaLock has any measured physical counterpart.

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: