fix(fields): make KoalaBear sextic proof replayable

[yudduy]

Fresh kernel replay of the imported KoalaBear.sexticPoly_irreducible proof can fail with a deep-recursion error on Lean 4.33.1, even though the original module builds. Pass the KoalaBear ZMod field and finite-type instances explicitly to the degree-six Rabin theorem so the certificate and theorem use the same instance path.

The polynomial, theorem statement, certificates, and trust assumptions are unchanged. The existing regression test imports the proof and checks its original body against its original type in a fresh kernel environment.

Validation:

• The regression failed on the original Lean 4.33.1 base and passed with the fix in the completed reproduction.
• The branch includes upstream main at 3468b38c8fd270f93f55a259220a8abc544e7437. All checks below pass on branch commit 9a0130b2de4909efd71760948cec9c50edb3031d with Lean 4.33.1:
  • lake build (169 seconds) and lake test (75 seconds).
  • lake exe axiomsweep --check: 9,870 declarations across 346 modules; no sorry or non-standard-axiom taint.
  • lake env lean tests/CompPolyTests/Fields/KoalaBear/SexticReplay.lean (77 seconds), directly executing the existing regression rather than relying only on its cached build.
  • Style, import, and documentation-integrity checks.

GitHub CI still requires maintainer approval to run this fork's workflows; those runs are not being reported as passed. Please approve the pending CI runs when reviewing this draft.

The competition integration temporarily pins the original fix commit 9d36af56cd57a468ade1cbbc8fae324983d79708 from this fork. That commit remains in this branch's history, so downstream users can continue with their tested dependency while this PR is reviewed.

[github-actions]

🤖 PR Summary

The overview should be standalone, with per-file specifics included, no critique, and organized under relevant headers. Since the PR is a fix for kernel replay, headers could be Kernel Replayability Fix and Testing. The core change is in SexticIrreducible.lean; the remaining files are test infrastructure. No sorry or admit are introduced.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	37
❌ Lines Removed	1

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff has several violations of the style guide and contains syntax errors that prevent compilation.

---

📄 **Per-File Summaries**

• CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean: In the proof of sexticPoly_irreducible, the call to irreducible_of_rabin_degree_six_of_card was changed to use an explicit @ application, passing (ZMod fieldSize), its field instance (ZMod.instField with instFactPrimeFieldSize), and its Fintype instance (ZMod.fintype). This ensures the ZMod instance path is made explicit during kernel replay, as stated in the added comment. No new lemmas, definitions, or sorrys were introduced; the rest of the proof remains identical.
• tests/CompPolyTests.lean: Added a public import of CompPolyTests.Fields.KoalaBear.SexticReplay, making the declarations from that module available in the test file and downstream. This likely provides definitions or theorems related to a sextic extension or replay construction for the KoalaBear field, expanding the scope of testable material.
• tests/CompPolyTests/Fields/KoalaBear/SexticReplay.lean: Added tests/CompPolyTests/Fields/KoalaBear/SexticReplay.lean, a new test file that rechecks the imported proof certificate KoalaBear.sexticPoly_irreducible from CompPoly.Fields.KoalaBear.Ext6.SexticIrreducible by replaying it through the kernel with a fresh addDeclCore call. The test looks up the theorem’s declaration in the kernel environment, constructs a new thmDecl named CompPolyTests.KoalaBear.replayed_sextic_irreducible, and verifies that the kernel accepts it without error, ensuring the original proof body is still valid after changes to the module.

---

Last updated: 2026-09-08 03:09 UTC.

[yudduy]

Continuing this compatibility work in zksecurity#1, targeting the zkSecurity fork for the Better Codes dependency. That PR includes Lean/Mathlib 4.33.1, the existing Rabin wrappers, this additional explicit-instance fix, and the fresh-kernel replay regression; its local build and test suite pass. Closing this proposal in favor of that review target. The existing fork branch and original pinned commit remain available for downstream users.