feat(Crypto/Systems): Elligator 1, Theorem 1 and Definition 2

[chris-anto-froeschl]

Formalizes results from Elligator: Elliptic-curve points indistinguishable from uniform random strings (Bernstein, Hamburg, Krasnova, Lange). Elligator is a way to encode points on certain elliptic curves as strings indistinguishable from uniform random data, used to make elliptic-curve-based protocols resistant to traffic analysis/censorship.

This PR is the foundational layer of a larger, ongoing effort. Beyond finishing Elligator 1 (Theorems 3 and 4, and a Curve1174 instantiation - see below), I intend to formalize the other members of the Elligator family over time, aiming for CSLib to eventually have a complete treatment of the Elligator line of constructions rather than just this one variant. The relevant papers are collected here. Flagging this now so the scope and naming decisions in this PR (e.g. Elligator1 as a namespace, not just Elligator) read as intended groundwork rather than arbitrary.

This PR contains only the foundational layer: Theorem 1 (the map from a field element to a curve point) and Definition 2 (the total map ϕ, extending Theorem 1 to all of F), kept "small" deliberately for review. The full Elligator 1 development - Theorem 3 (inversion), Theorem 4 (the bit-string encoding that gives Elligator its name), and an instantiation at Curve1174 (the paper's Section 4 curve, q = 2^251 - 9) - is complete in my working repository at chris-anto-froeschl/elligator and will follow as separate PRs once this base layer stabilizes. For orientation:

• README, including a translation table from the paper's numbering to the Lean declarations
• Blueprint, for the full dependency graph and statements

Scope of this PR

Main results:

• c, r, d: the curve parameters derived from s
• u, v, X, Y, x, y: the auxiliary and output coordinates, each with its own well-definedness/nonvanishing file
• χ: the quadratic character used throughout, built directly on Mathlib's quadraticChar (LegendreSymbol.lean)
• TwistedEdwardsCurve: a small, purpose-built structure for the complete Edwards curve equation and its affine points
• map_fulfills_curve_equation, variable_mul_ne_zero: Theorem 1's two conclusions
• ϕ: Definition 2's total map, packaged with a proof it lands on the curve (Map.lean)
• DecodingFunction: a thin wrapper exposing ϕ's result unwrapped from its subtype, for presentation

Generalization beyond the paper

The paper's standing hypothesis is q prime; several results here (including ϕ itself) hold for q a prime power congruent to 3 mod 4, so I've stated them with IsPrimePow q rather than Prime q throughout, and used Prime q only where the argument genuinely needs it (injectivity results relying on unique factorization of naturals below q).

Futhermore, all definitions are computable. ([DecidableEq F] is threaded explicitly rather than relying on Classical.choice). Whether this is fast at cryptographic field sizes is a separate question - see below.

Known lint-style failure: filenames

lake exe lint-style flags every file named after a lowercase paper variable (cProperties.lean, dProperties.lean, rProperties.lean, sProperties.lean, uProperties.lean, vProperties.lean, xProperties.lean, yProperties.lean) as not being UpperCamelCase. I've deliberately kept these as-is rather than mechanically renaming, for two reasons:

1. Each file's name mirrors the paper's own single-letter notation for that variable (c, d, r, s, u, v, x, y), which I think aids readability for anyone cross-referencing against the paper or the blueprint.
2. A straightforward rename isn't actually available for two of these without a collision: xProperties.lean → XProperties.lean and yProperties.lean → YProperties.lean would collide with the already-distinct XProperties.lean/YProperties.lean files in this same PR (the auxiliary coordinates X/Y, as opposed to the curve coordinates x/y) - these are only distinguishable by case on a case-sensitive filesystem today.

I'm open to either adding exceptions to scripts/nolints-style.txt, or renaming to content-distinguishing names (e.g. curveXProperties.lean) if that's preferred - happy to go whichever way maintainers want; just didn't want to make that call unilaterally before hearing a preference, and would rather open the PR with a known, explained lint failure than hold it up.

A general property merge distinguishing between parameters, helper variables and curve variables could also work. Although this would results in rather large files. This is all unavoidable due to the linearity of the paper.

χ and Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

χ is defined as quadraticChar F cast from ℤ into F itself (the form the paper uses), and every fact about it here is derived from Mathlib's quadraticChar API rather than reproven from scratch. I considered whether any of the resulting lemmas belong in Mathlib itself rather than here, but I think everything remaining is specific enough to this development (either tied to q ≡ 3 (mod 4), or small enough that a standalone Mathlib PR for it wouldn't be worth the overhead) - genuinely open to being told otherwise if a reviewer sees something worth splitting out.

