{"id":"palomar/PALOMAR-2026-10-02-000014","url":"https://github.com/jfairfaxball-348/pascal-cofactors/tree/02a52e71a0a5ab1e77824490d0c47650d4a45691","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-02-000014-v1.json","repo":"https://github.com/jfairfaxball-348/pascal-cofactors","tags":["math.NT","msc:11B65","number-theory","p-adic","combinatorics","lean-formalization"],"score":0,"title":"Pascal Cofactors","trust":"high","domain":"math.NT","source":"palomar","authors":["John Fairfax-Ball"],"reviews":0,"subject":"math.NT","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-02","reactions":{},"formalized":true}