Won Chul Yang (independent researcher, wcy0969@gmail.com)
Concept DOI: 10.5281/zenodo.21778049 (this release: 10.5281/zenodo.21778050)
A computational anatomy of the counterexamples to the Jacobian Conjecture announced in July 2026, built and verified between 2026-07-20 and 2026-08-04:
- Independent grounding of all three families. The F_m family on ℂ³ (generic fibers 2m−1), the marked-root K_n family on ℂⁿ (generic fibers n(n−2)), and the weighted-lift family on ℂ³ (every generic fiber degree ≥ 3): determinants, Hensel data, fiber counts and collision points verified symbolically (F_m: m = 2..5; K_n: n = 3..6; weighted-lift: seeds d = 2..5, i.e. fibers 3, 4, 5, 6).
- One seed, two axes. The original ℂ³ map is the common member of both families: an explicit automorphism pair identifies it with F₂ (A = (3a, b, −3c), B = (x, y, z/3), A∘F_orig∘B = F₂, exact symbolic identity), and it equals K₃ up to an invertible target change.
- A counting theorem for the v-chart neighborhood. In the design tuple (v = y+1/x, 2a = h(v), K/x = h′(v)): d = 3 is the unique rank-deficient consistent case; for every d ≥ 4 the forcing window is unimodular — the d ≥ 4 obstructions are one invariant kill, and four adjacent designs die at the same counting filter.
- A measured monodromy dichotomy. F₃'s generic-target monodromy is A₅ (order 60, transitive, primitive — 5-sheet Newton-continuation battery on two locked generic lines, 0 ambiguous trackings, controls clean); K₄'s is transitive but imprimitive (block hypothesis {tᵢ, ±a} confirmed; observed group order 192 | 384 = |ℤ₂ wr S₄|); and the weighted-lift member G (4 sheets, even fiber, ℂ³) is S₄ — primitive again, consistent with the independent S_n structure theory of that family (MikhailSzh/weighted-lift-galois, 2026-07-21). Primitive-monodromy étale compression therefore exists (F₃, G); primitivity is not determined by the chart; imprimitive compression is free under composition. v1.0.2 adds F₄ = S₇ (exact — order 5040, odd generators), refuting the A_{2m−1} conjecture for the F_m family: monodromy parity is m-dependent. v1.0.3 settles the parity mechanism via the discriminant-square law: Δ₃ = 4050000·W² with an explicit (now kernel-checked) witness ⇒ F₃'s geometric monodromy ⊆ A₅ at the family level, while m = 2, 4, 5 are strictly non-square — and m = 3's squareness is a UNIT phenomenon (arithmetic accident), not polynomial structure. Realized groups: S₃, S₄, A₅, S₇, block-wreath; pre-registered prediction: F₅ on the S₉ side.
- The pin-system wall theorem. In the marked-root §7 search grammar on ℂ³ (compatible selection family, monomial h = aⁿ, first congruence order): the D = 3 "sequential pin-then-fail" and D ≥ 4 "simultaneous contradictory pins" are ONE D-parametric linear pin-system; kill ⇔ rank([M|b]) = 2; the b-column is D-independent (Collapse Lemma, proven structurally for all D ≥ 3), so the wall is degree-blind, and n = 1 — precisely the K-family instance — is the sole survivor (homogeneous consistent case).
- Parity landscape. Every odd fiber cardinality ≥ 3 is realized in ℂ³ (F_m); even cardinalities in ℂⁿ, n ≥ 4 (K_n); and — as we verified during the pre-release citation sweep — even cardinalities in ℂ³ as well, via the independent weighted-lift family (Gallagher & GPT-5.6-sol, jacobianfun.org; we lead-verified the degree-4 member G: det JG ≡ −6, generic fiber exactly 4). Our wall theorems delimit WHERE even fibers cannot come from: the entire marked-root §7 grammar is parity-blind walled (n = 1 sole survivor, all D) — the weighted-lift family lives in a third, inequivalent chart, which is precisely the chart-scoping moral this release documents (three families, three charts, one seed).
lean_artifact/ contains Lean 4 (v4.31.0, Mathlib) proofs of the release's core
identities — the operator identities 𝓛_m R_m = (−1)^m m·C(2m−1,m) for
m = 2, 3, 4, 5 (JacAnat_T1m2..m5), the counting-theorem window determinant
(JacAnat_T2/T2b), and the D = 3, n = 2 pin-system wall instance (JacAnat_T3) —
each verifying with
#print axioms ⊆ {propext, Classical.choice, Quot.sound} (no sorry, no
native_decide). As of v1.0.1 the artifact is SELF-CONTAINED: lean_artifact/
carries its own lakefile.toml (Mathlib pinned to v4.31.0) and
lean-toolchain — clone, cd lean_artifact, lake exe cache get, then
lake env lean <file> on any of the 11 files. v1.0.1 adds the general-D
Collapse Lemma (JacAnat_Collapse.lean, the wall theorem's degree-blindness
core) as the 8th kernel-checked theorem. v1.0.3 adds three more: the
W-identity Delta_3 = 4050000W^2 (the parity-law square certificate,
JacAnat_W.lean), the m=2 closed discriminant form disc = -4phi
(JacAnat_DiscPhi.lean), and the disc(A_m) numeric facts (JacAnat_ADisc.lean)
— 11 theorems total. Don't trust us: run the kernel yourself.
repro/ contains the sympy scripts behind every claim (see REPRO_INDEX.md for
the claim → script map). All symbolic claims re-run in minutes on stock
sympy 1.14; monodromy batteries are pre-registered (locked loop specs and
tolerances included) and re-run in ~10 minutes.
These results were produced with an autonomous research loop (KoreoLoop/HELM) driving Claude Fable 5, Claude Opus 5 and Claude Sonnet 5, operated and steered by the author. Every registered claim passed an independent in-loop verifier plus a separate lead re-verification; several intermediate claims were REJECTED by that gate and corrected — the registry records both. The right response to skepticism about machine-generated mathematics is the artifact itself: check the Lean kernel, re-run the scripts.
- The original ℂ³ counterexample: announced by L. Alpöge, crediting Claude Fable and Akhil (2026-07-20).
- The F_m infinite family: Cal Aldred (with Claude Fable 5 and GPT-5.6 Sol), X, 2026-07-20. The marked-root K_n family with its dimension-independent proof: Harish (@hari65535) with GPT-5.6 Sol/Codex, X, 2026-07-20. The weighted-lift family: Alexis Gallagher with GPT-5.6-sol (jacobianfun.org, DOI 10.5281/zenodo.21479195). Further constructions: Manjaramkar, Zyskind, Holes, and others (see the note's references). This release independently verifies the three families and does not claim priority on any; our contributions are the identifications, the counting/wall theorems, the monodromy measurements, and the parity landscape.
Issues are open. The fastest way to refute any claim here: name the registry entry, run its script, exhibit the failing input. Counterexamples welcome.
Documents CC BY 4.0 · Lean artifact Apache-2.0 (Mathlib-compatible).