[SamuelSchlesinger]

Move monic_of_ne_zero from Complexity.Computability.Complexity.AffineDisperser.BinaryPolynomial to Complexity.Foundations.FieldTheory.Finite.BinaryField (scoped under Cslib), simplifying the existing monic_leastIrreducible proof and deleting the downstream local duplicate.

Addresses item D.7 in #949 (also noted in #939 Section B / #936).

Validation

Validated with the full 6-gate sequence on commit ab3e3bf9:

• lake build --wfail --iofail: passed cleanly (0 errors)
• lake exe mk_all --check: passed cleanly (no update necessary)
• lake test --wfail --iofail: passed cleanly (0 errors)
• lake lint: passed cleanly (linting passed for Complexity)
• lake exe lint-style: passed cleanly (0 warnings)
• lake exe checkInitImports: passed cleanly (0 warnings)
• python3 scripts/check_hygiene.py: passed cleanly
• python3 scripts/check_tidy_surface.py: passed cleanly (1301 public tidy statements matching baseline)
• python3 scripts/check_docs.py --config-only: passed cleanly

AI disclosure

Prepared with Jetski as worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at ab3e3bf.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at ab3e3bf (agent review, not human approval)

Verbatim move of monic_of_ne_zero. monic_leastIrreducible now uses it, and the old caller (BinaryPolynomial.lean:399) resolves. No copy remains, and no aliases are added. CI: https://github.com/cslib-community/complexitylib/actions/runs/40159329189.

Nit: in the Cslib root namespace, monic_of_ne_zero reads as a general polynomial fact, but it is specific to (ZMod 2)[X]. A BinaryField-scoped or …_zmod_two name would be clearer.