def definition def or abbrev

`alphaInverseUpper`

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

formal statement (Lean)

  31def alphaInverseUpper : ℝ := 137.039

Definition body.

  32
  33/-- The CODATA 2022 value lies inside the RS band. -/

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

AlphaProvenanceCert in IndisputableMonolith.Foundation.AlphaDerivationExplicit decl_use
codata_in_band in IndisputableMonolith.Foundation.AlphaDerivationExplicit decl_use

Lean names referenced from this declaration's body.