No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
51theorem alpha_value : alpha_approx = 1/137 := rfl
proof body
Term-mode proof.
52
53/-- The Lamb shift as a fraction of the 2S binding energy.
54 E_2S ≈ -3.4 eV, Lamb shift ≈ 4.4 μeV. -/
depends on (8)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
alpha_approx
in IndisputableMonolith.QFT.LambShift
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use