structure
definition
RunningGR4Cert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.RunningG on GitHub at line 275.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
272 abs (G_ratio 20e-9 r_ref - 32) < 2
273
274/-- Running G Predictions Certificate (Round 4). -/
275structure RunningGR4Cert where
276 r_ref_explicit : ∀ r target : ℝ, 0 < r → 1 < target → 0 < r_ref_exact r target
277 r_ref_above_r : ∀ r target : ℝ, 0 < r → 1 + abs beta_running < target →
278 r < r_ref_exact r target
279 rung_near_360 : r_ref_phi_rung_approx - 360 = 4
280 hypothesis_exists : H_GravitationalRunning
281
282theorem running_g_r4_cert : RunningGR4Cert where
283 r_ref_explicit := r_ref_exact_pos
284 r_ref_above_r := r_ref_exact_gt_r
285 rung_near_360 := rung_near_sync_period
286 hypothesis_exists := H_GravitationalRunning_certificate
287
288end RunningG
289end Gravity
290end IndisputableMonolith