{"id":"palomar/PALOMAR-2026-08-25-000002","url":"https://github.com/dcposch/jc2-lean/tree/b80667d80987ca48cb98e1eb31e1324251b7928a/gcd3-69-noncube","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-25-000002-v2.json","repo":"https://github.com/dcposch/jc2-lean","tags":["math.AG","math.AC","msc:14R15","msc:13P10","lean4","algebraic-geometry","number-theory","formal-verification"],"score":0,"title":"dcposch/jc2-lean","trust":"high","domain":"math.AG","source":"palomar","authors":["Dan Clemens Posch"],"reviews":0,"subject":"math.AG","summary":"Lean 4 / Mathlib formalization of a two-sheet implication in the aligned nontrivial cubic-Kummer analysis at actual partial degrees (6,9). Every field-valued solution of the four lower-Pfaffian invariant equations is proved to lie on a common-power sheet with zero source bracket or on an elliptic sheet; converse inclusions and existence of the sheets are not compared. The formalization derives the elliptic equation and terminal one-form, excludes nonconstant reduced rational trajectories on its C != 0 fibre by a finite forbidden-value argument, factors the C=0 fibre, and verifies the shifted…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","reactions":{},"formalized":true,"formalizes":[{"title":"GCD3 (6,9) lower-Pfaffian successor gate","identifier":"","relationship":"formalizes"}]}