def
definition
H_GPrecision
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.GravitationalConstantPrecision on GitHub at line 19.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
16 STATUS: EMPIRICAL_HYPO
17 TEST_PROTOCOL: Evaluation of G = λ_rec² c³ / (π ħ) using derived RS constants.
18 FALSIFIER: Measurement of G deviating from the derived value by > 22 ppm. -/
19def H_GPrecision : Prop :=
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. -/
24theorem gravitational_constant_precision (h : H_GPrecision) :
25 ∃ (error : ℝ), abs (G - 6.67430e-11) < error ∧ error < 1e-15 := h
26
27end Gravity
28end Physics
29end IndisputableMonolith