01 / Explore
Over k = AlgebraicClosure(F₂), the explicit polynomial map has det JF = 1 and is étale. Its function-field extension has degree 3 and is separable, while three exhibited distinct preimages collide.
F(x, y) = (P, Q)
P = x + x²y + x⁴ + x⁶y²
Q = y + x⁵ + x⁶y + x⁷y² + x⁸y³
Schematic 3D—not a literal embedding of F̄₂.
Schematic projection: curves and marker positions are illustrative. Only the displayed collision coordinates (0,1), (1,0), (1,1) and their common target (0,1) are exact claims.
View mode
Drag to rotate. Scroll to zoom. Keys 1–3 change mode; arrows rotate; +/− zoom; R resets. Touch uses a single-pointer drag; use the keyboard or wheel for zoom.
Étale mode: no local branch or ramification does not imply injectivity.
| Mode | Mathematical content |
|---|---|
| Generic fiber | The geometric generic fiber has cardinality exactly 3. |
| Explicit collision | Three exhibited distinct preimages, (0,1), (1,0), and (1,1), share the target (0,1). |
| Étale / no branch | The Jacobian determinant is 1, and AlgebraicGeometry.Etale affineMap is proved; no local branch or ramification does not imply injectivity. |
02 / Proof chain
The prose argument and the checked declarations stay side by side. Each step names the actual Lean object that carries it.
The displayed pair satisfies det JF = 1.
Generic.jacobian_detThe three exhibited distinct preimages (0,1), (1,0), and (1,1) share the target (0,1).
Final.collision_01_10Final.collision_01_11The actual target-field cubic gives function-field degree 3 and separability.
DegreeFromIrreducible.finrank_eq_threeDegreeFromIrreducible.extension_isSeparableAn explicit graph presentation proves the scheme-level predicate.
EtalePresentation.affineMap_etaleIts geometric generic fiber has cardinality exactly 3.
GeometricBridge.geometricFiberPoint_natCard_eq_threeNon-surjectivity and failure of isomorphism close the counterexample statement.
Final.fullCounterexampleMachine correspondence
The geometric bridge is distinct from the function-field calculation: it identifies fiber points with embeddings before counting them.
| Mathematical object | Lean theorem / definition |
|---|---|
| Base field k | Final.k = AlgebraicClosure (ZMod 2) |
| Actual target-field irreducibility | ActualIrreducibility.cubic_irreducible |
| Finite separable degree 3 | DegreeFromIrreducible.finSepDegree_eq_three |
| Fiber-point / embedding equivalence | GeometricBridge.geometricFiberPointFunctionFieldEmbeddingEquiv |
| Affine map is not an isomorphism | Final.affineMap_not_isIso |
03 / Verification & source
One authoritative historical local kernel receipt; one independent, digest-locked replay that corroborates it.
Lean 4.28.0 · Mathlib v4.28.0
source commit
ab26ce21e3b272eec73908d5ed2f8b10117f2e38
#check
DimensionTwoCounterexample.Final.fullCounterexample :
DimensionTwoCounterexample.Final.FullCounterexampleStatement
#print axioms
[propext, Classical.choice, Quot.sound]The original 2026-07-26 Apple arm64 run passed the geometric bridge, terminal theorem, root build, and KernelAudit.lean. The then-present .lake cache was later removed; this site does not claim a fresh local cache-free replay.
Independent evidence · corroborative
A separate read-only environment matched all Lean source digests and resolved dependency revisions, then reproduced the same four commands.
The Lean kernel receipt remains the mathematical authority. The replay is independent corroboration and does not replace that receipt.