Constants Fine Structure Constant

The ILG kernel exponent

The module FineStructureConstant defines a number called alphaLock, the information-limited gravity kernel exponent. Its value is (1 − 1/φ)/2, approximately 0.19, where φ is the golden ratio. The module establishes that alphaLock lies strictly between 0 and 1, and that it equals this φ-structural expression. These are the module's core theorems: bounds and structure.

The module's historical name is misleading. alphaLock is not the electromagnetic fine-structure constant α, whose measured value is about 1/137, or 0.0073. No conversion between alphaLock and α exists in the repository. The earlier claim that alphaLock resolves the question of what determines α is retracted. The honest position, stated in Constants.AlphaGenesis, is that the exact value of α⁻¹(0) remains a free boundary datum within Recognition Science, and the first-order construction value is excluded by measurement.

What the module establishes, in plain language, is a structural fact about a kernel exponent, not a derivation of a fundamental constant of electromagnetism. The theorems are machine-checked and axiom-clean. The number 0.19 is forced by the golden ratio through the framework's cost function, but it does not connect to the laboratory value of α. The module's value is in clarifying what Recognition Science does and does not claim about the fine-structure constant, and in securing recognition of that boundary.

THEOREM alphaLock_structure · IndisputableMonolith/Constants/FineStructureConstant.lean

THEOREM alphaLock_in_unit_interval · IndisputableMonolith/Constants/FineStructureConstant.lean

THEOREM alphaLock_structure · IndisputableMonolith/Constants/FineStructureConstant.lean

What this page does not claim

This module derives the electromagnetic fine-structure constant α. alphaLock is a step toward a ledger-to-lab conversion for α. The exact value of α is determined within Recognition Science.

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: