All-ones polynomials over GF(2) under the substitution X ↦ X² + X + 1 (OEIS A071642, TheoremDB P12771)
Formalizes in Lean 4 the resolution of a 2019 OEIS conjecture of L. H. Gallardo (comment on A071642; TheoremDB P12771): for every n ≥ 2 the all-ones polynomial 1 + X + ⋯ + Xⁿ is irreducible over GF(2) if and only if 1 + P + ⋯ + Pⁿ is irreducible over GF(2), where P = X² + X + 1. The compared statements are the per-n equivalence, the literal set-level form of the OEIS comment (the terms ≥ 2 coincide), and the failure of the excluded case n = 1. The proof is elementary: a factorization of the all-ones polynomial composes to one of the substituted polynomial; conversely irreducibility forces n…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-11-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-11-000004/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-09-11-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'