def definition def or abbrev

`regime_covered`

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

formal statement (Lean)

  67def regime_covered : ConvergenceRegime → Bool
  68  | .linearized => true
  69  | .weakField => true
  70  | .strongField => false  -- needs CMS
  71  | .ultraStrong => false   -- open
  72

used by (2)

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

linearized_covers_observational in IndisputableMonolith.Gravity.NonlinearReggeProof decl_use
linearized_implies_weak in IndisputableMonolith.Gravity.NonlinearReggeProof decl_use

depends on (1)

Lean names referenced from this declaration's body.

ConvergenceRegime in IndisputableMonolith.Gravity.NonlinearReggeProof decl_use