def
definition
isKnownWeakFamily
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cryptography.ECDLPWatch on GitHub at line 133.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
130 score : ∀ {p : ℕ}, PublicECDLPData p → ℝ
131
132/-- Known weak-curve classes must be separated from any standard-curve claim. -/
133def isKnownWeakFamily : CurveFamily → Prop
134 | CurveFamily.anomalous => True
135 | CurveFamily.supersingular => True
136 | CurveFamily.smallEmbeddingDegree => True
137 | _ => False
138
139/-- Watch predicate: a candidate invariant is being tested only on public data
140and against an explicitly tagged curve family. This carries no security claim. -/
141structure InvariantWatchRecord (I : PublicInvariant) where
142 family : CurveFamily
143 weak_family_tagged : isKnownWeakFamily family ∨ ¬ isKnownWeakFamily family
144
145end ECDLPWatch
146end Cryptography
147end IndisputableMonolith