isKnownWeakFamily
plain-language theorem explainer
The definition classifies elliptic curve families for the ECDLP watch harness by returning true exactly on anomalous, supersingular, and small-embedding-degree cases. Cryptographers auditing RS candidate invariants against public instances cite it to enforce explicit weak-family tagging before any invariant test. It is realized as a direct pattern match on the CurveFamily inductive type with no additional computation.
Claim. Let $F$ be a curve family. The predicate holds if and only if $F$ is anomalous, supersingular, or has small embedding degree; it fails on all other families.
background
The ECDLP Watch Surface module supplies a minimal mathematical surface for auditing discrete-logarithm claims on elliptic curves. It fixes a finite carrier in ZMod p, short Weierstrass equations, the chord-tangent group law, scalar multiplication, and an explicit ECDLP solution predicate, all without security assertions. The CurveFamily inductive type supplies the six tags toy, anomalous, supersingular, smallEmbeddingDegree, ordinaryPrimeOrder, and standardLike. The present definition isolates the three known weak tags so that any downstream watch record can separate them from standard-curve claims.
proof idea
The definition is a direct pattern match on the CurveFamily constructors. It returns True on the anomalous, supersingular, and smallEmbeddingDegree cases and False on every remaining constructor.
why it matters
The definition is referenced inside InvariantWatchRecord to populate the weak_family_tagged field, which records that a candidate invariant is exercised only on public data against an explicitly tagged family. It therefore supplies the separation step required by the module's stated goal of making the ordinary ECDLP problem precise before any RS invariant is tested. No framework landmark from the T0-T8 chain is invoked; the contribution is strictly local to the cryptography auditing surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.