PublicInvariant
plain-language theorem explainer
PublicInvariant structures any admissible watch score as a map from public ECDLP data to reals. Auditors of Recognition Science invariants in elliptic-curve settings cite it to enforce that all computations remain public. The declaration is a parameterless structure whose sole field is the universal quantification over primes p of PublicECDLPData p to real numbers.
Claim. A public invariant consists of a score function $score : ∀ {p : ℕ}, PublicECDLPData(p) → ℝ$, where PublicECDLPData(p) encodes the short Weierstrass curve, base point, target point, order, and cofactor.
background
The ECDLP Watch module supplies an explicit mathematical surface for elliptic-curve discrete-logarithm claims. It is not an attack module; its goal is to make the ordinary mathematical problem precise before testing any RS candidate invariant. PublicECDLPData collects the curve, base point, target point, order, and cofactor that an adversary can see.
proof idea
The declaration is a direct structure definition introducing the score field with no further computation or lemmas applied.
why it matters
PublicInvariant supplies the type for InvariantWatchRecord, which tags curve families as weak or not. It enforces the module's requirement that invariants depend only on public data, aligning with Recognition Science's separation of public and private information in cryptographic claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.