CurveFamily
plain-language theorem explainer
CurveFamily supplies an enumeration of six elliptic-curve classes that tags instances inside an ECDLP auditing harness. Researchers checking Recognition Science invariants on discrete-log problems cite the classification to isolate the three known-weak families from ordinary ones. The declaration is a plain inductive type whose constructors are consumed by case analysis in the downstream predicate isKnownWeakFamily.
Claim. An inductive type whose six constructors label the families toy curves, anomalous curves, supersingular curves, curves with small embedding degree, ordinary prime-order curves, and standard-like curves.
background
The ECDLP Watch module supplies a minimal explicit surface for auditing discrete-logarithm claims on elliptic curves. It fixes a finite carrier in ZMod p, a short Weierstrass equation, the chord-tangent group law on points including infinity, and scalar multiplication, all before any Recognition Science invariant is applied. The upstream theorem from PrimitiveDistinction states that the framework rests on seven independent axioms that reduce to four substantive structural conditions plus three definitional facts.
proof idea
Inductive definition that introduces the six constructors with no further equations or computational content. Downstream code such as isKnownWeakFamily performs exhaustive case analysis on the constructors to return True precisely for the three weak families.
why it matters
CurveFamily provides the explicit tagging required by InvariantWatchRecord and isKnownWeakFamily so that any later Recognition Science invariant is forced to declare whether it is being tested on a known-weak family. It directly implements the module's stated purpose of keeping invariants honest by restricting them to public data only. No open question or scaffolding is attached to the definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.