def
definition
verifiedConstants
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 45.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
alphaLock -
tick -
tick -
VerifiedConstant -
of -
one -
is -
of -
rank -
from -
one -
is -
of -
is -
C_proj -
K_net -
of -
is -
that -
point -
one -
value -
one -
self -
rank
used by
formal source
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",
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,