InvariantWatchRecord
plain-language theorem explainer
InvariantWatchRecord packages a PublicInvariant with a CurveFamily tag to record that any candidate score is evaluated only on public ECDLP data against an explicitly classified curve. Auditors of Recognition Science invariants would cite the structure when initializing an ECDLP watch harness. It is introduced as a direct structure definition containing two fields and no proof obligations.
Claim. For a public invariant $I$, an invariant watch record consists of a curve family $F$ together with the proposition that $F$ is known to be weak or is not known to be weak.
background
The module supplies an explicit mathematical surface for auditing elliptic-curve discrete-logarithm claims before any Recognition Science invariant is applied. PublicInvariant requires every score to be a function from public ECDLP data to reals. CurveFamily is the inductive enumeration of toy, anomalous, supersingular, small-embedding-degree, ordinary-prime-order, and standard-like classes; isKnownWeakFamily returns true precisely on the first three.
proof idea
The declaration is a direct structure definition. No lemmas are invoked and no tactics are executed; the two fields are simply typed.
why it matters
The structure supplies the basic record type for the ECDLP watch surface. It enforces separation of known-weak families from standard-curve claims and carries no security assertion, as stated in the module documentation. It therefore precedes any later application of Recognition Science invariants to ECDLP instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.