Performance at cryptographic scale (help wanted)

Curve1174 (q = 2^251 - 9, not part of this PR) is where this becomes relevant: χ and anything built from it have a (q-1)/2- or (q+1)/4-sized exponent, and generic Monoid.npow is O(n) in the exponent rather than O(log n) - naively evaluating χ at that scale is not just slow but algorithmically infeasible. I got as far as building a Pratt/Lucas primality certificate (binary modular exponentiation, kernel-checked) to prove Curve1174's characteristic is actually prime, but I'm not an expert on the broader performance question of making the rest of the pipeline (χ, X, Y, …) execute efficiently at this scale, and would very much welcome input from anyone more experienced with this if/when the Curve1174 follow-up PR comes up.

Edwards curve infrastructure

I couldn't find existing (twisted) Edwards curve infrastructure in Mathlib/CSLib, so I wrote a minimal TwistedEdwardsCurve structure (equation, validity, affine points) sufficient for this development. I'd appreciate guidance on:

1. whether this belongs in this PR's location, or should move to a more general curves location;
2. whether it's worth generalizing now (e.g. beyond the "complete" case this development needs) or better left minimal until a second consumer appears.

File organization

The proof follows a linear dependency chain - each variable (c, r, u, v, X, Y, x, y) is defined in terms of the previous ones, with its well-definedness/nonvanishing lemmas following immediately after. I organized files to mirror this chain (one file per variable's properties) rather than by topic, since the paper's own argument is inherently linear and a topic-based split would just relocate the ordering into implicit cross-file dependencies instead of making it visible. Map.lean itself stays intentionally thin - a presentation layer over the *Properties.lean files, restating each of Theorem 1/Definition 2's actual claims as a short delegation, so a reader can follow the paper's structure without wading through the underlying algebra.

I'm proposing a new Crypto/Systems subfolder for this, since CSLib's cryptography directory doesn't yet have an obvious home for a specific published construction (cryptosystem) like this - open to a different location if one's preferred, and, per above, would ideally be a home the rest of the Elligator family can share as those land too.

AI usage

I used Aristotle at a few points to find tactic proofs for lemmas I was stuck on, mostly in the finite-field/character-theoretic arithmetic. I reviewed and understood every proof it produced before merging, and rewrote several for clarity/idiom afterward; none of the mathematical statements themselves were AI-generated, only some proof scripts.

Context

This project started as my first real Lean project and bachelor's thesis. I've continued refining it over the past several months since to bring it up to a quality I'd consider submission-ready. Happy to iterate on structure, naming, or proof style based on review feedback.

[chris-anto-froeschl]

Just as a follow-up to the file-naming issue:

I came up with two other naming conventions, each with its own pros and cons.

a) Organize files by content

Elligator1/
    ├── CurveParameterProperties.lean
    ├── AuxiliaryCoordinatesProperties.lean
    └── OutputCoordinatesProperties.lean

The main disadvantage here is that it becomes harder to find a specific fact about a specific variable. For example, if I am looking for c_ne_zero, I would have to know that c is a curve parameter and then look for the corresponding section inside CurveParameterProperties.lean.

The other issue is that the files could become very large. Looking ahead to Theorem 3, the property files for individual variables are already around ~1000 LOC, so grouping all properties by content would likely result in some rather unwieldy files. Smaller content splits might be findable though (although perhaps just artificially). Some content related proofs are just rather large at the end of the day.

b) Organize properties hierarchically

To address the issue of increasingly large files, we could instead structure them like this:

Elligator1/
├── Variables.lean
├── Map.lean
├── DecodingFunction.lean
├── EdwardsCurve.lean
└── Properties/
    ├── CurveParameters/
    │   ├── SProperties.lean
    │   ├── CProperties.lean
    │   ├── RProperties.lean
    │   └── DProperties.lean
    ├── AuxiliaryCoordinates/
    │   ├── UProperties.lean
    │   ├── VProperties.lean
    │   ├── XProperties.lean
    │   └── YProperties.lean
    └── OutputCoordinates/
        ├── XProperties.lean
        └── YProperties.lean

This would keep the individual files at a manageable size and provide some context about what kind of properties they contain. It also avoids the casing conflict we would otherwise get with names such as sProperties and SProperties.

However, I still dislike the fact that you have to remember whether the variable mentioned in a filename is actually the lowercase or uppercase version. The current naming scheme avoids this issue entirely, since we do not have to worry about the corresponding linter complaints.

I hope that gives more helpful context.