class definition def or abbrev

`GRLimitParameterFacts`

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

formal statement (Lean)

 224class GRLimitParameterFacts : Prop where
 225  rs_params_small : alpha_from_phi < 1 ∧ cLag_from_phi < 1
 226  coupling_product_small : |alpha_from_phi * cLag_from_phi| < 0.02
 227  rs_params_perturbative : (|alpha_from_phi * cLag_from_phi|) < 0.1
 228
 229/-- Rigorous instance providing GRLimitParameterFacts with ACTUAL PROOFS. -/

used by (2)

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

grLimitParameterFacts_proven in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
coneEntropyStub in IndisputableMonolith.Relativity.NewFixtures decl_use

depends on (2)

Lean names referenced from this declaration's body.

alpha_from_phi in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
cLag_from_phi in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use