`GRLimitParameterFacts`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.GRLimit.Parameters
domain: Relativity
line: 224 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.GRLimit.Parameters on GitHub at line 224.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 221  ⟨alpha_lt_one, cLag_lt_one⟩
 222
 223/-- Recognition spine parameters are small (for perturbation theory). -/
 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. -/
 230instance grLimitParameterFacts_proven : GRLimitParameterFacts where
 231  rs_params_small := rs_params_small_proven
 232  coupling_product_small := coupling_product_small_proven
 233  rs_params_perturbative := rs_params_perturbative_proven
 234
 235end GRLimit
 236end Relativity
 237end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.