{"id":150,"job_id":29,"problem_id":1,"lane_id":3,"type":"formalize","user_id":1,"model":"claude-opus-5","provider":"anthropic","report_md":"# Job #29 (formalize): Fact A, Fact B and the Localized Merge Lemma of `research/LOCALIZED-GAP.md`, proved in Lean 4 against Mathlib (the lemma in a buffered form)\n\n**Caveat first.** The lemma is PROVEN in the note. The chain built on it is REFUTED in `research/OUTCOMES.md`\n(\"the localized merge chain, telescoped to level x\", 2026-08-17, as cited in the brief). This return\nformalizes the facts and the lemma. It does not reopen the chain and says nothing new about twin primes.\nConflict of interest: my person owns the repository.\n\n**Rung per claim.**\n- **Proven (Lean):**\n  - Fact A.\n  - Fact B, in two forms: separation, and at most one kill in an interval of length at most p − 2.\n  - The fold relation: folding by the next prime deletes exactly the classes {0, −2}.\n  - The Localized Merge Lemma, **with the gap bound assumed on gaps starting below Y + p**. Three forms:\n    - `localized_merge`: every such gap is shorter than p − 2;\n    - `localized_merge_M`: M(T_x, Y + p) < p − 2;\n    - `localized_merge_quarter`: M(T_x, Y + p) ≤ (p − 2)/4.\n- **Not proven:** the note's exact statement, with the hypothesis only on gaps starting below Y. The boundary\n  claim it would need (note §8, \"a fused gap starting below Y never ends above it\") is measured in the note,\n  not proved. Here it is replaced by the buffer.\n\nThe file is sorry-free and builds with no errors and no warnings. `#print axioms` on ten declarations lists\nonly `propext`, `Classical.choice` and `Quot.sound`. A negative control fails to build.\n\n## 0. Reformulation, first\n\n1. **Slots.** Slots are natural numbers r with r and r + 2 coprime to x#. `coprime_primorial_iff` proves\n   that coprime to y# is the same as having no prime factor ≤ y, i.e. the brief's x-rough.\n2. **Sorted sequence.**\n   - `next x s` is the least twin slot of T_x above s, defined with `Nat.find`. One exists because\n     (s+2)·x# ± 1 are slots.\n   - `not_isSlot_of_lt_next` shows that no slot lies strictly between s and `next x s`.\n   - I used this successor function instead of `Nat.nth`.\n3. **M and maxsum₂.** `M x Y` is the maximum of `next x s − s` over slots s < Y. `maxsum2 x Y` is the maximum\n   of `next x (next x s) − s` over slots s < Y. This is the left-endpoint rule (a) of §8, with a window\n   counted when its first gap starts below Y.\n4. **Folding.** p is the next prime after x (`p.Prime`, `x < p`, and every prime above x is ≥ p), and T_p is\n   the set of twin slots coprime to p#. `isSlot_fold` shows this is exactly T_x minus the slots with\n   p ∣ r or p ∣ r + 2. The brief's x ≥ 3 is kept; primality of x is not used.\n5. **Boundary buffer.**\n   - A new gap of T_p starting at s < Y fuses old gaps. The second of them starts at `next x s`, which can\n     be ≥ Y, where a bound on gaps starting below Y says nothing.\n   - The Lean statement therefore assumes the bound for gaps starting below Y + p.\n   - The proof uses it only at s and at `next x s`, and the latter is < s + p.\n\n## 1. Statements\n\n| Lean (namespace `LocalizedGap`) | statement |\n|---|---|\n| `coprime_primorial_iff` | `Coprime n (y#) ↔ ∀ q prime, q ≤ y → ¬ q ∣ n` |\n| **`factA`** | `3 ≤ x → IsSlot x s → ¬ IsSlot x (s + 2)` |\n| `factA_fails_at_two` | `IsSlot 2 1 ∧ IsSlot 2 3` (the bound x ≥ 3 is needed) |\n| **`isSlot_fold`** | `p.Prime → x < p → (∀ q prime, x < q → p ≤ q) → (IsSlot p r ↔ IsSlot x r ∧ ¬ (p ∣ r ∨ p ∣ r + 2))` |\n| **`factB_sep`** | `3 ≤ x →` slots `r < r'` of T_x, both killed by p `→ r + p ≤ r' + 2` (i.e. r' − r ≥ p − 2) |\n| **`factB_interval`** | `3 ≤ x → L + 2 ≤ p → #{r ∈ [a, a+L) : IsSlot x r ∧ killed by p} ≤ 1` |\n| **`localized_merge`** | the next-prime hypotheses, `3 ≤ x`, and `(∀ slot s of T_x, s < Y + p → next x s − s + 2 < p)` `→ M p Y ≤ maxsum2 x Y` |\n| `localized_merge_M` | the same with `M x (Y + p) + 2 < p` |\n| `localized_merge_quarter` | the same with `M x (Y + p) ≤ (p − 2)/4`, the note's constant |\n\n**Findings beyond the brief** (each proven in the file):\n- **Constant.** The lemma holds whenever the relevant old gaps are shorter than p − 2. The note's\n  M ≤ (p − 2)/4 is stronger than needed.\n- **Fact B separation** needs no bound on p. The case r' = r + 1 closes without one.\n\n## 2. Proof route, as formalized\n\n- **Fact A.** s, s + 2 and s + 4 cover every class mod 3, and 3 ≤ x. The last step is `omega`.\n- **Fact B.** Split into the four class cases for two kills r < r'. Each is a divisibility gap\n  (p ∣ A, p ∣ B, A < B ⟹ A + p ≤ B). The case r ≡ −2, r' ≡ 0 with r' = r + 2 is exactly Fact A. The\n  interval form follows from `Finset.card_le_one`.\n- **The lemma.** This route is shorter than the note's partition count, and I have not formalized the\n  note's argument. Take a slot s < Y of T_p, and let u₁ = next x s and u₂ = next x u₁.\n  - If u₁ survives the fold, the next T_p slot after s is at most u₁ < u₂.\n  - If u₁ is killed, then u₂ is not. Otherwise Fact B gives u₂ − u₁ ≥ p − 2, against the hypothesis at u₁.\n    The hypothesis applies there because u₁ < s + p < Y + p.\n  - Either way the new gap is at most u₂ − s, a two-gap window starting below Y, so it is ≤ maxsum₂(T_x, Y).\n\n**Trying to break it.** The checks table evaluates the definitions at x = 3, 5, 7, 11, 13 with p the next\nprime.\n- The M values are 6, 12, 30, 42, 66, the G₂ ladder of `research/G2-STATE.md` §2.\n- The hypothesis fails at all five levels, as §3 of the note predicts for small x.\n- Without the hypothesis the conclusion fails at (x, p, Y) = (5, 7, 500), where M(T_7) = 30 > maxsum₂(T_5)\n  = 24, and at (13, 17, 3000), where 108 > 96. So the hypothesis is doing work.\n- I found no instance where the hypothesis holds and the conclusion fails. The proof rules one out.\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, #89 and #113.\n- **Build.** `lake env lean LocalizedGap.lean` exits 0 in 15.9 s wall on an Apple M1, with no output. The\n  file is `LocalizedGap.lean`, 213 lines, sha256\n  `5438264261ed1e70e230895ac6665f2a5ba129fa491566863b9666edf4ffcaa1`, and `grep -c sorry` returns 0.\n- **Iterations.** Two builds:\n  1. an unknown constant, `Nat.dvd_sub'` (in this core `Nat.dvd_sub` takes the two divisibility\n     hypotheses), and a warning that `factB_sep`'s `2 ≤ p` was unused, so I removed it;\n  2. clean.\n- **Checks.** Ten axiom lines, all standard. The level table is the one above. `next 5` iterated from 0\n  gives 11, 17, 29, 41, 47, 59, the slots mod 30 and their shift by 30.\n- **Negative control.** In a copy, `factA`'s `3 ≤ x` was changed to `2 ≤ x`. The build exits 1, where 3 ≤ x\n  is used and at the call in `factB_sep`. That variant is false, by `factA_fails_at_two`.\n\n**Files.** `LocalizedGap.lean` and this report are uploaded. The checks tail, the logs and the manifest pins\nare inline in the recipe, with their sha256 values in `hashes`.\n\n## Sources\n\n- `research/LOCALIZED-GAP.md`, snapshot `main`, sha256 `d4fd6ccc10b72954b3527fcb411764945ea1a426d56de1e7cff5063f73a48b85`:\n  §2 (Facts A and B), §3 (the lemma and its proof), §8 (the boundary question), and §9 (attribution to\n  Holt and Rudd 2014, arXiv:1408.6002 Lemma 3.1, as the note cites it; not consulted by me).\n- `research/OUTCOMES.md` (closed route, 2026-08-17), as cited in the brief.\n- `research/G2-STATE.md` §2 (ladder values G₂ = 6, 12, 30, 42, 66), snapshot `main`, read in job #26.\n- Mathlib at the commit above: `Nat.Prime.dvd_primorial_iff`, `primorial_pos`, `primorial_two`,\n  `Nat.coprime_of_dvd`, `Nat.Coprime.coprime_dvd_left`, `Nat.Coprime.eq_one_of_dvd`, `Nat.dvd_sub`,\n  `Nat.le_of_dvd`, `Nat.find`, `Finset.card_le_one`, `Finset.sup_le`, `Finset.le_sup`.\n\nNo local-only sources.\n\n**Transcript:** from the GET /start that received job #29 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":{"LocalizedGap.lean":"5438264261ed1e70e230895ac6665f2a5ba129fa491566863b9666edf4ffcaa1","lg-build.log (inline in recipe)":"abe480ddc86fedd4ae7ddd652bb707d1342d937547fc0c62e4cc58bb29a79c0f","lg-checks.log (inline in recipe)":"ad80a5beafadeac0e80dcaf8d3ef8a4ace967d86b1db554850a2b59337b92cd2","lean-toolchain (inline in recipe)":"3aac669c7a910ec2389f4e4f921b605adf6ebf2d1e0c9b9cd0be4d33f3f5db71","lg-negative.log (inline in recipe)":"02804d2dd81ea8e55e6a4479048439a702dfec3f002d2fd6e7e6c76ebe17dd13","LGChecksTail.lean (inline in recipe)":"565e078c06e1323c4433c4b67e9760005a714896afcb2c4e157e66fc08458a66","lake-manifest.json (pins inline in recipe)":"713e3b169ede20be0a2767072005a84a3527c83b748a9420ab769b8e8cd8f278"},"author_rung":"proven","status":"pending","final_rung":null,"created_at":"2026-09-11T16:25:44.723Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[],"messages":[]},"tokens":{"log":"claude-code","input":226,"models":{"<synthetic>":0,"claude-opus-5":50255},"output":50255,"source":"claude-jsonl","entries":9,"cache_read":2650819,"cache_write":58455},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe, job #29 (Lean 4 + Mathlib cache; about 20-35 seconds per build once the cache is present, three builds)\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 `LocalizedGap.lean` (sha256 `5438264261ed1e70e230895ac6665f2a5ba129fa491566863b9666edf4ffcaa1`) and run `/usr/bin/time -p lake env lean LocalizedGap.lean > lg-build.log 2>&1`.\n   Expected: exit 0, and no Lean output (the log holds only the three timing lines), about 16 s on an Apple M1. `grep -c sorry LocalizedGap.lean` prints 0.\n3. Checks: `cat LocalizedGap.lean LGChecksTail.lean > LocalizedGapChecks.lean` with the tail below, then\n   `lake env lean LocalizedGapChecks.lean > lg-checks.log 2>&1; echo \"exit $?\" >> lg-checks.log`.\n   Expected: the log below. It has ten axiom lines with no `sorryAx`, a table of (x, p, Y, M(T_x,Y+p), p-2, hypothesis, M(T_p,Y), maxsum2(T_x,Y), conclusion)\n   at five small levels, where the hypothesis fails everywhere and the conclusion fails at (5,7,500) and (13,17,3000), and the slots 11, 17, 29, 41, 47, 59 of T_5. Exit 0.\n4. Negative control: in a copy `LocalizedGapNeg.lean`, change `theorem factA {x s : ℕ} (hx : 3 ≤ x)` to `(hx : 2 ≤ x)`, then\n   `lake env lean LocalizedGapNeg.lean > lg-negative.log 2>&1; echo \"exit $?\" >> lg-negative.log`. Expected: exit 1, with the log below.\n   That variant is false, not merely unproved: `factA_fails_at_two` shows 1 and 3 are both twin slots of T_2.\n\nWhat reviewers should check by eye:\n- the definitions `IsSlot`, `Kill`, `next`, `M` and `maxsum2` (lines 36-39 and 144-162);\n- the statements of `factA`, `isSlot_fold`, `factB_sep`, `factB_interval` and `localized_merge` / `_M` / `_quarter` against `research/LOCALIZED-GAP.md` §2-§3;\n- the stated reformulation: the gap bound is assumed on gaps starting below Y + p, not below Y.\n\n## LocalizedGap.lean (full text)\n\n```lean\nimport Mathlib\n\n/-!\n# Fact A, Fact B and the Localized Merge Lemma of `research/LOCALIZED-GAP.md`\n\nJob #29 (formalize). The lemma is PROVEN in the note. The chain built on it is REFUTED\n(`research/OUTCOMES.md`, \"the localized merge chain, telescoped to level x\", 2026-08-17). Formalizing the\nlemma does not reopen that chain.\n\n**Reformulation, stated first.**\n* Twin slots are natural numbers `r` with `r` and `r + 2` coprime to `x#`. `coprime_primorial_iff` shows\n  that coprime to `x#` is the same as `x`-rough, i.e. no prime factor `≤ x`.\n* `next x s` is the least twin slot of `T_x` above `s` (`Nat.find`; one exists by periodicity).\n  `not_isSlot_of_lt_next` shows that no slot lies strictly between, so `s ↦ next x s` is the sorted\n  successor.\n* `M x Y` is the maximum of `next x s − s` over slots `s < Y`. `maxsum2 x Y` is the maximum of\n  `next x (next x s) − s` over slots `s < Y`. This is the left-endpoint rule (a) of §8, applied to a\n  window's first gap.\n* `T_p` is `T_x` folded by `p`, for `p` the next prime after `x` (`isSlot_fold`). `x ≥ 3`; primality of\n  `x` is not used.\n* **Boundary.** The hypothesis is placed on gaps starting below `Y + p`, not below `Y`. A new gap starting\n  below `Y` fuses old gaps whose later members can start at or above `Y`. The note's §8 settles this\n  empirically, so here it is assumed.\n* **Constant.** `localized_merge` needs only that those old gaps are shorter than `p − 2`.\n  `localized_merge_quarter` is the note's `M ≤ (p − 2)/4` form, on the same buffered range.\n* **Route.** This differs from the note's partition count. By Fact B, two consecutive old slots cannot\n  both be killed when their gap is below `p − 2`. So the next `T_p` slot after `s` is at most the second\n  `T_x` successor of `s`.\n-/\n\nopen Finset\n\nnamespace LocalizedGap\n\n/-- `r` is a twin slot of `T_x`: `r` and `r + 2` are both coprime to `x#`. -/\nabbrev IsSlot (x r : ℕ) : Prop := Nat.Coprime r (primorial x) ∧ Nat.Coprime (r + 2) (primorial x)\n\n/-- `r` is killed by the fold by `p`: `r ≡ 0` or `r ≡ −2 (mod p)`. -/\nabbrev Kill (p r : ℕ) : Prop := p ∣ r ∨ p ∣ r + 2\n\n/-- Coprime to `y#` is the same as `y`-rough. -/\ntheorem coprime_primorial_iff (n y : ℕ) :\n    Nat.Coprime n (primorial y) ↔ ∀ q, q.Prime → q ≤ y → ¬ q ∣ n := by\n  constructor\n  · intro h q hq hqy hqn\n    have h1 : Nat.Coprime q (primorial y) := Nat.Coprime.coprime_dvd_left hqn h\n    exact hq.one_lt.ne' (h1.eq_one_of_dvd (hq.dvd_primorial_iff.2 hqy))\n  · intro h\n    apply Nat.coprime_of_dvd\n    intro k hk hkn hkP\n    exact h k hk (hk.dvd_primorial_iff.1 hkP) hkn\n\n/-! ## Fact A -/\n\n/-- **Fact A.** For `x ≥ 3`, no two twin slots of `T_x` are 2 apart. -/\ntheorem factA {x s : ℕ} (hx : 3 ≤ x) (hs : IsSlot x s) : ¬ IsSlot x (s + 2) := by\n  intro hs2\n  have h3 : ∀ n, Nat.Coprime n (primorial x) → ¬ 3 ∣ n := fun n hn =>\n    (coprime_primorial_iff n x).1 hn 3 Nat.prime_three hx\n  have a := h3 s hs.1\n  have b := h3 (s + 2) hs.2\n  have c := h3 (s + 2 + 2) hs2.2\n  omega\n\n/-- The bound `x ≥ 3` is needed: `1` and `3` are both twin slots of `T_2`. -/\ntheorem factA_fails_at_two : IsSlot 2 1 ∧ IsSlot 2 3 := by\n  simp only [IsSlot, primorial_two]\n  decide\n\n/-! ## Fact B -/\n\n/-- Folding by the next prime `p` deletes exactly the slots in the classes `{0, −2} mod p`. -/\ntheorem isSlot_fold {x p r : ℕ} (hp : p.Prime) (hxp : x < p) (hnext : ∀ q, q.Prime → x < q → p ≤ q) :\n    IsSlot p r ↔ IsSlot x r ∧ ¬ Kill p r := by\n  have key : ∀ n, Nat.Coprime n (primorial p) ↔ Nat.Coprime n (primorial x) ∧ ¬ p ∣ n := by\n    intro n\n    rw [coprime_primorial_iff, coprime_primorial_iff]\n    constructor\n    · intro h\n      exact ⟨fun q hq hqx => h q hq (by omega), h p hp le_rfl⟩\n    · rintro ⟨h, hpn⟩ q hq hqp\n      rcases Nat.lt_or_ge x q with hxq | hqx\n      · have hqeq : q = p := le_antisymm hqp (hnext q hq hxq)\n        rw [hqeq]\n        exact hpn\n      · exact h q hq hqx\n  simp only [IsSlot, Kill, key, not_or]\n  tauto\n\nlemma add_le_of_dvd_of_lt {p A B : ℕ} (hA : p ∣ A) (hB : p ∣ B) (h : A < B) : A + p ≤ B := by\n  have := Nat.le_of_dvd (by omega) (Nat.dvd_sub hB hA)\n  omega\n\n/-- **Fact B**, separation form: two killed twin slots `r < r'` of `T_x` satisfy `r' − r ≥ p − 2`. -/\ntheorem factB_sep {x p r r' : ℕ} (hx : 3 ≤ x) (hr : IsSlot x r) (hr' : IsSlot x r')\n    (hk : Kill p r) (hk' : Kill p r') (hlt : r < r') : r + p ≤ r' + 2 := by\n  rcases hk with h | h <;> rcases hk' with h' | h'\n  · have := add_le_of_dvd_of_lt h h' hlt\n    omega\n  · have := add_le_of_dvd_of_lt h h' (by omega : r < r' + 2)\n    omega\n  · rcases Nat.lt_trichotomy (r + 2) r' with h2 | h2 | h2\n    · have := add_le_of_dvd_of_lt h h' h2\n      omega\n    · have hr2 : IsSlot x (r + 2) := by rw [h2]; exact hr'\n      exact absurd hr2 (factA hx hr)\n    · have := add_le_of_dvd_of_lt h' h h2\n      omega\n  · have := add_le_of_dvd_of_lt h h' (by omega : r + 2 < r' + 2)\n    omega\n\n/-- **Fact B**, interval form: an interval `[a, a + L)` with `L ≤ p − 2` contains at most one kill. -/\ntheorem factB_interval {x p a L : ℕ} (hx : 3 ≤ x) (hL : L + 2 ≤ p) :\n    ((Ico a (a + L)).filter (fun r => IsSlot x r ∧ Kill p r)).card ≤ 1 := by\n  rw [Finset.card_le_one]\n  intro r hr r' hr'\n  simp only [Finset.mem_filter, Finset.mem_Ico] at hr hr'\n  by_contra hne\n  rcases Nat.lt_or_gt_of_ne hne with h | h\n  · have := factB_sep hx hr.2.1 hr'.2.1 hr.2.2 hr'.2.2 h\n    omega\n  · have := factB_sep hx hr'.2.1 hr.2.1 hr'.2.2 hr.2.2 h\n    omega\n\n/-! ## The sorted slot sequence, `M` and `maxsum₂` -/\n\ntheorem exists_slot_gt (x s : ℕ) : ∃ t, s < t ∧ IsSlot x t := by\n  have hP : 1 ≤ primorial x := primorial_pos x\n  have hK : s + 2 ≤ (s + 2) * primorial x := by nlinarith\n  refine ⟨(s + 2) * primorial x - 1, by omega, ?_, ?_⟩\n  · apply Nat.coprime_of_dvd\n    intro k hk h1 h2\n    have h3 : k ∣ (s + 2) * primorial x := Dvd.dvd.mul_left h2 _\n    have h4 := Nat.dvd_sub h3 h1\n    rw [show (s + 2) * primorial x - ((s + 2) * primorial x - 1) = 1 by omega] at h4\n    exact hk.one_lt.ne' (Nat.dvd_one.mp h4)\n  · apply Nat.coprime_of_dvd\n    intro k hk h1 h2\n    have h3 : k ∣ (s + 2) * primorial x := Dvd.dvd.mul_left h2 _\n    have h4 := Nat.dvd_sub h1 h3\n    rw [show (s + 2) * primorial x - 1 + 2 - (s + 2) * primorial x = 1 by omega] at h4\n    exact hk.one_lt.ne' (Nat.dvd_one.mp h4)\n\n/-- The next twin slot of `T_x` above `s`. -/\ndef next (x s : ℕ) : ℕ := Nat.find (exists_slot_gt x s)\n\ntheorem lt_next (x s : ℕ) : s < next x s := (Nat.find_spec (exists_slot_gt x s)).1\n\ntheorem isSlot_next (x s : ℕ) : IsSlot x (next x s) := (Nat.find_spec (exists_slot_gt x s)).2\n\ntheorem next_le {x s t : ℕ} (h : s < t) (ht : IsSlot x t) : next x s ≤ t :=\n  Nat.find_min' _ ⟨h, ht⟩\n\n/-- `next x s` is the successor: no twin slot lies strictly between `s` and `next x s`. -/\ntheorem not_isSlot_of_lt_next {x s t : ℕ} (h1 : s < t) (h2 : t < next x s) : ¬ IsSlot x t :=\n  fun ht => absurd (next_le h1 ht) (by omega)\n\n/-- `M(T_x, Y)`: the largest gap between consecutive twin slots of `T_x` among gaps starting below `Y`. -/\ndef M (x Y : ℕ) : ℕ := ((range Y).filter (IsSlot x)).sup fun s => next x s - s\n\n/-- `maxsum₂(T_x, Y)`: the largest sum of two consecutive gaps of `T_x`, the first starting below `Y`. -/\ndef maxsum2 (x Y : ℕ) : ℕ := ((range Y).filter (IsSlot x)).sup fun s => next x (next x s) - s\n\n/-! ## The Localized Merge Lemma -/\n\n/-- **Localized Merge Lemma**, gap form. If every gap of `T_x` starting below `Y + p` is shorter than\n`p − 2`, then `M(T_p, Y) ≤ maxsum₂(T_x, Y)`. -/\ntheorem localized_merge {x p Y : ℕ} (hx : 3 ≤ x) (hp : p.Prime) (hxp : x < p)\n    (hnext : ∀ q, q.Prime → x < q → p ≤ q)\n    (hgap : ∀ s, IsSlot x s → s < Y + p → next x s - s + 2 < p) :\n    M p Y ≤ maxsum2 x Y := by\n  unfold M\n  refine Finset.sup_le fun s hs => ?_\n  show next p s - s ≤ maxsum2 x Y\n  rw [Finset.mem_filter, Finset.mem_range] at hs\n  obtain ⟨hsY, hsp⟩ := hs\n  have hsx : IsSlot x s := ((isSlot_fold hp hxp hnext).1 hsp).1\n  have hwin : next x (next x s) - s ≤ maxsum2 x Y :=\n    Finset.le_sup (f := fun s => next x (next x s) - s)\n      (by rw [Finset.mem_filter, Finset.mem_range]; exact ⟨hsY, hsx⟩)\n  have h1 := lt_next x s\n  have h2 := lt_next x (next x s)\n  by_cases hk : Kill p (next x s)\n  · have hk2 : ¬ Kill p (next x (next x s)) := by\n      intro hk2\n      have hsep := factB_sep hx (isSlot_next x s) (isSlot_next x (next x s)) hk hk2 h2\n      have hg1 := hgap s hsx (by omega)\n      have hg2 := hgap (next x s) (isSlot_next x s) (by omega)\n      omega\n    have hslot2 : IsSlot p (next x (next x s)) := (isSlot_fold hp hxp hnext).2 ⟨isSlot_next x _, hk2⟩\n    have := next_le (by omega : s < next x (next x s)) hslot2\n    omega\n  · have hslot1 : IsSlot p (next x s) := (isSlot_fold hp hxp hnext).2 ⟨isSlot_next x s, hk⟩\n    have := next_le h1 hslot1\n    omega\n\n/-- **Localized Merge Lemma**, `M` form: `M(T_x, Y + p) < p − 2` implies `M(T_p, Y) ≤ maxsum₂(T_x, Y)`. -/\ntheorem localized_merge_M {x p Y : ℕ} (hx : 3 ≤ x) (hp : p.Prime) (hxp : x < p)\n    (hnext : ∀ q, q.Prime → x < q → p ≤ q) (hM : M x (Y + p) + 2 < p) :\n    M p Y ≤ maxsum2 x Y := by\n  refine localized_merge hx hp hxp hnext fun s hs hsY => ?_\n  have hle : next x s - s ≤ M x (Y + p) :=\n    Finset.le_sup (f := fun s => next x s - s) (by rw [Finset.mem_filter, Finset.mem_range]; exact ⟨hsY, hs⟩)\n  omega\n\n/-- **Localized Merge Lemma**, the note's form on the buffered range: `M(T_x, Y + p) ≤ (p − 2)/4`. -/\ntheorem localized_merge_quarter {x p Y : ℕ} (hx : 3 ≤ x) (hp : p.Prime) (hxp : x < p)\n    (hnext : ∀ q, q.Prime → x < q → p ≤ q) (hM : M x (Y + p) ≤ (p - 2) / 4) :\n    M p Y ≤ maxsum2 x Y := by\n  refine localized_merge_M hx hp hxp hnext ?_\n  omega\n\nend LocalizedGap\n```\n\n## LGChecksTail.lean (appended to a copy of LocalizedGap.lean for step 3; sha256 `565e078c06e1323c4433c4b67e9760005a714896afcb2c4e157e66fc08458a66`)\n\n```lean\n/-! ## Checks (appended to a copy of `LocalizedGap.lean`; not part of the proof file) -/\n\n#print axioms LocalizedGap.coprime_primorial_iff\n#print axioms LocalizedGap.factA\n#print axioms LocalizedGap.factA_fails_at_two\n#print axioms LocalizedGap.isSlot_fold\n#print axioms LocalizedGap.factB_sep\n#print axioms LocalizedGap.factB_interval\n#print axioms LocalizedGap.not_isSlot_of_lt_next\n#print axioms LocalizedGap.localized_merge\n#print axioms LocalizedGap.localized_merge_M\n#print axioms LocalizedGap.localized_merge_quarter\n\n-- (x, p, Y, M(T_x, Y+p), p-2, hypothesis M(T_x, Y+p) + 2 < p, M(T_p, Y), maxsum2(T_x, Y), M(T_p, Y) ≤ maxsum2(T_x, Y))\n-- At small x the hypothesis fails; this only shows the objects compute as defined.\n#eval [(3, 5, 500), (5, 7, 500), (7, 11, 2000), (11, 13, 2000), (13, 17, 3000)].map fun (x, p, Y) =>\n  (x, p, Y, LocalizedGap.M x (Y + p), p - 2, decide (LocalizedGap.M x (Y + p) + 2 < p),\n   LocalizedGap.M p Y, LocalizedGap.maxsum2 x Y, decide (LocalizedGap.M p Y ≤ LocalizedGap.maxsum2 x Y))\n\n-- The first twin slots of T_5 (mod 30: 11, 17, 29) read through `next`.\n#eval (List.range 6).foldl (fun acc _ => acc ++ [LocalizedGap.next 5 (acc.getLast?.getD 0)]) ([] : List ℕ)\n```\n\n## Build output (lg-build.log, sha256 `abe480ddc86fedd4ae7ddd652bb707d1342d937547fc0c62e4cc58bb29a79c0f`)\n\n```\nreal 15.85\nuser 3.24\nsys 11.44\n```\n\n## Checks (lg-checks.log, sha256 `ad80a5beafadeac0e80dcaf8d3ef8a4ace967d86b1db554850a2b59337b92cd2`)\n\n```\n'LocalizedGap.coprime_primorial_iff' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.factA' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.factA_fails_at_two' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.isSlot_fold' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.factB_sep' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.factB_interval' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.not_isSlot_of_lt_next' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.localized_merge' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.localized_merge_M' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LocalizedGap.localized_merge_quarter' depends on axioms: [propext, Classical.choice, Quot.sound]\n[(3, 5, 500, 6, 3, false, 12, 12, true), (5, 7, 500, 12, 5, false, 30, 24, false),\n  (7, 11, 2000, 30, 9, false, 42, 42, true), (11, 13, 2000, 42, 11, false, 66, 66, true),\n  (13, 17, 3000, 66, 15, false, 108, 96, false)]\n[11, 17, 29, 41, 47, 59]\nexit 0\n```\n\n## Negative control, full log (lg-negative.log, sha256 `02804d2dd81ea8e55e6a4479048439a702dfec3f002d2fd6e7e6c76ebe17dd13`)\n\n```\nLocalizedGapNeg.lean:59:55: error: Application type mismatch: The argument\n  hx\nhas type\n  2 ≤ x\nbut is expected to have type\n  3 ≤ x\nin the application\n  (coprime_primorial_iff n x).mp hn 3 Nat.prime_three hx\nLocalizedGapNeg.lean:106:30: error: Application type mismatch: The argument\n  hx\nhas type\n  3 ≤ x\nbut is expected to have type\n  2 ≤ x\nin the application\n  factA hx\nexit 1\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":13},"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-11T16:25:44.747Z","department_id":null,"run_id":null,"triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"Register per `CLAUDE.md`. The lemma is PROVEN; the chain built on it is REFUTED in `research/OUTCOMES.md` (\"the localized merge chain, telescoped to level x\", 2026-08-17). Formalizing the lemma does not reopen the chain and should not be described as doing so.\n\nStatements (`research/LOCALIZED-GAP.md` sections 2 and 3). Fix a prime x >= 3 and let T_x be the set of twin slots: integers r with r and r+2 both x-rough (no prime factor <= x). Fact A: no two twin slots of T_x are 2 apart (s, s+2, s+4 all x-rough would cover every class mod 3). Fact B: folding T_x by a prime p > x deletes exactly the slots in the classes {0, -2} mod p; in an interval shorter than p-2, at most one slot is deleted. Localized Merge Lemma: write M(T_x, Y) for the largest gap between consecutive twin slots among gaps starting below Y, and maxsum_2(T_x, Y) for the largest sum of two consecutive such gaps; if M(T_x, Y) <= (p-2)/4 then M(T_p, Y) <= maxsum_2(T_x, Y), where T_p is T_x after folding by p (assume p is the next prime after x, or state the weaker hypothesis you use).\n\nWrite a Lean 4 file against Mathlib proving Fact A, Fact B and the lemma. The proof of the lemma is a counting argument: a new gap G fusing j+1 old gaps contains j kills, G <= (j+1)M; if G >= p-2, partition into ceil(G/(p-2)) subintervals shorter than p-2 to get j <= G/(p-2) + 1, then G(1 - M/(p-2)) <= 2M, contradiction with M <= (p-2)/4. Formalizing \"consecutive gaps starting below Y\" requires a definition of the sorted slot sequence; use `Nat.nth` on the predicate or a `Finset` sorted list, and state the boundary convention (the note's section 8 says a fused gap starting below Y never ends above it; you may need to assume or prove a version of this).\n\nReturn the `.lean` file, toolchain, build output and sha256 in `hashes`. If the statement needed reformulation, put the reformulation first. Grade `conjectured` if any sorry remains.","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/150/transcript","files":[{"sha256":"0bc6f2c24b4080324e6e935b4242068b902d8ccadabfe4f971040b5445ee347f","name":"report29.md","bytes":8103},{"sha256":"5438264261ed1e70e230895ac6665f2a5ba129fa491566863b9666edf4ffcaa1","name":"LocalizedGap.lean","bytes":9881}],"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":[]}