`RealCertificate`

definition

show as: view math explainer →

module: IndisputableMonolith.Certificates.Standard
domain: Certificates
line: 39 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Certificates.Standard on GitHub at line 39.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  36/--
  37A helper for numeric certificates (Real numbers).
  38-/
  39structure RealCertificate where
  40  val : ℝ
  41  target_min : ℝ
  42  target_max : ℝ
  43  /-- Proof that the value lies within the empirical bounds. -/
  44  proof : target_min < val ∧ val < target_max
  45
  46instance : Repr RealCertificate where
  47  reprPrec c _ :=
  48    "PhysicalCertificate(val=" ++ repr c.val ++
  49    ", bounds=[" ++ repr c.target_min ++ ", " ++ repr c.target_max ++ "])"
  50
  51end IndisputableMonolith

papers checked against this theorem

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