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)
161def partial_alpha (alpha_s f_g : ℝ) (deltas : ℕ → ℝ) (N : ℕ) : ℝ :=
proof body
Definition body.
162 alpha_s - f_g + (Finset.range N).sum (fun n => deltas (n + 1))
163
164/-! ## CODATA Target -/
165
166/-- CODATA 2022 value of α⁻¹. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
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
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use