Open Research Index

dcposch/jc2-lean

Dan Clemens Posch

Palomar Registrypalomar/PALOMAR-2026-08-29-000002Aug 29, 2026math.AGscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-29-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000002/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-29-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'