{"id":"palomar/PALOMAR-2026-08-29-000002","url":"https://github.com/dcposch/jc2-lean/tree/ba44127093e65cbd862604a16e3fe79fb63e93cf/gcd3-69-cube","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000002-v1.json","repo":"https://github.com/dcposch/jc2-lean","tags":["math.AG","math.AC","msc:14R15","msc:13P10","algebraic-geometry","lean-formalization","polynomials","commutative-algebra"],"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 proof of the source-facing polynomial-cube exclusion at actual partial degrees (6,9). From literal bivariate polynomials of outer degrees six and nine, leading coefficients s^6 and s^9 for a common polynomial s, and nonzero constant Keller bracket, the formalization proves that no such source exists, including when s is constant. It constructs the finite-pole or infinity expansion, exhausts every timing of the eight Faber loads through rho2, and excludes the remaining elliptic, cusp, zero-invariant, and constant-core terminal fibres. It does not claim the reduction from an…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true,"formalizes":[{"title":"GCD3 (6,9) cube-core mismatch gate","identifier":"","relationship":"formalizes"},{"title":"GCD3 (6,9) cube-core rational trajectory gate","identifier":"","relationship":"formalizes"}]}