doc(RabinCertificate): correct the _of_card rationale and signature

[alexanderlhicks]

Follow-up to #306.

Motivation

The _of_card wrappers #306 added are correct and the KoalaBear proofs do read better for them, but two things were left inconsistent.

The stated rationale does not hold. The docstrings justified the numeral form by claiming the Fintype.card F form forces a from-empty kernel replay to reduce Fintype.card F — "for a ZMod p field, an enumeration of ~p elements". It does not. rw [hcard] elaborates to Eq.mpr (id (congrArg motive hcard)) cert, whose kernel check only beta-reduces the motive, so Fintype.card F never reaches whnf position. Measured kernel type-checking of both proofs, three runs each:

run	quintic rw [hcard]	quintic _of_card	sextic rw [hcard]	sextic _of_card
1	6.87 ms	3.42 ms	5.19 ms	2.71 ms
2	9.82 ms	9.42 ms	5.14 ms	4.58 ms
3	4.61 ms	5.30 ms	9.55 ms	7.51 ms

Run-to-run variance within a single form exceeds the difference between the forms. And since Lean kernel-checks every theorem at addDecl during an ordinary lake build, a from-empty replay runs that same check — had the previous form forced a 2^31-element enumeration, main could not have built.

The real benefit is the one irreducible_X_pow_four_sub_C_of_card already documents on the binomial side: the generated certificates are already stated in terms of fieldSize (chainExp 1 steps = fieldSize ^ d), so each Rabin condition applies directly instead of needing a rw [hcard] cast. The docstrings now say that.

The wiki still pointed at the old wrappers. Step 3 of "Adding a new non-binomial extension" in docs/wiki/field-extensions.md — the recipe every new extension follows — named irreducible_of_rabin_prime_degree / irreducible_of_rabin_degree_six, while the two canonical callers had moved to the _of_card forms. So the repo was giving two conflicting instructions about which wrapper to use. Per the maintenance contract in docs/wiki/README.md.

Changes

• RabinCertificate.lean — rewrite both _of_card docstrings with the accurate rationale; drop "the two forms are definitionally equal" (the plain form is the q := Fintype.card F instance of the numeral one, not a defeq variant); add an ### Explicit-cardinality forms section header, since the new declarations sat under a header whose prose described only the two Fintype.card-shaped wrappers; mention the forms in the module docstring.
• API — make q implicit ({d q : ℕ}) and rename hq to hcard, matching irreducible_X_pow_four_sub_C_of_card. q is uniquely determined by hcard, which precedes h_trace/h_cop, so inference never needs higher-order matching against X ^ (?q ^ d). Both call sites shorten; the quintic one returns to a single line.
• QuinticIrreducible.lean — the module docstring still named the pre-feat: make KoalaBear Rabin irreducibility certificates re-checkable by kernel replay #306 lemma.
• docs/wiki/field-extensions.md — name the _of_card forms in the API table, the wrapper table, and the recipe; note that a composite d with no _of_card form still uses irreducible_of_rabin_two_prime_factors with a rw [hcard] cast.
• tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean — pin the round trip. prime_degree_recovered / degree_six_recovered instantiate each _of_card form at q := Fintype.card F with rfl and must yield the plain statement verbatim, so "nothing is weakened" is CI-enforced rather than asserted, and a future edit cannot silently add a hypothesis or shift an exponent. The opposite direction is the wrapper's own proof body.

No statement changes: quinticPoly_irreducible, sexticPoly_irreducible and both Fact instances are untouched.

Validation

lake build (2631 jobs), lake test, ./scripts/lint-style.sh, python3 ./scripts/check-docs-integrity.py — all clean. Axiom hygiene of both irreducibility theorems re-checked: [propext, Classical.choice, Quot.sound].

Note for maintainers unrelated to this diff: scripts/lint-style.sh globs only CompPoly/**/*.lean and *.lean, so tests/ is never linted. I ran lint-style.py on the changed test file separately (clean), but the gap is worth closing.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

