def definition def or abbrev

`H_GPrecision`

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

formal statement (Lean)

  19def H_GPrecision : Prop :=

proof body

Definition body.

  20  ∃ (error : ℝ), abs (G - 6.67430e-11) < error ∧ error < 1e-15
  21
  22/-- **THEOREM: High-Precision G Identity**
  23    Newton's gravitational constant G matches the CODATA value within 22 ppm. -/

used by (1)

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

gravitational_constant_precision in IndisputableMonolith.Physics.GravitationalConstantPrecision decl_use

depends on (7)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
Identity in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use