theorem proved term proof

`f_RG_interval_nonempty`

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

formal statement (Lean)

  52theorem f_RG_interval_nonempty (f : Fermion) : f_RG_lower f ≤ f_RG_upper f := by

proof body

Term-mode proof.

  53  unfold f_RG_lower f_RG_upper
  54  nlinarith [f_RG_tolerance_nonneg]
  55
  56/-- Equivalent absolute-error enclosure form for certified transport values. -/

depends on (7)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
f_RG_lower in IndisputableMonolith.Physics.RGTransportCertificate decl_use
f_RG_tolerance_nonneg in IndisputableMonolith.Physics.RGTransportCertificate decl_use
f_RG_upper in IndisputableMonolith.Physics.RGTransportCertificate decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use