This PR corrects the documentation and API signature of the _of_card wrapper theorems in RabinCertificate.lean, whose original docstring falsely claimed a kernel-replay performance advantage. It also updates the wiki to refer to the _of_card forms (which were the canonical callers after #306) and adds a round-trip test to pin the equivalence between the two forms.

No sorry or admit are introduced; all existing theorems remain unchanged.

Documentation

• RabinCertificate.lean — Rewrote the docstrings of irreducible_of_rabin_prime_degree_of_card and irreducible_of_rabin_degree_six_of_card to give an accurate rationale: the benefit is that the generated certificates are already stated in terms of fieldSize, so each Rabin condition applies directly without a rw [hcard] cast. Removed the incorrect claim that the numeral form forces a cheaper kernel reduction. Added a section header ### Explicit-cardinality forms and updated the module docstring to mention these variants.
• docs/wiki/field-extensions.md — Updated the API table, wrapper table, and step‑by‑step recipe to point new extensions at the _of_card forms instead of the now‑noncanonical irreducible_of_rabin_prime_degree / irreducible_of_rabin_degree_six. Notes that composite‑degree cases without an _of_card form still use irreducible_of_rabin_two_prime_factors with a rw [hcard] cast.
• QuinticIrreducible.lean — Module docstring corrected to reference irreducible_of_rabin_prime_degree_of_card.

Refactoring

• RabinCertificate.lean — Changed the q parameter of both _of_card theorems from explicit (q : ℕ) to implicit {q : ℕ}, and renamed hq to hcard (matching irreducible_X_pow_four_sub_C_of_card). This makes call sites shorter: q is uniquely determined by hcard, which precedes h_trace/h_cop.
• QuinticIrreducible.lean and SexticIrreducible.lean — Updated calls to the _of_card wrappers to omit the now‑implicit fieldSize argument. The proof bodies otherwise unchanged.

Testing

• tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean — Added OfCardRoundTrip namespace containing prime_degree_recovered and degree_six_recovered. Each instantiates the _of_card form at q := Fintype.card F using rfl and recovers the plain theorem statement verbatim. This machine‑checks that the two forms are equally strong, preventing any future weakening of the _of_card hypotheses.

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	85
❌ Lines Removed	32

---

Lean Declarations

✏️ Added: 2 declaration(s)

tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean (2)

• theorem degree_six_recovered {F : Type*} [Field F] [Fintype F] {f : F[X]}
• theorem prime_degree_recovered {F : Type*} [Field F] [Fintype F] {f : F[X]} {d : ℕ}

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff conforms to the project's PR guidelines and style conventions. All naming, naming logic, module layout, variable conventions, and deprecation policy are respected. The description and title are formatted correctly, the _of_card refactor follows the existing code patterns, and documentation and tests are updated accordingly. No violations found.

---

📄 **Per-File Summaries**

• CompPoly/Data/Polynomial/RabinCertificate.lean: The file RabinCertificate.lean was updated in two main ways. First, the module‑level docstring now explicitly mentions the _of_card variant theorems and explains that they accept the field size as a numeral q with a Fintype.card F = q equality — the shape concrete extensions use. Second, the two existing _of_card theorems (irreducible_of_rabin_prime_degree_of_card and irreducible_of_rabin_degree_six_of_card) were refactored: the q parameter was changed from an explicit argument (in parentheses) to an implicit binder (in curly braces), and the cardinality hypothesis was renamed from hq to hcard. Their docstrings were rewritten to emphasise that their content is identical to the corresponding base theorems, that the substitution subst hcard recovers the base form, and that a regression test pins the instantiation at q := Fintype.card F. No sorry or admit appears in the diff.
• CompPoly/Fields/KoalaBear/Ext5/QuinticIrreducible.lean: The PR updates the call to irreducible_of_rabin_prime_degree_of_card by removing the explicit fieldSize parameter (now inferred from hcard), and updates the module docstring to reference the corrected theorem name irreducible_of_rabin_prime_degree_of_card (formerly irreducible_of_rabin_prime_degree). The proof body of quinticPoly_irreducible is adjusted accordingly, while the antecedent lemmas quintic_bezout_check, quintic_trace_chain, quintic_trace_exp, and quinticPoly_natDegree remain unchanged.
• CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean: The proof of sexticPoly_irreducible was modified to remove the explicit fieldSize argument from the call to irreducible_of_rabin_degree_six_of_card, since its type is now inferred automatically from hcard.
• docs/wiki/field-extensions.md: The documentation file field-extensions.md was updated to add descriptions of new _of_card theorem forms for Rabin irreducibility certificates, specifically irreducible_of_rabin_prime_degree_of_card and irreducible_of_rabin_degree_six_of_card. These accept the field size as a numeral q with a hcard : Fintype.card F = q hypothesis, allowing concrete extensions to apply the conditions directly using the certificate's fieldSize without per-condition rw [hcard] casts. The relevant table in the Rabin certificates documentation and the step-by-step irreducibility wrapper guide in the walkthrough were both updated to reflect these forms, noting the inter-derivability with the plain forms (via rfl instantiation) and that composite-degree cases without _of_card forms still use irreducible_of_rabin_two_prime_factors with explicit rw [hcard] casts. Additionally, the diff mentions that tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean pins the round-trip equivalence between the two forms.
• tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean: Adds a new OfCardRoundTrip namespace containing two theorems, prime_degree_recovered and degree_six_recovered, that each recover the plain Rabin irreducibility theorem from its _of_card variant by instantiating q := Fintype.card F via rfl. These serve as a machine-checked verification that the _of_card forms are exactly as strong as the original forms, preventing future accidental changes to the _of_card hypotheses. No sorry or admit are introduced.

---

Last updated: 2026-08-18 00:35 UTC.

[github-actions]

Build Timing Report

• Commit: 1cde597
• Message: Merge 7812930 into 32a0c29
• Ref: docs/rabin-of-card-rationale
• Comparison baseline: 32a0c29 from merge-base on main.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: library build (warm) lake build; test path lake test.
• Clean build was skipped (warm/incremental CI; no toolchain or lake-manifest change). Runs automatically when lean-toolchain or lake-manifest.json changes, or via Actions → Lean Action CI → Run workflow with clean_build.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Library build (warm)	13.64	13.61	-0.03	ok
Test path	11.35	11.08	-0.27	ok

Incremental Rebuild Signal

• Warm-only run: default CI reuses cached oleans and rebuilds dirty modules only. No same-job clean:warm ratio.

Slowest Current Build Files (warm library build)

Showing 9 slowest current targets from the warm library build log, with comparison against the baseline warm library build log when available.

Current (s)	Baseline (s)	Delta (s)	Path
3.90	4.00	-0.10	CompPoly/Fields/KoalaBear/Ext5/QuinticIrreducible.lean
2.70	2.60	+0.10	CompPoly/Fields/KoalaBear/Ext6/SexticCertData.lean
2.70	2.80	-0.10	CompPoly/Fields/KoalaBear/Ext5/QuinticCertData.lean
2.30	2.10	+0.20	CompPoly/Data/Polynomial/RabinCertificate.lean
1.90	1.90	+0.00	CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean
1.50	1.70	-0.20	CompPoly/Fields/KoalaBear/Ext6.lean
1.50	1.70	-0.20	CompPoly/Fields/KoalaBear/Ext5.lean
1.30	1.40	-0.10	CompPoly/Fields/KoalaBear/Ext6/GaloisField.lean
1.30	1.40	-0.10	CompPoly.lean