doc(RabinCertificate): clarify the cold-replay mechanism

[kobizk]

Documentation-only

• Explains why fresh replay can normalize differently: it checks a serialized and reconstructed expression graph.
• Clarifies that rw [hcard] introduced concrete caller-side Eq.mpr transports.
• Records the observed path: npowRec unfolded X ^ (fieldSize ^ 6) one exponent step at a time until the deep-recursion guard fired.
• Evidence: https://github.com/zksecurity/comppoly-rabin-replay-repro

[github-actions]

🤖 PR Summary

Documentation

• Single file changed: CompPoly/Data/Polynomial/RabinCertificate.lean
• What is documented: The functions irreducible_of_rabin_degree_six (and contextually irreducible_of_rabin_prime_degree).
• Key clarification: The documentation now explains the performance motivation for accepting an explicit hcard : Fintype.card F = q parameter. It describes that directly using the Rabin certificate to discharge conditions avoids Eq.mpr transports that were introduced by rw [hcard]. In a cold replay, checking such a transport's certificate argument caused Polynomial.pow to unfold into npowRec and Nat.rec, stepping through X ^ (fieldSize ^ 6) one exponent at a time until Lean's deep-recursion guard fired. The new comment notes that supplying hcard as ZMod.card _ sidesteps this issue.
• No code, theorems, definitions, or proofs changed — only inline documentation revised.
• No sorry or admit placeholders introduced.
• Supporting evidence: The PR body references a reproduction repository at https://github.com/zksecurity/comppoly-rabin-replay-repro to illustrate the observed cold-replay slowdown.
• Relevance: This documentation is important for future developers to understand an optimization that prevents performance degradation during cold replays, without altering the mathematical specification.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	6
❌ Lines Removed	2

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings. The diff is a docstring-only update that adheres to the project's documentation standards and style guide; no violations were identified.

---

📄 **Per-File Summaries**

• CompPoly/Data/Polynomial/RabinCertificate.lean: The commit updates the documentation comment for irreducible_of_rabin_degree_six (and the earlier irreducible_of_rabin_prime_degree, based on the comment's context) to explain the performance motivation for accepting an explicit hcard : Fintype.card F = q parameter. It describes that discharging Rabin conditions via direct certificate application avoids the Eq.mpr transports introduced by rw [hcard], and notes that in a cold replay, checking such a transport's certificate argument caused Polynomial.pow to unfold into npowRec and Nat.rec, stepping through X ^ (fieldSize ^ 6) one exponent at a time until Lean's deep-recursion guard fired. The comment states that supplying hcard as ZMod.card _ sidesteps this issue. No code, theorems, definitions, or proofs are changed; only the inline documentation is revised.

---

Last updated: 2026-09-01 18:50 UTC.

[dhsorens]

thanks for the contribution @kobizk, and welcome! merging