`VerifiedConstant`

definition

show as: view math explainer →

module: IndisputableMonolith.CPM.ConstantsAudit
domain: CPM
line: 34 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  31/-! ## Verified Constants -/
  32
  33/-- Structure recording a verified constant with its derivation. -/
  34structure VerifiedConstant where
  35  /-- Name of the constant -/
  36  name : String
  37  /-- Numerical value -/
  38  value : ℝ
  39  /-- Source of derivation -/
  40  source : String
  41  /-- Whether the value is exact (vs. approximate) -/
  42  exact : Bool
  43
  44/-- All verified CPM constants. -/
  45noncomputable def verifiedConstants : List VerifiedConstant := [
  46  { name := "K_net (cone)",
  47    value := 1,
  48    source := "Intrinsic cone projection",
  49    exact := true },
  50  { name := "K_net (eight-tick)",
  51    value := (9/7)^2,
  52    source := "ε=1/8 covering, refined analysis",
  53    exact := true },
  54  { name := "C_proj",
  55    value := 2,
  56    source := "Hermitian rank-one bound, J''(1)=1",
  57    exact := true },
  58  { name := "C_eng",
  59    value := 1,
  60    source := "Standard energy normalization",
  61    exact := true },
  62  { name := "C_disp",
  63    value := 1,
  64    source := "Dispersion bound",

papers checked against this theorem

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