{"id":113,"job_id":28,"problem_id":1,"lane_id":3,"type":"formalize","user_id":1,"model":"claude-opus-5","provider":"anthropic","report_md":"# Job #28 (formalize): L4 of `research/lemmaV-parseval.js`, ∑_{a≠0 mod e} F_H(a/e) = h(e − h), proved in Lean 4 against Mathlib; the script's \"equality iff δ = 0\" clause fails\n\n**Caveat first.** L4 is a finite identity that serves the mean-square Lemma V, which is PROVEN in the repo.\nThe route above Lemma V is CLOSED (`research/OUTCOMES.md`, 2026-08-18, as cited in the brief). The Lean\nproof fixes the rung of L4 and of its corollaries (V1) and (V2). It says nothing new about twin primes.\nConflict of interest: my person owns the repository.\n\n**Rung per claim.**\n- **Proven (Lean):**\n  - the counting identity;\n  - the full sum over a mod e;\n  - the sum over a ≠ 0, which is L4;\n  - (V2), |Ψ| ≤ h(g − h);\n  - (V1), Ψ = 0 when g | H.\n- **Refuted:** the script's clause \"with equality iff delta = 0\" (§2).\n  - Counterexample in Lean: the instance g = 2, H = 1, δ = 1.\n  - Also in Lean, the whole family g = 2k, H = k(2j+1), δ = k.\n- **Hand proof, not formalized; verified numerically for g ≤ 16, H ≤ 40:** the converse, that these are the\n  only equality cases with g ∤ H and integer δ ≢ 0 (mod g).\n\nThe file is sorry-free and builds with no errors and no warnings. `#print axioms` on eight declarations\nlists only `propext`, `Classical.choice` and `Quot.sound`; `class_form` uses only `propext`. A negative\ncontrol fails to build.\n\n## 0. The statements as formalized\n\n| Lean (namespace `ParsevalL4`) | statement |\n|---|---|\n| `pairCount e H` | `#((Icc 1 H ×ˢ Icc 1 H).filter (fun p => (e:ℤ) ∣ p.1 − p.2))` |\n| **`pairCount_formula`** | `0 < e → H = Q * e + h → h < e → pairCount e H = e * Q^2 + 2 * h * Q + h` |\n| `class_form` | `h ≤ e → h * (Q+1)^2 + (e − h) * Q^2 = e * Q^2 + 2 * h * Q + h` (the brief's residue-class form) |\n| `ee t`, `F H t` | `exp(2πit)`, and `‖∑ m ∈ Icc 1 H, ee (m * t)‖ ^ 2` (a real number) |\n| **`sum_F_eq_pairCount`** | `0 < e → ∑ a ∈ range e, F H (a / e) = e * pairCount e H` |\n| **`sum_F_nonzero`** (L4) | `0 < e → H = Q * e + h → h < e → ∑ a ∈ Ico 1 e, F H (a / e) = h * (e − h)` (in ℝ) |\n| `Psi g δ H` | `∑ a ∈ Ico 1 g, F H (a / g) * ee (−a δ / g)`, with δ real |\n| **`norm_Psi_le`** (V2) | `0 < g → H = Q * g + h → h < g → ‖Psi g δ H‖ ≤ h * (g − h)` |\n| **`Psi_eq_zero_of_dvd`** (V1) | `0 < g → g ∣ H → Psi g δ H = 0` |\n| **`V2_equality_off_zero`** | `‖Psi 2 1 1‖ = 1 * (2 − 1) ∧ ‖Psi 2 1 1‖ = ‖Psi 2 0 1‖` |\n| **`norm_Psi_half`** | `0 < k → ‖Psi (2k) k (k(2j+1))‖ = k * (2k − k)` |\n\n**Reformulations.**\n- a mod e is taken as a ∈ [0, e), and \"a ≠ 0\" as a ∈ [1, e).\n- m − n is taken in ℤ.\n- e ≥ 1 is a hypothesis. Q and h are explicit, with H = Qe + h and h < e.\n- δ is real, which is more general than the script's use.\n\nNothing else is changed.\n\n## 1. Proof route, as formalized\n\n- **Count.**\n  - Induction on H with D(H+1) = D(H) + 2⌊H/e⌋ + 1. The new pairs are (H+1, n), (m, H+1) and the diagonal.\n  - #{n ≤ H : e | H+1−n} = ⌊H/e⌋, by the reflection n ↦ H+1−n and `Nat.succ_div`.\n  - The closed form e⌊H/e⌋² + 2(H mod e)⌊H/e⌋ + H mod e satisfies the same recurrence. The proof\n    splits on h+1 < e versus h+1 = e, using `Nat.div_mod_unique`.\n  - The brief's class-size route is recorded as the identity `class_form` but is not used.\n- **Sum.**\n  1. |S|² = S·conj S (`Complex.mul_conj'`), and e(x)·conj e(y) = e(x − y).\n  2. e((m−n)a/e) = (ζ^(m−n))^a with ζ = exp(2πi/e) a primitive e-th root (`Complex.isPrimitiveRoot_exp`).\n  3. Swap the sums.\n  4. Orthogonality: ∑_{a<e} (ζ^k)^a = e·[e | k], via `IsPrimitiveRoot.zpow_eq_one_iff_dvd` and `geom_sum_eq`.\n- **L4.** Subtract a = 0: F_H(0) = H², and e(eQ² + 2hQ + h) − (Qe + h)² = h(e − h), by `linear_combination`.\n- **(V2)** follows from the triangle inequality, with |e(·)| = 1 and F ≥ 0. **(V1)** is (V2) with h = 0.\n\n## 2. The equality clause (challenge to the script)\n\n**What the script says.**\n- Header comment, lines 45–47: \"|Psi| <= Psi(g,0) = h(g-h) [= (V2), with equality iff delta = 0]\".\n- S1 printout, lines 246–248, and the embedded output, lines 642–644: \"(V2) WITH its equality case\".\n\n**The clause fails, in two ways.**\n\n(a) When g | H, both sides are 0 for every δ, by (V1).\n\n(b) Take g ∤ H and integer δ ≢ 0 (mod g). Equality |Ψ| = h(g − h) holds **exactly when g = 2·gcd(g, H)**, i.e.\nH is an odd multiple of g/2, **and δ ≡ g/2 (mod g)**.\n\n**The \"if\" direction, in Lean (`norm_Psi_half`, at δ = k).** The general δ ≡ k (mod 2k) follows by\nperiodicity, which is not formalized. Take g = 2k and H = k(2j+1).\n- At even a = 2b with 0 < b < k: x = e(b/k) ≠ 1 and x^H = 1, so the geometric sum and F_H(a/g) vanish\n  (`F_half_even`).\n- At odd a: e(−ak/(2k)) = −1 (`ee_half_odd`).\n- Hence Ψ = −∑_{a≠0} F_H(a/g) = −h(g − h).\n\nThe instance g = 2, H = 1, δ = 1 is also proved on its own (`V2_equality_off_zero`).\n\n**The \"only if\" direction, by hand (not formalized).**\n1. Equality in the triangle inequality needs every nonzero term F_H(a/g)·e(−aδ/g) to share one phase.\n2. F_H(1/g) > 0, because g ∤ H.\n3. If g ≥ 3 and F_H(2/g) > 0, the phases at a = 1 and a = 2 agree only when e(δ/g) = 1, i.e. g | δ.\n4. F_H(2/g) = 0 iff g | 2H. With g ∤ H, that means g = 2·gcd(g, H).\n5. In that case the nonzero terms are exactly the odd a. For g ≥ 4, a = 1 and a = 3 force e(2δ/g) = 1, so\n   δ ≡ 0 or g/2 (mod g).\n6. For g = 2 (H odd) there is a single term, so every δ gives equality, and δ ≡ 1 = g/2.\n\n**Numerics (verified, over the stated range).** `l4-equality-scan.js` covers g = 2..16 and H = 1..40 with\ng ∤ H, and δ = 1..g−1, 4346 cases in all.\n- Equality holds in 55 cases, and that set equals the predicted set.\n- Every other case falls short of h(g − h) by at least 1.0.\n- L4 itself holds to within 5.4e−13 over the same range.\n\n**Consequence.** L4, (V1) and (V2) stand. The parenthetical should read: equality iff δ ≡ 0 (mod g), or\ng | H, or (g = 2·gcd(g, H) and δ ≡ g/2 (mod g)). I did not trace whether any downstream argument uses the\n\"only if\" half of the clause; that is left open for whoever integrates this. No patch is submitted.\n\n## 3. Build, checks, custody\n\n- **Toolchain.** `leanprover/lean4:v4.33.1` and Lake 5.0.0, with Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`.\n  This is the same project as returns #76, #77, #79 and #89.\n- **Build.** `lake env lean ParsevalL4.lean` exits 0 in 34.6 s wall on an Apple M1, with no output. The file\n  is `ParsevalL4.lean`, 340 lines, sha256 `e3350d5561a355219b1a253e814fd35567f883986bbf79c41435f32190d392dd`,\n  and `grep -c sorry` returns 0.\n- **Iterations.** Three builds:\n  1. two `rw` \"motive is not type correct\" errors on `if` conditions, fixed with `if_congr`; the build was\n     then clean;\n  2. after adding the equality family: an unknown constant, `Nat.Ico_succ_right` (renamed in this Mathlib),\n     so I replaced the reindexing with `Finset.sum_nbij'`;\n  3. clean.\n- **Checks.**\n  - Eight axiom lines, all standard.\n  - `#eval`: the brute-force `pairCount` equals the closed form for all e ≤ 30 and H ≤ 40, the script's S1\n    range. The output is `true`.\n  - Sample values: (3, 7) gives 17 and (30, 40) gives 60.\n- **Negative control.** In a copy, `pairCount_formula`'s closed form was changed to drop `+ h`. The build\n  exits 1: the goal in `pairCount_formula` is left unsolved, and `linear_combination` in `sum_F_nonzero`\n  fails with `-(e h) = 0`.\n- **Scan.** node v25.2.0, about 1 s.\n\n**Files.** Uploaded: `ParsevalL4.lean`, `l4-equality-scan.js` and this report. The checks tail, the logs, the\nscan output and the manifest pins are inline in the recipe, with their sha256 values in `hashes`.\n\n## Sources\n\n- `research/lemmaV-parseval.js`, snapshot `main`, sha256 `22a84fa310418caf75ea1dbd9fe2811264af8f09abc9edd54373d8b12c0d5f44`:\n  - header lines 36–47 (L1–L4 and the corollary with the equality clause);\n  - S1, lines 230–248 (L4 check and proof printout);\n  - embedded output, lines 636–644.\n- `research/OUTCOMES.md` (closed route, 2026-08-18), as cited in the brief; I did not reread it.\n- Mathlib at the commit above: `Complex.isPrimitiveRoot_exp`, `IsPrimitiveRoot.zpow_eq_one_iff_dvd`,\n  `IsPrimitiveRoot.pow_eq_one_iff_dvd`, `geom_sum_eq`, `Complex.mul_conj'`, `Complex.exp_conj`,\n  `Complex.exp_int_mul`, `Complex.exp_pi_mul_I`, `Complex.norm_exp_ofReal_mul_I`, `Finset.sum_mul_sum`,\n  `Finset.sum_comm`, `Finset.sum_Icc_succ_top`, `Finset.sum_nbij'`, `Finset.card_filter`, `Nat.succ_div`,\n  `Nat.div_mod_unique`, `Odd.neg_one_zpow`, `norm_sum_le`.\n\nNo local-only sources.\n\n**Transcript:** from the GET /start that received job #28 to this return. Removed: system reminders,\nthe bearer token, session ids, home, scratchpad and task-directory paths, and an e-mail address.\n","patch":null,"cpu_hours":0.05,"hashes":{"ParsevalL4.lean":"e3350d5561a355219b1a253e814fd35567f883986bbf79c41435f32190d392dd","l4-equality-scan.js":"fb847c4087b4bcd5e92f17c49d6dc639f3941aaa85eeba0a3b393aa7140815a1","l4-build.log (inline in recipe)":"85ce1fd18416d86d1766ce4537540606a40c2f3174a9910719d44572fa9390a2","l4-checks.log (inline in recipe)":"3c6cc5ee8150f2d14b1c5507f24e74f16f3245f2291cafa95728ba8541f0376b","lean-toolchain (inline in recipe)":"3aac669c7a910ec2389f4e4f921b605adf6ebf2d1e0c9b9cd0be4d33f3f5db71","l4-negative.log (inline in recipe)":"eecc54508c066f073e0f6de483ee6c5e55575bd4a6655a32afbd03984e4e9f90","L4ChecksTail.lean (inline in recipe)":"c3123883943161c21025a3f2270971583feab0e66636a5e596d10f74907070d5","l4-equality-scan.out (inline in recipe)":"14272cbe872ab976ba1bd5feb5374eea47e41d8c768d134d689593cee6f3ab56","lake-manifest.json (pins inline in recipe)":"713e3b169ede20be0a2767072005a84a3527c83b748a9420ab769b8e8cd8f278"},"author_rung":"proven","status":"pending","final_rung":null,"created_at":"2026-09-11T15:50:52.042Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[],"messages":[]},"tokens":{"log":"claude-code","input":320,"models":{"claude-opus-5":89155},"output":89155,"source":"claude-jsonl","entries":10,"cache_read":2373269,"cache_write":108077},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe, job #28 (Lean 4 + Mathlib cache; about 35 seconds per build once the cache is present, three builds; one 1-second node run)\n\n1. Toolchain and project, as in job #22 (return #76):\n   ```\n   curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --no-modify-path --default-toolchain none\n   export PATH=\"$HOME/.elan/bin:$PATH\"\n   lake +leanprover/lean4:stable new alt22 math && cd alt22\n   lake exe cache get\n   ```\n   Pins are below. `lean-toolchain` is `leanprover/lean4:v4.33.1` (sha256 `3aac669c7a910ec2389f4e4f921b605adf6ebf2d1e0c9b9cd0be4d33f3f5db71`), and Mathlib is at `0df444a360eaa60ab8c11dca51a86af692955474`.\n2. Save the file below as `ParsevalL4.lean` (sha256 `e3350d5561a355219b1a253e814fd35567f883986bbf79c41435f32190d392dd`) and run `/usr/bin/time -p lake env lean ParsevalL4.lean > l4-build.log 2>&1`.\n   Expected: exit 0, and no Lean output (the log holds only the three timing lines), about 35 s on an Apple M1. `grep -c sorry ParsevalL4.lean` prints 0.\n3. Checks: `cat ParsevalL4.lean L4ChecksTail.lean > ParsevalL4Checks.lean` with the tail below, then\n   `lake env lean ParsevalL4Checks.lean > l4-checks.log 2>&1; echo \"exit $?\" >> l4-checks.log`.\n   Expected: the log below, with eight axiom lines (no `sorryAx`), `true` for the brute-force pair count against e Q² + 2 h Q + h over e ≤ 30 and H ≤ 40,\n   and the sample values. Exit 0.\n4. Negative control: in a copy `ParsevalL4Neg.lean`, change the statement line of `pairCount_formula` from\n   `pairCount e H = e * Q ^ 2 + 2 * h * Q + h := by` to `pairCount e H = e * Q ^ 2 + 2 * h * Q := by`, then\n   `lake env lean ParsevalL4Neg.lean > l4-negative.log 2>&1; echo \"exit $?\" >> l4-negative.log`.\n   Expected: exit 1, with the log below: unsolved goal in `pairCount_formula`, and `linear_combination` failing in `sum_F_nonzero` with `-(e h) = 0`.\n5. Equality-case scan (not part of the Lean proof): `node l4-equality-scan.js > l4-equality-scan.out` (node v25.2.0; script sha256 `fb847c4087b4bcd5e92f17c49d6dc639f3941aaa85eeba0a3b393aa7140815a1`,\n   uploaded and inline below). Expected output below, sha256 `14272cbe872ab976ba1bd5feb5374eea47e41d8c768d134d689593cee6f3ab56`: 4346 cases, 55 observed equality cases equal to the predicted set, smallest other gap 1.000000.\n\nWhat reviewers should check by eye:\n- the definitions `ind`, `pairCount`, `ee`, `F`, `Psi` and the statements of `pairCount_formula`, `sum_F_nonzero`, `norm_Psi_le`, `Psi_eq_zero_of_dvd`, `V2_equality_off_zero`, `norm_Psi_half` against the brief and `research/lemmaV-parseval.js` lines 36-47;\n- `a` runs over `range e` and `Ico 1 e`; `m − n` is taken in ℤ; `δ` is real.\n\n## ParsevalL4.lean (full text)\n\n```lean\nimport Mathlib\n\n/-!\n# L4 of `research/lemmaV-parseval.js`: `∑_{a ≠ 0 mod e} F_H(a/e) = h(e − h)` for `H = Qe + h`\n\nJob #28 (formalize). L4 is a finite identity that serves the mean-square Lemma V (PROVEN in the repo), whose\nroute above it is CLOSED (`research/OUTCOMES.md`, 2026-08-18). A Lean proof fixes the rung of this identity\nonly.\n\n* `pairCount e H = #{(m, n) ∈ [1, H]² : e ∣ m − n}`. `pairCount_formula`: for `H = Q e + h`, `h < e`, it\n  equals `e Q² + 2 h Q + h`. The proof is by induction on `H`, using `D(H+1) = D(H) + 2⌊H/e⌋ + 1`.\n  `class_form` records the brief's `h(Q+1)² + (e−h)Q²`.\n* `F H t = ‖∑_{m=1}^{H} e(m t)‖²` with `e(t) = exp(2πit)`. `sum_F_eq_pairCount`:\n  `∑_{a=0}^{e−1} F_H(a/e) = e · pairCount e H`. The proof expands `|S|² = S · conj S`, swaps the sums, and\n  uses orthogonality `∑_{a<e} ζ^{ka} = e·[e ∣ k]` for `ζ = exp(2πi/e)` (`Complex.isPrimitiveRoot_exp`).\n* `sum_F_nonzero`: `∑_{a=1}^{e−1} F_H(a/e) = h(e − h)`, which is L4.\n* `Psi g δ H = ∑_{a=1}^{g−1} F_H(a/g) e(−aδ/g)`. `norm_Psi_le` is the script's (V2): `‖Ψ‖ ≤ h(g − h)`.\n  `Psi_eq_zero_of_dvd` is (V1): `Ψ = 0` when `g ∣ H`.\n* `V2_equality_off_zero`: the script's clause \"with equality iff delta = 0\" fails at `g = 2, H = 1, δ = 1`,\n  where `‖Ψ‖ = h(g − h) = Ψ(2, 0, 1) = 1`. `norm_Psi_half` gives the family: `g = 2k`, `H = k(2j+1)`, `δ = k`.\n-/\n\nopen Complex Finset\nopen scoped Real ComplexConjugate\n\nnamespace ParsevalL4\n\n/-! ## The count over ℕ -/\n\n/-- The indicator `[e ∣ m − n]`, with the difference taken in `ℤ`. -/\ndef ind (e m n : ℕ) : ℕ := if (e : ℤ) ∣ (m : ℤ) - n then 1 else 0\n\n/-- `#{(m, n) ∈ [1, H]² : e ∣ m − n}`. -/\ndef pairCount (e H : ℕ) : ℕ :=\n  ((Icc 1 H ×ˢ Icc 1 H).filter (fun p : ℕ × ℕ => (e : ℤ) ∣ (p.1 : ℤ) - p.2)).card\n\n/-- The same count as a double sum of indicators. -/\ndef pairSum (e H : ℕ) : ℕ := ∑ m ∈ Icc 1 H, ∑ n ∈ Icc 1 H, ind e m n\n\ntheorem pairCount_eq_pairSum (e H : ℕ) : pairCount e H = pairSum e H := by\n  unfold pairCount pairSum ind\n  rw [Finset.card_filter, Finset.sum_product]\n\nlemma ind_comm (e m n : ℕ) : ind e m n = ind e n m := by\n  unfold ind\n  exact if_congr dvd_sub_comm rfl rfl\n\nlemma ind_self (e m : ℕ) : ind e m m = 1 := by\n  simp [ind]\n\nlemma count_dvd (e H : ℕ) : ∑ k ∈ Icc 1 H, (if e ∣ k then 1 else 0) = H / e := by\n  induction H with\n  | zero => simp\n  | succ k ih => rw [Finset.sum_Icc_succ_top (by omega), ih, Nat.succ_div]\n\n/-- `#{n ∈ [1, H] : e ∣ (H + 1) − n} = ⌊H/e⌋`, by the reflection `n ↦ H + 1 − n`. -/\nlemma count_shift (e H : ℕ) : ∑ n ∈ Icc 1 H, ind e (H + 1) n = H / e := by\n  rw [← count_dvd e H]\n  refine Finset.sum_nbij' (fun n => H + 1 - n) (fun k => H + 1 - k) ?_ ?_ ?_ ?_ ?_\n  · intro n hn\n    simp only [Finset.mem_Icc] at hn ⊢\n    omega\n  · intro k hk\n    simp only [Finset.mem_Icc] at hk ⊢\n    omega\n  · intro n hn\n    simp only [Finset.mem_Icc] at hn\n    omega\n  · intro k hk\n    simp only [Finset.mem_Icc] at hk\n    omega\n  · intro n hn\n    simp only [Finset.mem_Icc] at hn\n    unfold ind\n    have h : ((H + 1 : ℕ) : ℤ) - (n : ℤ) = ((H + 1 - n : ℕ) : ℤ) := by omega\n    exact if_congr (by rw [h, Int.natCast_dvd_natCast]) rfl rfl\n\nlemma pairSum_succ (e H : ℕ) : pairSum e (H + 1) = pairSum e H + 2 * (H / e) + 1 := by\n  unfold pairSum\n  rw [Finset.sum_Icc_succ_top (by omega : 1 ≤ H + 1)]\n  have hin : ∀ m, ∑ n ∈ Icc 1 (H + 1), ind e m n = ∑ n ∈ Icc 1 H, ind e m n + ind e m (H + 1) :=\n    fun m => Finset.sum_Icc_succ_top (by omega) _\n  simp only [hin, Finset.sum_add_distrib, ind_self]\n  have h1 : ∑ m ∈ Icc 1 H, ind e m (H + 1) = H / e := by\n    rw [← count_shift e H]\n    exact Finset.sum_congr rfl fun m _ => ind_comm e m (H + 1)\n  rw [h1, count_shift]\n  ring\n\n/-- The closed form `e Q² + 2 h Q + h` with `Q = ⌊H/e⌋`, `h = H mod e`. -/\ndef closedForm (e H : ℕ) : ℕ := e * (H / e) ^ 2 + 2 * (H % e) * (H / e) + H % e\n\nlemma closedForm_succ {e : ℕ} (he : 0 < e) (H : ℕ) :\n    closedForm e (H + 1) = closedForm e H + 2 * (H / e) + 1 := by\n  unfold closedForm\n  have hdm : H % e + e * (H / e) = H := Nat.mod_add_div H e\n  have hlt : H % e < e := Nat.mod_lt H he\n  generalize hQ : H / e = Q at hdm ⊢\n  generalize hr : H % e = r at hdm hlt ⊢\n  rcases Nat.lt_or_ge (r + 1) e with h | h\n  · obtain ⟨h1, h2⟩ := (Nat.div_mod_unique he).2 ⟨(by linarith : r + 1 + e * Q = H + 1), h⟩\n    rw [h1, h2]\n    ring\n  · have he' : e = r + 1 := by omega\n    obtain ⟨h1, h2⟩ := (Nat.div_mod_unique he).2 ⟨(by linarith : 0 + e * (Q + 1) = H + 1), he⟩\n    rw [h1, h2, he']\n    ring\n\ntheorem pairSum_eq_closedForm {e : ℕ} (he : 0 < e) (H : ℕ) : pairSum e H = closedForm e H := by\n  induction H with\n  | zero => simp [pairSum, closedForm]\n  | succ k ih => rw [pairSum_succ, ih, closedForm_succ he]\n\n/-- The counting identity: for `H = Q e + h` with `h < e`, the number of pairs is `e Q² + 2 h Q + h`. -/\ntheorem pairCount_formula {e H Q h : ℕ} (he : 0 < e) (hH : H = Q * e + h) (hh : h < e) :\n    pairCount e H = e * Q ^ 2 + 2 * h * Q + h := by\n  obtain ⟨hQ, hr⟩ := (Nat.div_mod_unique he).2 ⟨(by rw [hH]; ring : h + e * Q = H), hh⟩\n  rw [pairCount_eq_pairSum, pairSum_eq_closedForm he, closedForm, hQ, hr]\n\n/-- The residue-class form: `h` classes of size `Q + 1` and `e − h` of size `Q`. -/\ntheorem class_form {e Q h : ℕ} (hh : h ≤ e) :\n    h * (Q + 1) ^ 2 + (e - h) * Q ^ 2 = e * Q ^ 2 + 2 * h * Q + h := by\n  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hh\n  rw [Nat.add_sub_cancel_left]\n  ring\n\n/-! ## The complex sum -/\n\n/-- `e(t) = exp(2πit)`. -/\nnoncomputable def ee (t : ℝ) : ℂ := Complex.exp (2 * π * I * t)\n\n/-- `F_H(t) = |∑_{m=1}^{H} e(m t)|²`. -/\nnoncomputable def F (H : ℕ) (t : ℝ) : ℝ := ‖∑ m ∈ Icc 1 H, ee (m * t)‖ ^ 2\n\nlemma norm_ee (t : ℝ) : ‖ee t‖ = 1 := by\n  unfold ee\n  rw [show 2 * (π : ℂ) * I * (t : ℂ) = ((2 * π * t : ℝ) : ℂ) * I by push_cast; ring]\n  exact Complex.norm_exp_ofReal_mul_I _\n\nlemma F_nonneg (H : ℕ) (t : ℝ) : 0 ≤ F H t := by\n  unfold F\n  positivity\n\nlemma ee_mul_conj (x y : ℝ) : ee x * conj (ee y) = ee (x - y) := by\n  unfold ee\n  rw [← Complex.exp_conj, ← Complex.exp_add]\n  congr 1\n  simp only [map_mul, map_ofNat, Complex.conj_ofReal, Complex.conj_I]\n  push_cast\n  ring\n\nlemma ee_int_mul (e : ℕ) (k : ℤ) (a : ℕ) :\n    ee ((k : ℝ) * a / e) = (Complex.exp (2 * π * I / e) ^ k) ^ a := by\n  unfold ee\n  rw [← zpow_natCast, ← zpow_mul, ← Complex.exp_int_mul]\n  congr 1\n  push_cast\n  ring\n\n/-- Orthogonality: `∑_{a<e} (ζ^k)^a = e` if `e ∣ k` and `0` otherwise, for `ζ = exp(2πi/e)`. -/\nlemma orth {e : ℕ} (he : 0 < e) (k : ℤ) :\n    ∑ a ∈ range e, (Complex.exp (2 * π * I / e) ^ k) ^ a = if (e : ℤ) ∣ k then (e : ℂ) else 0 := by\n  have hζ := Complex.isPrimitiveRoot_exp e he.ne'\n  split_ifs with hk\n  · rw [(hζ.zpow_eq_one_iff_dvd k).2 hk]\n    simp\n  · have hne : Complex.exp (2 * π * I / e) ^ k ≠ 1 := fun h => hk ((hζ.zpow_eq_one_iff_dvd k).1 h)\n    have hpow : (Complex.exp (2 * π * I / e) ^ k) ^ e = 1 := by\n      rw [← zpow_natCast, ← zpow_mul, mul_comm k (e : ℤ), zpow_mul, zpow_natCast, hζ.pow_eq_one, one_zpow]\n    rw [geom_sum_eq hne, hpow, sub_self, zero_div]\n\nlemma F_eq (H : ℕ) (t : ℝ) :\n    (F H t : ℂ) = ∑ m ∈ Icc 1 H, ∑ n ∈ Icc 1 H, ee (((m : ℝ) - n) * t) := by\n  unfold F\n  rw [Complex.ofReal_pow, ← Complex.mul_conj', map_sum, Finset.sum_mul_sum]\n  refine Finset.sum_congr rfl fun m _ => Finset.sum_congr rfl fun n _ => ?_\n  rw [ee_mul_conj]\n  congr 1\n  ring\n\n/-- `∑_{a=0}^{e−1} F_H(a/e) = e · #{(m, n) ∈ [1, H]² : e ∣ m − n}`. -/\ntheorem sum_F_eq_pairCount {e : ℕ} (he : 0 < e) (H : ℕ) :\n    ∑ a ∈ range e, F H ((a : ℝ) / e) = e * pairCount e H := by\n  apply Complex.ofReal_injective\n  push_cast\n  rw [pairCount_eq_pairSum]\n  unfold pairSum\n  push_cast\n  simp_rw [Finset.mul_sum, F_eq]\n  have hterm : ∀ a m n : ℕ, ee (((m : ℝ) - n) * ((a : ℝ) / e)) =\n      (Complex.exp (2 * π * I / e) ^ ((m : ℤ) - n)) ^ a := by\n    intro a m n\n    rw [← ee_int_mul]\n    congr 1\n    push_cast\n    ring\n  simp_rw [hterm]\n  rw [Finset.sum_comm]\n  refine Finset.sum_congr rfl fun m _ => ?_\n  rw [Finset.sum_comm]\n  refine Finset.sum_congr rfl fun n _ => ?_\n  rw [orth he]\n  unfold ind\n  split_ifs <;> simp\n\nlemma F_zero (H : ℕ) : F H 0 = (H : ℝ) ^ 2 := by\n  unfold F ee\n  simp\n\n/-- **L4.** For `H = Q e + h` with `h < e`: `∑_{a=1}^{e−1} F_H(a/e) = h(e − h)`. -/\ntheorem sum_F_nonzero {e H Q h : ℕ} (he : 0 < e) (hH : H = Q * e + h) (hh : h < e) :\n    ∑ a ∈ Ico 1 e, F H ((a : ℝ) / e) = (h : ℝ) * ((e : ℝ) - h) := by\n  have hfull := sum_F_eq_pairCount he H\n  have hsplit : range e = insert 0 (Ico 1 e) := by\n    ext a\n    simp only [Finset.mem_range, Finset.mem_insert, Finset.mem_Ico]\n    omega\n  rw [hsplit, Finset.sum_insert (by simp), pairCount_formula he hH hh] at hfull\n  rw [Nat.cast_zero, zero_div, F_zero] at hfull\n  subst hH\n  push_cast at hfull\n  linear_combination hfull\n\n/-! ## The consequences (V1), (V2), and the equality clause -/\n\n/-- `Ψ(g, δ, H) = ∑_{a=1}^{g−1} F_H(a/g) e(−aδ/g)`. -/\nnoncomputable def Psi (g : ℕ) (δ : ℝ) (H : ℕ) : ℂ :=\n  ∑ a ∈ Ico 1 g, (F H ((a : ℝ) / g) : ℂ) * ee (-(a : ℝ) * δ / g)\n\n/-- (V2): `‖Ψ(g, δ, H)‖ ≤ h(g − h)` for `H = Q g + h`, `h < g`. -/\ntheorem norm_Psi_le {g H Q h : ℕ} (hg : 0 < g) (hH : H = Q * g + h) (hh : h < g) (δ : ℝ) :\n    ‖Psi g δ H‖ ≤ (h : ℝ) * ((g : ℝ) - h) := by\n  unfold Psi\n  refine (norm_sum_le _ _).trans (le_of_eq ?_)\n  rw [← sum_F_nonzero hg hH hh]\n  refine Finset.sum_congr rfl fun a _ => ?_\n  rw [norm_mul, norm_ee, mul_one, Complex.norm_real, Real.norm_of_nonneg (F_nonneg _ _)]\n\n/-- (V1): `Ψ(g, δ, H) = 0` when `g ∣ H`. -/\ntheorem Psi_eq_zero_of_dvd {g H : ℕ} (hg : 0 < g) (hdvd : g ∣ H) (δ : ℝ) : Psi g δ H = 0 := by\n  obtain ⟨Q, rfl⟩ := hdvd\n  have h := norm_Psi_le hg (by ring : g * Q = Q * g + 0) hg δ\n  simpa using h\n\nlemma F_one (t : ℝ) : F 1 t = 1 := by\n  unfold F\n  simp [norm_ee]\n\n/-- The script's \"(V2) with equality iff delta = 0\" fails: at `g = 2, H = 1` (so `h = 1`) the bound\n`h(g − h) = 1` is attained at `δ = 1` as well as at `δ = 0`. -/\ntheorem V2_equality_off_zero :\n    ‖Psi 2 1 1‖ = ((1 : ℕ) : ℝ) * (((2 : ℕ) : ℝ) - ((1 : ℕ) : ℝ)) ∧ ‖Psi 2 1 1‖ = ‖Psi 2 0 1‖ := by\n  have key : ∀ δ : ℝ, ‖Psi 2 δ 1‖ = 1 := by\n    intro δ\n    unfold Psi\n    rw [show Finset.Ico 1 2 = {1} by decide, Finset.sum_singleton, F_one]\n    simp [norm_ee]\n  exact ⟨by rw [key]; norm_num, by rw [key, key]⟩\n\n/-! ## The equality cases of (V2) away from `δ ≡ 0` -/\n\nlemma sum_Icc_pow_eq_zero {x : ℂ} {H : ℕ} (hx : x ≠ 1) (hH : x ^ H = 1) :\n    ∑ m ∈ Icc 1 H, x ^ m = 0 := by\n  have hre : ∑ m ∈ Icc 1 H, x ^ m = ∑ i ∈ range H, x ^ (i + 1) := by\n    refine Finset.sum_nbij' (fun m => m - 1) (fun i => i + 1) ?_ ?_ ?_ ?_ ?_\n    · intro m hm\n      simp only [Finset.mem_Icc, Finset.mem_range] at hm ⊢\n      omega\n    · intro i hi\n      simp only [Finset.mem_Icc, Finset.mem_range] at hi ⊢\n      omega\n    · intro m hm\n      simp only [Finset.mem_Icc] at hm\n      omega\n    · intro i hi\n      simp only [Finset.mem_range] at hi\n      omega\n    · intro m hm\n      simp only [Finset.mem_Icc] at hm\n      congr 1\n      omega\n  rw [hre]\n  simp_rw [pow_succ, ← Finset.sum_mul]\n  rw [geom_sum_eq hx, hH, sub_self, zero_div, zero_mul]\n\n/-- For `H = k(2j+1)`, `F_H(2b/(2k)) = 0` when `0 < b < k`. -/\nlemma F_half_even {k j b : ℕ} (hb0 : 0 < b) (hbk : b < k) :\n    F (k * (2 * j + 1)) (((2 * b : ℕ) : ℝ) / ((2 * k : ℕ) : ℝ)) = 0 := by\n  have hk : 0 < k := by omega\n  have hζ := Complex.isPrimitiveRoot_exp k hk.ne'\n  have hterm : ∀ m : ℕ, ee ((m : ℝ) * (((2 * b : ℕ) : ℝ) / ((2 * k : ℕ) : ℝ))) =\n      (Complex.exp (2 * π * I / k) ^ b) ^ m := by\n    intro m\n    rw [show (m : ℝ) * (((2 * b : ℕ) : ℝ) / ((2 * k : ℕ) : ℝ)) = ((b : ℤ) : ℝ) * m / k by\n      push_cast\n      rw [mul_div_mul_left _ _ (by norm_num : (2 : ℝ) ≠ 0)]\n      ring]\n    rw [ee_int_mul, zpow_natCast]\n  unfold F\n  simp_rw [hterm]\n  have hx : Complex.exp (2 * π * I / k) ^ b ≠ 1 := by\n    rw [Ne, hζ.pow_eq_one_iff_dvd]\n    exact Nat.not_dvd_of_pos_of_lt hb0 hbk\n  have hH : (Complex.exp (2 * π * I / k) ^ b) ^ (k * (2 * j + 1)) = 1 := by\n    rw [← pow_mul, show b * (k * (2 * j + 1)) = k * (b * (2 * j + 1)) by ring, pow_mul, hζ.pow_eq_one, one_pow]\n  rw [sum_Icc_pow_eq_zero hx hH, norm_zero]\n  norm_num\n\n/-- At odd `a`, `e(−a k/(2k)) = −1`. -/\nlemma ee_half_odd {k a : ℕ} (hk : 0 < k) (ha : Odd a) :\n    ee (-(a : ℝ) * (k : ℝ) / ((2 * k : ℕ) : ℝ)) = -1 := by\n  have hkR : (k : ℝ) ≠ 0 := by exact_mod_cast hk.ne'\n  rw [show -(a : ℝ) * (k : ℝ) / ((2 * k : ℕ) : ℝ) = ((-(a : ℤ) : ℤ) : ℝ) * ((1 : ℕ) : ℝ) / ((2 : ℕ) : ℝ) by\n    push_cast\n    field_simp]\n  rw [ee_int_mul, pow_one, show 2 * (π : ℂ) * I / ((2 : ℕ) : ℂ) = π * I by push_cast; ring, Complex.exp_pi_mul_I]\n  have hodd : Odd (a : ℤ) := ha.natCast\n  rw [zpow_neg, hodd.neg_one_zpow]\n  norm_num\n\n/-- The equality case of (V2) at `δ ≢ 0`: for `g = 2k` and `H = k(2j+1)` (so `h = k`), `‖Ψ(g, k, H)‖ = h(g − h)`. -/\ntheorem norm_Psi_half {k j : ℕ} (hk : 0 < k) :\n    ‖Psi (2 * k) k (k * (2 * j + 1))‖ = (k : ℝ) * (((2 * k : ℕ) : ℝ) - k) := by\n  have hsum := sum_F_nonzero (e := 2 * k) (H := k * (2 * j + 1)) (Q := j) (h := k) (by omega) (by ring) (by omega)\n  have hterm : ∀ a ∈ Ico 1 (2 * k),\n      (F (k * (2 * j + 1)) ((a : ℝ) / ((2 * k : ℕ) : ℝ)) : ℂ) * ee (-(a : ℝ) * (k : ℝ) / ((2 * k : ℕ) : ℝ)) =\n        -(F (k * (2 * j + 1)) ((a : ℝ) / ((2 * k : ℕ) : ℝ)) : ℂ) := by\n    intro a ha\n    rw [Finset.mem_Ico] at ha\n    rcases Nat.even_or_odd a with ⟨b, rfl⟩ | hodd\n    · have h0 := F_half_even (k := k) (j := j) (b := b) (by omega) (by omega)\n      rw [show ((b + b : ℕ) : ℝ) = ((2 * b : ℕ) : ℝ) by push_cast; ring, h0]\n      simp\n    · rw [ee_half_odd hk hodd]\n      ring\n  unfold Psi\n  rw [Finset.sum_congr rfl hterm, Finset.sum_neg_distrib, norm_neg, ← Complex.ofReal_sum, Complex.norm_real,\n    Real.norm_of_nonneg (Finset.sum_nonneg fun a _ => F_nonneg _ _), hsum]\n\nend ParsevalL4\n```\n\n## L4ChecksTail.lean (appended to a copy of ParsevalL4.lean for step 3; sha256 `c3123883943161c21025a3f2270971583feab0e66636a5e596d10f74907070d5`)\n\n```lean\n/-! ## Checks (appended to a copy of `ParsevalL4.lean`; not part of the proof file) -/\n\n#print axioms ParsevalL4.pairCount_formula\n#print axioms ParsevalL4.class_form\n#print axioms ParsevalL4.sum_F_eq_pairCount\n#print axioms ParsevalL4.sum_F_nonzero\n#print axioms ParsevalL4.norm_Psi_le\n#print axioms ParsevalL4.Psi_eq_zero_of_dvd\n#print axioms ParsevalL4.V2_equality_off_zero\n#print axioms ParsevalL4.norm_Psi_half\n\n-- The pair count by brute force (Finset filter) against e Q² + 2 h Q + h, over the script's range e ≤ 30, H ≤ 40.\n#eval ((List.range 30).map (· + 1)).all fun e => (List.range 41).all fun H =>\n  ParsevalL4.pairCount e H == e * (H / e) ^ 2 + 2 * (H % e) * (H / e) + H % e\n\n-- A few values (e, H, count).\n#eval [(1, 5), (3, 7), (5, 12), (7, 7), (30, 40)].map fun (e, H) => (e, H, ParsevalL4.pairCount e H)\n```\n\n## Build output (l4-build.log, sha256 `85ce1fd18416d86d1766ce4537540606a40c2f3174a9910719d44572fa9390a2`)\n\n```\nreal 34.62\nuser 4.87\nsys 14.35\n```\n\n## Checks (l4-checks.log, sha256 `3c6cc5ee8150f2d14b1c5507f24e74f16f3245f2291cafa95728ba8541f0376b`)\n\n```\n'ParsevalL4.pairCount_formula' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ParsevalL4.class_form' depends on axioms: [propext]\n'ParsevalL4.sum_F_eq_pairCount' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ParsevalL4.sum_F_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ParsevalL4.norm_Psi_le' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ParsevalL4.Psi_eq_zero_of_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ParsevalL4.V2_equality_off_zero' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ParsevalL4.norm_Psi_half' depends on axioms: [propext, Classical.choice, Quot.sound]\ntrue\n[(1, 5, 25), (3, 7, 17), (5, 12, 30), (7, 7, 7), (30, 40, 60)]\nexit 0\n```\n\n## Negative control, full log (l4-negative.log, sha256 `eecc54508c066f073e0f6de483ee6c5e55575bd4a6655a32afbd03984e4e9f90`)\n\n```\nParsevalL4Neg.lean:116:45: error: unsolved goals\ne H Q h : ℕ\nhe : 0 < e\nhH : H = Q * e + h\nhh : h < e\nhQ : H / e = Q\nhr : H % e = h\n⊢ e * Q ^ 2 + 2 * h * Q + h = e * Q ^ 2 + 2 * h * Q\nParsevalL4Neg.lean:222:2: error: ring failed, ring expressions not equal\ne Q h : ℕ\nhe : 0 < e\nhh : h < e\nhsplit : range e = insert 0 (Ico 1 e)\nhfull : (↑Q * ↑e + ↑h) ^ 2 + ∑ x ∈ Ico 1 e, F (Q * e + h) (↑x / ↑e) = ↑e * (↑e * ↑Q ^ 2 + 2 * ↑h * ↑Q)\n⊢ -(↑e * ↑h) = 0\nexit 1\n```\n\n## l4-equality-scan.js (sha256 `fb847c4087b4bcd5e92f17c49d6dc639f3941aaa85eeba0a3b393aa7140815a1`)\n\n```js\n// Job #28: where does |Psi(g, delta, H)| = h(g-h) hold with delta != 0 mod g?  (h = H mod g != 0; integer delta.)\n// Psi(g, delta, H) = sum_{a=1}^{g-1} F_H(a/g) e(-a delta/g),  F_H(t) = |sum_{m=1}^{H} e(mt)|^2.  Double precision, tol 1e-9.\n// Prediction tested: equality at delta != 0 mod g  <=>  g = 2 gcd(g, H) and delta = g/2.\nconst G = 16, HMAX = 40, TOL = 1e-9;\nconst gcd = (a, b) => { while (b) [a, b] = [b, a % b]; return a; };\nfunction F(H, t) { let re = 0, im = 0; for (let m = 1; m <= H; m++) { re += Math.cos(2 * Math.PI * m * t); im += Math.sin(2 * Math.PI * m * t); } return re * re + im * im; }\nlet cases = 0, maxBoundErr = 0, minGap = Infinity; const observed = [], predicted = [];\nfor (let g = 2; g <= G; g++) for (let H = 1; H <= HMAX; H++) {\n  const h = H % g; if (h === 0) continue;\n  const Fa = []; for (let a = 1; a < g; a++) Fa.push(F(H, a / g));\n  const S0 = Fa.reduce((x, y) => x + y, 0); maxBoundErr = Math.max(maxBoundErr, Math.abs(S0 - h * (g - h)));\n  for (let d = 1; d < g; d++) {\n    let re = 0, im = 0; for (let a = 1; a < g; a++) { re += Fa[a - 1] * Math.cos(-2 * Math.PI * a * d / g); im += Fa[a - 1] * Math.sin(-2 * Math.PI * a * d / g); }\n    cases++;\n    const gap = h * (g - h) - Math.hypot(re, im);\n    if (gap <= TOL) observed.push(`${g},${H},${d}`); else minGap = Math.min(minGap, gap);\n    if (g % 2 === 0 && gcd(g, H) === g / 2 && d === g / 2) predicted.push(`${g},${H},${d}`);\n  }\n}\nconsole.log(`scan g=2..${G}, H=1..${HMAX} with g not dividing H, integer delta=1..g-1: ${cases} cases`);\nconsole.log(`L4 check: max |sum_{a!=0} F_H(a/g) - h(g-h)| = ${maxBoundErr.toExponential(2)}`);\nconsole.log(`equality |Psi| = h(g-h) at delta != 0 mod g: observed ${observed.length}, predicted ${predicted.length}`);\nconsole.log(`observed set equals predicted set: ${observed.length === predicted.length && observed.every((x, i) => x === predicted[i])}`);\nconsole.log(`smallest non-equality gap h(g-h) - |Psi|: ${minGap.toFixed(6)}`);\nconsole.log(`all equality cases (g,H,delta): ${observed.join('  ')}`);\n```\n\n## l4-equality-scan.out (sha256 `14272cbe872ab976ba1bd5feb5374eea47e41d8c768d134d689593cee6f3ab56`)\n\n```\nscan g=2..16, H=1..40 with g not dividing H, integer delta=1..g-1: 4346 cases\nL4 check: max |sum_{a!=0} F_H(a/g) - h(g-h)| = 5.40e-13\nequality |Psi| = h(g-h) at delta != 0 mod g: observed 55, predicted 55\nobserved set equals predicted set: true\nsmallest non-equality gap h(g-h) - |Psi|: 1.000000\nall equality cases (g,H,delta): 2,1,1  2,3,1  2,5,1  2,7,1  2,9,1  2,11,1  2,13,1  2,15,1  2,17,1  2,19,1  2,21,1  2,23,1  2,25,1  2,27,1  2,29,1  2,31,1  2,33,1  2,35,1  2,37,1  2,39,1  4,2,2  4,6,2  4,10,2  4,14,2  4,18,2  4,22,2  4,26,2  4,30,2  4,34,2  4,38,2  6,3,3  6,9,3  6,15,3  6,21,3  6,27,3  6,33,3  6,39,3  8,4,4  8,12,4  8,20,4  8,28,4  8,36,4  10,5,5  10,15,5  10,25,5  10,35,5  12,6,6  12,18,6  12,30,6  14,7,7  14,21,7  14,35,7  16,8,8  16,24,8  16,40,8\n```\n\n## lake-manifest.json pins (sha256 `713e3b169ede20be0a2767072005a84a3527c83b748a9420ab769b8e8cd8f278`)\n\n```\nmathlib 0df444a360eaa60ab8c11dca51a86af692955474 v4.33.1\nplausible b7eb3304aeae834b12dda98993a37f6a41f6f0bb main\nLeanSearchClient 5f4d51b81cbd3f6b32b156bfad9056621a040404 main\nimportGraph 16f02aa7642864af59f1ff0e384a015994db9118 main\nproofwidgets 4be2e3d5087eeb272cf5a8853b8f9dd025ef5957 main\naesop 3448c0bcc5ce01b2d1546e483ec3620e32df3d0e master\nQq 92c15be17b7caf78c2ad767ec40f89052d908d81 master\nbatteries 4488d40d070b9700d4d5a6aa342f0d40c31b2a2d main\nCli 6130a47896ce867c6a4a55373441e59e565bad0f v4.33.0\n```","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":21},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":null,"research_route_id":null,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-09-11T15:50:52.066Z","department_id":null,"run_id":null,"triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"Calibration per `CLAUDE.md`: L4 is a finite identity proved in one paragraph inside `research/lemmaV-parseval.js` (embedded output, section S1) and verified numerically for e <= 30, H <= 40. The lemma it serves (mean-square Lemma V) is PROVEN in the repo; the route above it is CLOSED (`research/OUTCOMES.md`, 2026-08-18). A Lean proof fixes the rung of this identity only.\n\nStatement. For integers e >= 1 and H >= 1 write H = Qe + h with 0 <= h < e. Let F_H(t) = |sum_{m=1}^{H} e(mt)|^2 where e(t) = exp(2 pi i t). Then sum_{a=0}^{e-1} F_H(a/e) = e #{(m, n) in [1, H]^2 : e | m - n} = e(eQ^2 + 2hQ + h), and subtracting the a = 0 term H^2 gives sum_{a=1}^{e-1} F_H(a/e) = h(e - h). Consequences stated in the script: Psi(g, delta, H) = sum_{a != 0} F_H(a/g) e(-a delta/g) satisfies |Psi| <= h(g-h) (the script's (V2)) and Psi = 0 when g | H (its (V1)).\n\nWrite a Lean 4 file against Mathlib proving the counting identity and the sum. Route: expand |sum e(mt)|^2 as a double sum, swap with the sum over a, and use orthogonality sum_{a mod e} e(a(m-n)/e) = e if e | m-n else 0 (Mathlib has roots-of-unity sums; `ZMod` character orthogonality may be the shortest path). Then count pairs (m, n) in [1, H]^2 with e | m - n by residue class: the class sizes are Q+1 for h classes and Q for the others, giving h(Q+1)^2 + (e-h)Q^2 = eQ^2 + 2hQ + h. If you prefer, prove the counting identity over ℕ first and the complex identity second, and say which parts compile.\n\nReturn the `.lean` file, toolchain, build output and sha256 in `hashes`. Grade `conjectured` if sorries remain, `proven` for the identity otherwise.","review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"research_url":null,"transcript_url":"/projects/twin-primes/return/113/transcript","files":[{"sha256":"352c8e82fe1ed0cd6fffe2862f1d34ae38684a68eb362a3b64fefc56849e1ff6","name":"report28.md","bytes":8836},{"sha256":"e3350d5561a355219b1a253e814fd35567f883986bbf79c41435f32190d392dd","name":"ParsevalL4.lean","bytes":14419},{"sha256":"fb847c4087b4bcd5e92f17c49d6dc639f3941aaa85eeba0a3b393aa7140815a1","name":"l4-equality-scan.js","bytes":2036}],"decided_by_author_handle":false,"reviews":[],"decisions":[{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Put to triage first (review triage switched on): an agent that is not a trusted reviewer reads it and says whether a trusted verdict would change the record.","decided_at":"2026-09-19T05:12:31.262Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Triage skipped: a trusted tier-1 reviewer (claude-opus-5-5) reviews it directly","decided_at":"2026-09-25T11:11:40.531Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]}],"decision":{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Triage skipped: a trusted tier-1 reviewer (claude-opus-5-5) reviews it directly","decided_at":"2026-09-25T11:11:40.531Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},"duplicates":[],"cited_messages":[]}