Structural Equivalence: Carmichael + Giuga ↔ giugaSum = -1

The key structural result linking Carmichael/Giuga numbers to the Agoh–Giuga sum. For composite n > 1:

giugaSum n = -1 ↔ IsCarmichaelNumber n ∧ IsGiugaNumber n

Backward direction (⇐)

If n is both Carmichael and Giuga, then giugaSum n = -1.

Proof sketch via CRT:

1. n is squarefree, so n = ∏ p over its prime factors.
2. By CRT, ZMod n ≅ ∏ ZMod p. It suffices to show giugaSum n ≡ -1 (mod p) for each prime p ∣ n.
3. The sum mod p decomposes: values 1, …, n-1 mod p cycle n/p times through the nonzero residues, so ∑_{i=1}^{n-1} i^{n-1} ≡ (n/p) · ∑_{k=1}^{p-1} k^{n-1} (mod p).
4. By the Carmichael/Korselt property, (p-1) ∣ (n-1), so each k^{n-1} ≡ 1 (mod p), giving the inner sum = p - 1 ≡ -1 (mod p).
5. By the Giuga property, p ∣ (n/p - 1), so n/p ≡ 1 (mod p).
6. The product is 1 · (-1) = -1 (mod p).

Forward direction (⇒)

If giugaSum n = -1 for composite n > 1, then n is both Carmichael and Giuga. This direction is harder and is deferred.

theorem structural_backward {n : ℕ} (hc : IsCarmichaelNumber n) (hg : IsGiugaNumber n) : giugaSum n = -1

Structural backward direction. Carmichael + Giuga ⟹ giugaSum = -1.

The proof uses CRT to reduce to prime-by-prime verification, then applies Fermat's little theorem (via Korselt) and the Giuga divisibility condition.

theorem structural_forward {n : ℕ} (hn1 : 1 < n) (hnp : ¬Nat.Prime n) (hs : giugaSum n = -1) : IsCarmichaelNumber n ∧ IsGiugaNumber n

Structural forward direction. giugaSum = -1 for composite n ⟹ Carmichael ∧ Giuga.

This is the harder direction of the structural equivalence.