feat(NumberTheory/Wilson): explicit square root of -1 modulo a prime

[AlyciaBHZ]

Adds an explicit square root of -1 in ZMod p, together with the half-factorial pairing
identity it rests on.

• ZMod.factorial_eq_neg_one_pow_mul_half_factorial_sq: for odd p, pairing each factor
  above (p - 1) / 2 with its negative gives (p - 1)! = (-1)^m * (m !)^2 in ZMod p,
  where m = (p - 1) / 2. This assumes only Odd p, not primality.
• ZMod.half_factorial_sq_eq_neg_one: for prime p with p % 4 ≠ 3, ((p - 1) / 2)! is a
  square root of -1.

Why

Mathlib already has the two neighbouring statements, but not this one:

• ZMod.exists_sq_eq_neg_one_iff gives IsSquare (-1 : ZMod p) ↔ p % 4 ≠ 3 — existence only.
• ZMod.mod_four_ne_three_of_sq_eq_neg_one goes the other way: given some y with y ^ 2 = -1,
  conclude p % 4 ≠ 3.

So the library can tell you a square root exists, and can use one if you already have it, but
there is no way to get from the congruence condition to a specific root. I checked all seventeen
uses of IsSquare (-1 : ZMod _) currently in Mathlib and none of them exhibits a witness.

There is at least one downstream development that reproved the pairing identity because of this:
SumOfTwoSquares/Wilson.lean in seewoo5/DifferentProofs states it verbatim in a docstring,
though only for p ≡ 1 mod 4 and with primality assumed. That seems like the usual sign that a
lemma belongs upstream. I do not have a consumer for it in my own work — I ran into the gap while
formalizing something adjacent and it seemed worth contributing rather than keeping local.

The pairing identity is also worth having separately: it is the core step of the standard
Wilson-theorem argument, and it holds for any odd p, so it is not really a statement about
primes at all.

Placement

half_factorial_sq_eq_neg_one goes naturally in Mathlib/NumberTheory/Wilson.lean, next to
ZMod.wilsons_lemma which it uses. The pairing identity would fit Mathlib/Data/ZMod/Factorial.lean,
but that file carries assert_not_exists TwoSidedIdeal and wilsons_lemma pulls in
FieldTheory.Finite.Basic, so the two may have to live in separate files. I have put both in
Wilson.lean for now — happy to split them if that is preferred.

AI disclosure

Per the AI policy: the Lean proofs were drafted with an OpenAI Codex agent, orchestrated by Claude
Code, and I reviewed the result. Before opening this I re-ran the duplicate search against current
master, against CSLib, Batteries and Lean core, across language:lean on GitHub, and by type
signature on Loogle — the type-level query (Nat.factorial ?n : ZMod ?p) ^ 2 = -1 returns only
mod_four_ne_three_of_sq_eq_neg_one, which is the converse direction. lake build,
lake exe runLinter and lake exe lint-style were run by hand. Please add the LLM-generated
label — I do not have permission to set it myself.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 76dfe476e0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Wilson	1768	1770	+2 (+0.11%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.Wilson	2

---

Declarations diff (regex)

+ factorial_eq_neg_one_pow_mul_half_factorial_sq
+ half_factorial_sq_eq_neg_one

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 76dfe47).

• +2 new declarations
• −0 removed declarations

+ZMod.factorial_eq_neg_one_pow_mul_half_factorial_sq
+ZMod.half_factorial_sq_eq_neg_one

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 76dfe476e0
Reference commit 62244e5ddb

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[wwylele]

Could you reuse the declared variable?

Suggested change

	theorem half_factorial_sq_eq_neg_one (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
	theorem half_factorial_sq_eq_neg_one (hp : p % 4 ≠ 3) :

[wwylele]

Should also add the previous main results here prime_iff_fac_equiv_neg_one

[wwylele]

Suggested change

	/-- If `p` is odd, pairing each factor above `(p - 1) / 2` with its negative gives
	`(p - 1)! = (-1) ^ ((p - 1) / 2) * (((p - 1) / 2)!) ^ 2` in `ZMod p`.
	The identity only needs the modulus to be odd; primality is not required. -/
	theorem factorial_eq_neg_one_pow_mul_half_factorial_sq (p : ℕ) (hp : Odd p) :
	/-- If `p` is odd, pairing each factor above `(p - 1) / 2` with its negative gives
	`(p - 1)! = (-1) ^ ((p - 1) / 2) * (((p - 1) / 2)!) ^ 2` in `ZMod p`. -/
	theorem factorial_eq_neg_one_pow_mul_half_factorial_sq (p : ℕ) (hp : Odd p) :

[wwylele]

The second part reads like straw man argument against something that doesn't exist

Suggested change

	/-- Let `p` be prime with `p % 4 ≠ 3`. Then `((p - 1) / 2)!` is a specified square root of `-1`
	in `ZMod p`.
	This gives an explicit witness, namely the half-factorial itself, rather than merely asserting
	that some square root exists. -/
	/-- Let `p` be prime with `p % 4 ≠ 3`. Then `((p - 1) / 2)!` is a specified square root of `-1`
	in `ZMod p`. -/

[wwylele]

Could you shorten the PR description? (And if it was written by AI, please write it yourself as per the guideline

[AlyciaBHZ]

Thanks — all four applied.

The variable one only affected the second theorem; the first sits above the variable (p : ℕ) [Fact p.Prime] line and does not want the primality instance anyway, so I left its binders explicit.

You are right about the second docstring paragraph. The comparison I had in mind was with ZMod.exists_sq_eq_neg_one_iff, but this file carries assert_not_exists legendreSym.quadratic_reciprocity so I cannot name it here, and arguing against something I am not allowed to mention reads exactly as badly as you say. Dropped.

Added wilsons_lemma and Nat.prime_iff_fac_equiv_neg_one to the main results list as well — you are right that adding a section listing only my own additions was the wrong shape.