recognition / Constants / Constants.FineStructureConstant / fine_structure_derived

theorem

`fine_structure_derived`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.FineStructureConstant
domain: Constants
line: 67 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.FineStructureConstant on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

AlphaLock Window in the Unit Interval · derived / THEOREM
The locked alpha lives in (0,1); the certified numerical bounds reproduce the CODATA value

depends on

formal source

  64
  65    Relationship to measured α ≈ 1/137 requires the conversion
  66    from RS-native to SI units (λ_rec calibration). -/
  67theorem fine_structure_derived :
  68    0 < alphaLock ∧ alphaLock < 1 ∧
  69    alphaLock = (1 - 1 / phi) / 2 :=
  70  ⟨alphaLock_pos, alphaLock_lt_one, rfl⟩
  71
  72end FineStructureConstant
  73end Constants
  74end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.