feat: make KoalaBear Rabin irreducibility certificates re-checkable by kernel replay

[kobizk]

Add explicit-cardinality Rabin wrappers so quinticPoly_irreducible/sexticPoly_irreducible state their certificates with the field size as a numeral, letting a from-empty kernel replay avoid reducing Fintype.card (ZMod p) (~p elements); definitionally equal, nothing weakened.

[github-actions]

🤖 PR Summary

The PR introduces wrapper lemmas that accept an explicit field cardinality parameter q (with a hypothesis Fintype.card F = q) and then subst hq to delegate to existing Rabin irreducibility tests. This makes the certificates in quinticPoly_irreducible and sexticPoly_irreducible definitionally equal to numerals, so a kernel replay from an empty environment can compute them without reducing Fintype.card (ZMod p) (~p elements). All existing behavior is preserved; no sorry or admit are added or removed.

Key Changes:

• RabinCertificate.lean: Added irreducible_of_rabin_prime_degree_of_card and irreducible_of_rabin_degree_six_of_card. Both take (q : ℕ) and (hq : Fintype.card F = q), then subst hq and call the original lemmas. This ensures the certificate’s cardinality argument is a numeral (e.g. fieldSize), not a Fintype.card expression.
• QuinticIrreducible.lean: Replaced two calls to irreducible_of_rabin_prime_degree (which required rw [hcard]) with a single call to the new irreducible_of_rabin_prime_degree_of_card, passing fieldSize and hcard. The rw steps are eliminated; subproofs dvd_X_pow_sub_X_of_runChain and isCoprime_X_pow_sub_X_of_runChain are unchanged.
• SexticIrreducible.lean: Replaced call to irreducible_of_rabin_degree_six with the new irreducible_of_rabin_degree_six_of_card, passing fieldSize and hcard. Three rw steps removed.

Objective: The change is purely about making the proof terms amenable to kernel replay for verification without requiring the kernel to compute Fintype.card (ZMod p) for a large prime (~p). The mathematical content is unchanged.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	41
❌ Lines Removed	12

---

Lean Declarations

✏️ Added: 2 declaration(s)

CompPoly/Data/Polynomial/RabinCertificate.lean (2)

• theorem irreducible_of_rabin_degree_six_of_card {F : Type*} [Field F] [Fintype F]
• theorem irreducible_of_rabin_prime_degree_of_card {F : Type*} [Field F] [Fintype F]

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Minor style violation detected; otherwise compliant with guidelines.

---

📄 **Per-File Summaries**

• CompPoly/Data/Polynomial/RabinCertificate.lean: Added two new theorems, irreducible_of_rabin_prime_degree_of_card and irreducible_of_rabin_degree_six_of_card, which are variants of the existing irreducible_of_rabin_degree_six and irreducible_of_rabin_prime_degree that take an explicit cardinality parameter q with a hypothesis Fintype.card F = q and then subst hq to delegate to the original theorems. The docstrings explain that this
• CompPoly/Fields/KoalaBear/Ext5/QuinticIrreducible.lean: The proof of quinticPoly_irreducible was refactored to replace the two-step irreducible_of_rabin_prime_degree calls (which required rewriting by hcard : Fintype.card Field = fieldSize) with a single call to the new lemma irreducible_of_rabin_prime_degree_of_card, which takes fieldSize and hcard as explicit parameters. The two underlying subproofs (dvd_X_pow_sub_X_of_runChain and isCoprime_X_pow_sub_X_of_runChain) remain unchanged; the refactor eliminates the rw [hcard] steps, streamlining the proof.
• CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean: The proof of sexticPoly_irreducible was updated to call irreducible_of_rabin_degree_six_of_card (instead of irreducible_of_rabin_degree_six), passing fieldSize and hcard as explicit arguments. The three rw [hcard] steps were removed from the body of the proof, as the new lemma presumably handles the cardinality condition internally.

---

Last updated: 2026-08-17 01:09 UTC.

[alexanderlhicks]

Thanks!