IndisputableMonolith.Relativity.GRLimit.ParametersTest

   1import Mathlib
   2import IndisputableMonolith.Relativity.GRLimit.Parameters
   3
   4/-!
   5# Smoke Tests for GRLimitParameterFacts
   6
   7Verifies that the rigorous instance `grLimitParameterFacts_proven` is available
   8and that all bounds hold as expected.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Relativity
  13namespace GRLimit
  14
  15-- Smoke test: instance is available
  16example : GRLimitParameterFacts := inferInstance
  17
  18-- Smoke test: individual bounds hold
  19example : alpha_from_phi < 1 := by
  20  have := GRLimitParameterFacts.rs_params_small (self := inferInstance)
  21  exact this.1
  22
  23example : cLag_from_phi < 1 := by
  24  have := GRLimitParameterFacts.rs_params_small (self := inferInstance)
  25  exact this.2
  26
  27example : |alpha_from_phi * cLag_from_phi| < 0.02 := by
  28  exact GRLimitParameterFacts.coupling_product_small (self := inferInstance)
  29
  30example : |alpha_from_phi * cLag_from_phi| < 0.1 := by
  31  exact GRLimitParameterFacts.rs_params_perturbative (self := inferInstance)
  32
  33-- Smoke test: numeric bounds are as expected
  34example : alpha_from_phi < 1 / 2 := alpha_lt_half
  35example : cLag_from_phi < 1 / 10 := cLag_lt_one_tenth
  36
  37-- Smoke test: positivity
  38example : 0 < alpha_from_phi := rs_params_positive.1
  39example : 0 < cLag_from_phi := rs_params_positive.2
  40
  41#check grLimitParameterFacts_proven
  42#check alpha_from_phi
  43#check cLag_from_phi
  44
  45end GRLimit
  46end Relativity
  47end IndisputableMonolith
  48