2. Conformance: Buzzard’s spec vs. this formalization🔗

Kevin Buzzard’s challenge (Jacobian_challenge.lean) lists 24 definitions, instances and theorems as sorry stubs — the API a solution must provide, with exact names and types. This repository supplies real declarations for every one.

ChallengeConformance.lean is the machine-check: each item below is an example that restates Buzzard’s verbatim signature and discharges it with our declaration. The file compiles with no errors, no sorry, and axiom-clean — so the table is not a claim, it is checked by the Lean kernel (and, independently, by the real leanprover/comparator: see verify.sh).

To validate an item yourself: read Buzzard’s required type (left of :=), confirm it matches the spec, then follow the submission surface link into Jacobians.lean and on into the proof. Every row links the spec, the check, and our code.

Reproduce the check: lake env lean ChallengeConformance.lean (expects no output).

1. 2.1. Definitions
2. 2.2. Instances on the Jacobian
3. 2.3. Theorems & lemmas