InvariantWatchRecord
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assert security for any invariant.
- Does not implement an ECDLP solver or attack.
- Does not reference Recognition Science constants, phi-ladder, or forcing chain.
- Does not constrain the score function beyond the public-data requirement.
formal statement (Lean)
141structure InvariantWatchRecord (I : PublicInvariant) where
142 family : CurveFamily
143 weak_family_tagged : isKnownWeakFamily family ∨ ¬ isKnownWeakFamily family
144
145end ECDLPWatch
146end Cryptography
147end IndisputableMonolith