Pascal Cofactors
A Lean 4 formalisation of p-adic valuation laws for alternating cofactors C_d(p^a) = (p^(ad)+1)/(p^a+1) with odd d. It proves finite-window coefficient scaling and an exact pre-extremal restricted-binomial-gcd formula, identifies the sparse endpoint, proves the least extremal row T_p(C_d(p^a)) = p^(ad)+1 for odd d >= 5, and gives the full cubic classification for p^(2a)-p^a+1. The Palomar Challenge records coefficient scaling, the exact bounded gcd formula, the odd-degree least-row theorem, and the cubic classification.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-02-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-02-000014/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-10-02-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'