dcposch/jc2-lean
Lean 4 / Mathlib formalization of the vertex-gap obstruction at (k,d2) = (2,2) (label thm:22, Theorem 3.4 in the current compilation) from the campaign paper "A Vertex-Gap Obstruction for Low-Degree Strip Pairs in the Plane Jacobian Conjecture": for polynomials P, Q in K[x,y] over a field K of characteristic not in {2,3,5}, supported in the normalized type-(2,2) Newton strips along (1,2) with [P,Q] = x^2, the block coefficients satisfy a3 = 0 and a2^2*a6 = 0 - so the generic chart a2*a6 != 0 of the strip family is empty (VertexGap22, plus the side-symmetric companion VertexGap22_swapped in…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-20-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-20-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-20-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'