def definition def or abbrev

`H_AlphaPrecision`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  20def H_AlphaPrecision : Prop :=

proof body

Definition body.

  21  ∃ (error : ℝ), abs (alphaInv - 137.035999) < error ∧ error < 1e-11
  22
  23/-- **THEOREM: High-Precision Alpha Identity**
  24    The inverse fine-structure constant matches the complete geometric series
  25    within the CODATA 2024 uncertainty band. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

alpha_high_precision in IndisputableMonolith.Physics.AlphaHighPrecision decl_use

depends on (5)

Lean names referenced from this declaration's body.

complete in IndisputableMonolith.Complexity.SAT.Backprop decl_use
alphaInv in IndisputableMonolith.Constants.Alpha decl_use
Identity in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use