---
name: Agoh-Giuga Conjecture Deep Dive (2026-04-20 夕, STEP AG)
description: Agoh-Giuga (Giuga 1950, Agoh 1995) n≤5000 で 0 composite counterexamples. Lean 4 n≤50 で agohGiugaHolds = Nat.Prime の iff 形式 zero-sorry 証明.
type: project
originSessionId: 79081859-fd56-4821-a0d2-932be27d647a
---
# Agoh-Giuga 深堀 — STEP AG (2026-04-20 夕)

## 対象

**Agoh-Giuga conjecture (Giuga 1950, Agoh 1995 再定式化)**:
n が prime ⟺ Σ_{k=1}^{n-1} k^(n-1) ≡ −1 (mod n)

- "⟹" は Fermat's Little Theorem (trivially true)
- "⟸" は 76 年 OPEN
- 反例の必要条件: n は Giuga number + Carmichael number の両方 (極めて稀)
- 実証: 10^4890 以下 counterexample なし (Borwein-Girgensohn-Pinelis)

## 本 session 成果

### 1. 実証 (`scripts/agoh-giuga-verify-rei-lens.ts`)

- **n ≤ 5000**: 669 primes pass / **0 composite counterexamples** ✅
- 計算時間 11.8 秒 (modular exponentiation via BigInt)
- **Mod-96 分布**: 比較的 uniform (top r=7 3.74% / bottom r=25 2.39%, 1.5× variation)
- Oppermann primeHi +14.97% と対比すれば **Rei-neutral** signal

### 2. Lean 4 `AgohGiuga.lean` — **12 theorems zero-sorry**

**★ 中核定理 ★**:

```lean
theorem agoh_giuga_verified_leq_50 :
    ((List.range 51).filter (· ≥ 2)).all (fun n =>
      agohGiugaHolds n = decide (Nat.Prime n)) = true := by native_decide
```

これは Agoh-Giuga の **iff 形式 (full biconditional)** を n ≤ 50 で完全検証. 単に "Fermat's Little Theorem" の方向でなく、**逆向き (composite は通らない)** も含む.

個別 sanity:
- 通過 (primes): `ag_2`, `ag_3`, `ag_5`, `ag_7`
- 不通過 (composites): `ag_4`, `ag_6`, `ag_15`, `ag_25`

補助定理:
- `agoh_giuga_no_composite_counterexample_leq_50` (半分方向)
- `agoh_giuga_prime_sum_eq_p_minus_1` (FLT の Lean 4 empirical instance)

Build time 7.4 秒.

## 新規 AI 生成問題 Q37-Q39

**Q37**: なぜ Agoh-Giuga mod-96 分布は Oppermann primeHi +14.97% 級の非対称を示さないか? "additive prime-gap" (Oppermann) と "multiplicative modular" (Agoh-Giuga) の違い?

**Q38**: Agoh-Giuga (Σ k^(n-1) ≡ -1) と Lehmer (φ(n)|n-1) はどちらも "primality via modular condition". 構造的相互関係 (同値, strictly stronger/weaker) の形式化可能か?

**Q39**: Agoh-Giuga の "power sum" は Q33 Universal Attractor framework の一般化対象となりうるか? iterated 形式 (例: S(n), S(S(n)+n), ...) で attractor を定義できるか?

## D-FUMT₈ 状況

| 項目 | state |
|---|---|
| Agoh-Giuga 全般 (∀n) | NEITHER (OPEN 76 年) |
| Agoh-Giuga n ≤ 5000 empirical | TRUE (0 violations) |
| Lean 4 iff 形式 n ≤ 50 | TRUE (12 zero-sorry) |
| mod-96 Rei signal | TRUE (null - uniform) |
| Q37-Q39 新規 | NEITHER |

## commit

`(push 済, commit ID は次回読み込み時)`

## 累計 (2026-04-20 夕)

- 論文 120 本 publish 済
- Lean 4 theorem +12 (本 session AG)
- 本日合計 Lean 4 +93 (Legendre 11 + Lehmer 8 + ABC 9 + Gilbreath 10 + Andrica 26 + ES 30 + UA 8 + KL 10 + AG 12, dedup 後)
- **Q-ID 連番 Q1 → Q39**