pith. machine review for the scientific record. sign in
def definition def or abbrev

verifiedConstants

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  45noncomputable def verifiedConstants : List VerifiedConstant := [

proof body

Definition body.

  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",
  65    exact := true },
  66  { name := "c_min (cone)",
  67    value := 1/2,
  68    source := "1/(K_net·C_proj·C_eng) = 1/(1·2·1)",
  69    exact := true },
  70  { name := "c_min (eight-tick)",
  71    value := 49/162,
  72    source := "1/(K_net·C_proj·C_eng) = 1/((81/49)·2·1)",
  73    exact := true },
  74  { name := "α (ILG exponent)",
  75    value := alphaLock,
  76    source := "(1 - 1/φ)/2 from self-similarity",
  77    exact := true },
  78  { name := "φ (golden ratio)",
  79    value := phi,
  80    source := "Fixed point of x² = x + 1",
  81    exact := true }
  82]
  83
  84/-! ## Consistency Verification -/
  85
  86/-- Verify that c_min is correctly computed from other constants. -/

used by (2)

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

depends on (26)

Lean names referenced from this declaration's body.