{"id":5411,"job_id":10823,"problem_id":1,"lane_id":null,"type":"explore","user_id":103,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Statement map of the G2 lower-bound Lean proof (return #2597)\n\nItem 5 of the outside expert's round 2 agenda (`research/expert-review/2026-10-22-round2.md`, line 620), the part that needs no fresh build: do the three mapped declarations of kk-lower-bound mean what its prose says, at the real cutoff, the integer gap, the quantifier order and the constant? Read and run on 2026-10-22 by the `audit-statement-map` lane.\n\n## Result\n\n**All three mapped declarations match their prose claims, and the match is now checked by Lean, not only read.** `PrimaryMain.manuscript_main_goal` says: there are a real c > 0 and a real y0 such that for every real y ≥ y0, c · y(log y)^3(log log log y)^2/(log log y)^4 ≤ G2(P(y)), where P(y) is the product of the primes p ≤ y (real comparison) and G2 is the largest distance between consecutive integers n with gcd(n(n+2), P(y)) = 1. That is equation (1) of `inputs/manuscript.md` and of `inputs/kk-lower-bound.revised.md`, with the project's G2 from `research/lane-common/common.md`. `IntegerMainBinding.integer_maximum_binding` says that for every finite set S of primes this finite G2 is attained at some integer start and bounds every consecutive gap at every integer start. `IntegerMainBinding.manuscript_integer_main_goal` is Theorem 1 of `manuscript.md` clause for clause and does not mention G2.\n\n`statement-map/checks/Unfold.lean` restates each mapped type with every authored definition replaced by its body, down to `Real.log`, `Nat.floor`, `Finset.range`/`filter`/`Icc`/`sup`/`prod`, `Nat.Prime`, `Nat.gcd` and `Int.gcd`, and Lean accepts each restatement, by `rfl`, `Iff.rfl`, a one-line rewrite, or the mapped proof itself. The same file re-runs the proof with c fixed: c = 1/chooseB(12), written out in numerals, `exp` and `log`, with log10 chooseB(12) = 8615.5487, so c ≈ 10^-8615.55. That agrees with #5316. The mapped statement asserts only \"∃ c > 0\", so the value is a property of the proof, not of the statement. The threshold y0 is not numeric: it is a maximum that includes three thresholds from existential growth lemmas.\n\nFourteen mutants that change the cutoff, the gap definition, the quantifiers, the shape or the logarithm base each fail to typecheck against the mapped proof, with a type mismatch at the proof term. A fifteenth, M14 (the constant doubled), is checked against this lane's own explicit-constant proof in `checks/Unfold.lean`, not against a mapped declaration: it shows 2/chooseB(12) is not that proof's constant. Two mutants that add an axiom (`axiom`, `sorry`) compile, and `#print axioms` lists the extra axiom (`smuggled`, `sorryAx`). Three source-level mutants, which edit a definition inside the package and rebuild all 38 modules, break the build: a √y cutoff breaks the lemma `mem_mainPrimes`, and if that lemma is edited to match, it breaks `PrimaryMain.lean:43`, where the completion bound for `G2 (primeCutoff y)` no longer casts to the mutated family. A one-class survivor predicate breaks `Arithmetic.lean`. The one hypothesis carried as an argument, `PrimeFamily S`, is needed: without it the binding is false at S = {0} (`checks/PrimeFamilyNeeded.lean`). O1 to O7 stay outside every mapped statement.\n\nThis agrees with `BINDING.md` Part 1 (does-lean-kk lane, 2026-10-21) on every entry. I did the unfolding before I opened `BINDING.md`. What this file adds is the kernel-checked restatements, the constant witness, the mutants and the `PrimeFamily` counterexample. It does not add a second human reading of the manuscript: one referee (this lane) wrote the plain-mathematics text below, and Lean checks that the Lean restatements equal the mapped types, not that the English equals the Lean.\n\n## Sources and environment\n\n- Lean sources: `inputs/*.lean`, the bytes REPLAY.md built (38 files, `inputs/MANIFEST.sha256`). Every Lean line quoted here is from those files at the line given. The definitions table joins a multi-line definition onto one line, with `;` where the source has a line break inside a tactic block.\n- Prose: `inputs/manuscript.md` (the paper of record for #2597, sha256 `6c287c18…8e80` per `BINDING.md`), Abstract lines 11-23 and Theorem 1 at lines 40-46; `inputs/kk-lower-bound.revised.md`, equations (1) and (2) at lines 19-60, which the `statement-bundle.json` locators cite.\n- Project G2: `research/lane-common/common.md` line 5 and `research/ladder/results.md` line 3.\n\nThe replay environment of REPLAY.md is gone: its `.elan/` and `project/.lake/` were gitignored and left with that worktree. So I rebuilt a private copy in `statement-map/env/` (gitignored), with every step under `nice -n 10`:\n\n| step | command | time |\n|---|---|---|\n| sources | `scripts/setup_env.sh` copies the 38 files from `inputs/` and checks them against `statement-map/env-sha256.txt`: 38 OK (`logs/07-env-sources-sha.log`) | <1 s |\n| toolchain | elan into `statement-map/.elan`, `leanprover/lean4:v4.35.0-rc3`, commit `470d5ce1…`, the pinned one | not timed |\n| Mathlib | `lake exe cache get` resolved Mathlib at `331d5244…`. The manifest is unchanged. It decompressed 9000 files already in the local Mathlib cache, the files REPLAY.md downloaded from cache.mathlib.org on 2026-10-17 (`logs/01-cache-get.log`) | 1 min 31 s |\n| build | `scripts/build_seq.sh`: one `lake build <Module>` at a time in import order, `LEAN_NUM_THREADS=4`, so at most one Lean process runs; 38 of 38 \"Build completed successfully\" (`logs/02-build-seq.log`) | 3 min 6 s |\n\nThis is not the fresh rebuild the expert schedules for later. Mathlib's oleans are Mathlib's CI objects from a local cache, no `leanchecker` ran, and no second kernel ran. It only gives each check below an environment to elaborate in. The author's objects were not used.\n\n## The definitions, unfolded\n\nEvery name the three statements use, from the authored files down to Mathlib and core. \"Kernel\" in the last column names the `checks/Unfold.lean` example that Lean accepts for that row.\n\n| Lean (file:line, verbatim) | Plain mathematics | Kernel |\n|---|---|---|\n| `def mainPrimes (y : ℝ) : Finset ℕ := primeCutoff y` (SieveParameters.lean:185) and `def primeCutoff (z : ℝ) : Finset ℕ := (Finset.range (⌊z⌋₊ + 1)).filter Nat.Prime` (ManuscriptResidues.lean:23) | S_y = {p ∈ ℕ : p prime, p ≤ ⌊y⌋} = {p prime : p ≤ y} for y ≥ 0 (`mem_mainPrimes`, SieveParameters.lean:187). Empty for y < 2. | `mainPrimes y = (Finset.range (⌊y⌋₊ + 1)).filter Nat.Prime := rfl` |\n| `def PrimeFamily (S : Finset Nat) : Prop := ∀ p ∈ S, Nat.Prime p` (FiniteCoreTargets.lean:22) | S is a finite set of primes, ∅ allowed | used verbatim in claim 2 |\n| `def period (S : Finset Nat) : Nat := ∏ p ∈ S, p` (:25) | P_S = ∏_{p∈S} p; P_{S_y} = P(y), which is x# at x = ⌊y⌋ | inside the rows below |\n| `def Survivor (S : Finset Nat) (n : Nat) : Prop := Nat.gcd (n * (n + 2)) (period S) = 1` (:28) | n ≥ 0 is admissible: gcd(n(n+2), P_S) = 1 | inside `cyclicGapDistances` row |\n| `def IntSurvivor (S : Finset Nat) (n : Int) : Prop := Int.gcd (n * (n + 2)) (period S : Int) = 1` (:32) | n ∈ ℤ is admissible; `Int.gcd` is the gcd of absolute values | `IntConsecutive` row |\n| `def IntConsecutive (S : Finset Nat) (s : Int) (d : Nat) : Prop := 0 < d ∧ IntSurvivor S s ∧ IntSurvivor S (s + (d : Int)) ∧ ∀ i : Nat, 0 < i → i < d → ¬ IntSurvivor S (s + (i : Int))` (:58) | s and s + d are consecutive admissible integers at distance d ≥ 1 | `IntConsecutive S s d ↔ (0 < d ∧ Int.gcd (s * (s + 2)) ((∏ p ∈ S, p : ℕ) : ℤ) = 1 ∧ …) := Iff.rfl` |\n| `Consecutive` (:54), the same over `Nat` | the same for s ≥ 0 | inside next row |\n| `def cyclicGapDistances (S : Finset Nat) : Finset Nat := by classical; exact (Finset.Icc 1 (period S)).filter (fun d => ∃ s ∈ Finset.range (period S), Consecutive S s d)` (:64) | {d ∈ [1, P_S] : some s ∈ [0, P_S) has s, s + d consecutive admissible}. s + d may pass P_S, so the gap across the period boundary counts. | membership `↔ d ∈ Finset.Icc 1 (∏ p ∈ S, p) ∧ ∃ s ∈ Finset.range (∏ p ∈ S, p), 0 < d ∧ Nat.gcd (s * (s + 2)) (∏ p ∈ S, p) = 1 ∧ …`, by `rw [Finset.mem_filter]; rfl` |\n| `def G2 (S : Finset Nat) : Nat := (cyclicGapDistances S).sup id` (:72) | the largest such d; 0 if the set is empty, which never happens for a prime family (`G2_attained_and_bounds` gives 1 ≤ G2 S ≤ P_S) | `G2 S = (cyclicGapDistances S).sup id := rfl` |\n| `def mainShape (y : ℝ) : ℝ := y * (Real.log y) ^ 3 * (Real.log (Real.log (Real.log y))) ^ 2 / (Real.log (Real.log y)) ^ 4` (SieveParameters.lean:191) | y(log y)^3(log log log y)^2/(log log y)^4, natural logs; equal to the prose for y > e^e, and Mathlib's `log 0 = 0`, `log(-x) = log x`, `x/0 = 0` below that | `mainShape y = y * Real.log y ^ 3 * … := rfl` |\n\n`Finset.filter` in `cyclicGapDistances` carries the `Decidable` instance that the `classical` tactic chose, so an `rfl` restatement with a freshly elaborated filter fails on the instance, not on the mathematics. The membership form does not depend on the instance.\n\nThe G2 here is the endpoint distance: a gap of distance d has d − 1 excluded integers between its ends. `statement-map/scripts/g2_literal.py` transcribes the definition literally (survivors tested by gcd with no reduction mod P, starts in [0, P), distances in [1, P]) and gives 2, 6, 12, 30, 42, 66, 108, 150 at x = 2, 3, 5, 7, 11, 13, 17, 19. That is the G2 column of `research/ladder/results.md` (lines 453-460), and G2 − 1 is A144311. The maximum over integer starts in [−2P, P) agrees for x ≤ 13. The empty family gives G2 = 1 (`logs/04-g2-literal.log`, 3 s at one thread). This is separate code, so it checks the arithmetic of the definition, not the Lean elaboration. `BINDING.md` Appendix B ran the same comparison independently.\n\n## Declaration 1: `PrimaryMain.manuscript_main_goal` (claim `main_eq1`)\n\n**Lean** (PrimaryMain.lean:38 and SieveParameters.lean:196-198):\n\n```lean\ntheorem manuscript_main_goal : SieveParameters.ManuscriptMainGoal := by\ndef ManuscriptMainGoal : Prop :=\n  ∃ c : ℝ, 0 < c ∧ ∃ y0 : ℝ, ∀ y : ℝ, y0 ≤ y →\n    c * mainShape y ≤ (KKFiniteCoreDraft.G2 (mainPrimes y) : ℝ)\n```\n\n**Unfolded meaning.** There exist a real c > 0 and a real y0 such that for every real y ≥ y0,\n\nc · y(log y)^3(log log log y)^2/(log log y)^4 ≤ G2(P(y)),\n\nwhere P(y) = ∏_{p ≤ y} p over primes p with p ≤ y as reals, and G2(P(y)) is the largest distance between consecutive integers n with gcd(n(n+2), P(y)) = 1, the period-crossing gap included.\n\n- Real cutoff: y is real, and the family is the primes p ≤ ⌊y⌋, which equals the primes p ≤ y. The \"≤\" is inclusive, so a prime y counts.\n- Gap: distance between consecutive admissible integers (G2), not the count of excluded integers (G2 − 1). The cast `(… : ℝ)` is `Nat.cast`. The gap side has no floor.\n- Quantifier order: ∃ c, then ∃ y0, then ∀ y. c and y0 do not depend on y. The reversed order (c after y) is trivially true, because G2 ≥ 1 on every prime family. `checks/TrivialOrder.lean` proves it in eleven lines, so the mapped order is what carries the content.\n- Constant: the statement only asserts that some c exists. The proof's witness is `primaryCoefficient = 1 / chooseB 12` (PrimaryMain.lean:13). With `chooseB A = 1 + 6 * survivorConstant * A ^ 4` (ManuscriptParameters.lean:226), `survivorConstant = uniformConstant * productConstant`, `productConstant = 128 * ordinaryConstant ^ 2`, `ordinaryConstant = 4 * exp (10 * log 4)` (RealBand.lean:57-59) and `uniformConstant = 2 * exp (20 * log 4 * (512 * log 4) + 80 * log 4)` (SieveParameters.lean:14-19):\n\n  chooseB(12) = 1 + 6 · 2e^U · 2^51 · 12^4, with U = 10240 (ln 4)^2 + 80 ln 4 = 19790.2590,\n\n  so log10 chooseB(12) = 8615.548715 and c ≈ 10^-8615.55 (`scripts/constant.py`, 60-digit `Decimal`, `logs/05-constant.log`; a magnitude, not a certificate). `checks/Unfold.lean` proves `explicit_coefficient`: ∃ Y, ∀ y ≥ Y, [that expression with numerals, `Real.exp` and `Real.log`] · mainShape y ≤ G2(mainPrimes y). Axioms: `propext`, `Classical.choice`, `Quot.sound`.\n- Threshold: y0 = max(Y_smooth, `supplyThreshold`), where `supplyThreshold = max (300000^4) e` (PrimeReserveBudget.lean:16). Y_smooth (SmoothBudget.lean:130-131) is the maximum of `SmoothParameters.threshold 12 (chooseB 12)`, exp((96 · 2^22)^2) and three thresholds Y1, Y2, Y3 from the existential lemmas `SmoothLogLimit.eventual_u_log_u`, `SmoothParameters.eventual_u_growth` and `SmoothParameters.eventual_Z_growth`. I did not trace Y1 to Y3 to numbers. The statement claims no numeric onset, and neither does the prose (manuscript.md Section 8: \"We do not claim an optimized or practical numerical onset\").\n- Hypotheses: none. The type has no arguments.\n\n**Prose.** manuscript.md Abstract, (1): \"G_2(P(y)) ≫ y(log y)^3(log log log y)^2/(log log y)^4 (y → ∞)\", with P(y) the product of \"every prime at or below the real cutoff y\" and 𝒯_y = {n ∈ ℤ : gcd(n(n+2), P(y)) = 1}. kk-lower-bound.revised.md (1) is the same display, and its Section 1 defines G2(P(y)) as \"the largest distance between consecutive members of this periodic set, including the gap across a period boundary. A gap of length G therefore contains G − 1 excluded integers\", with G2(P(p_k)) − 1 = A144311(k) as its (2). The project's G2 (common.md line 5, results.md line 3) is the same object with the same convention.\n\n**Kernel check.** `SieveParameters.ManuscriptMainGoal ↔ ∃ c : ℝ, 0 < c ∧ ∃ y0 : ℝ, ∀ y : ℝ, y0 ≤ y → c * (y * Real.log y ^ 3 * Real.log (Real.log (Real.log y)) ^ 2 / Real.log (Real.log y) ^ 4) ≤ (G2 ((Finset.range (⌊y⌋₊ + 1)).filter Nat.Prime) : ℝ) := Iff.rfl`, accepted.\n\n**Verdict: matches.** One note on the prose: kk-lower-bound.revised.md derives (1) from imported analytic inputs (Kalmynin-Konyagin Lemma 1, Mertens, the prime number theorem, Hildebrand-Tenenbaum) and says \"No implied constant or numerical starting threshold is certified\". The Lean proof uses none of those inputs and fixes c. So the statement matches, while the Lean route is the finite one of manuscript.md, not the revised manuscript's.\n\n## Declaration 2: `IntegerMainBinding.integer_maximum_binding` (claim `integer_maximum`)\n\n**Lean** (IntegerMainBinding.lean:29-31):\n\n```lean\ntheorem integer_maximum_binding (S : Finset Nat) (hS : PrimeFamily S) :\n    (∃ s : Int, IntConsecutive S s (G2 S)) ∧\n    (∀ (s : Int) (d : Nat), IntConsecutive S s d → d ≤ G2 S) := by\n```\n\n**Unfolded meaning.** For every finite set S of natural numbers all of which are prime: (a) some integer s, possibly negative, has s and s + G2(S) consecutive admissible integers for P_S; (b) every pair of consecutive admissible integers s < s + d, at any integer s, has d ≤ G2(S). So G2(S) is the attained maximum of consecutive gaps over all of ℤ.\n\n- Hypothesis carried as an argument: `hS : PrimeFamily S`. It is satisfiable on the family the theorem is used at (`ReserveBudget.fullPrimeFamily y : PrimeFamily (primeCutoff y)`, checked in `checks/PrimeFamilyNeeded.lean`), and it is needed. At S = {0}, P_S = 0, `Finset.Icc 1 0` is empty, G2 {0} = 0, and no gap has 0 < 0. `binding_needs_prime_family : ¬ ∀ S : Finset ℕ, ∃ s : ℤ, IntConsecutive S s (G2 S)` is proved there, with the three standard axioms. It analyses no analytic content.\n- Empty family: PrimeFamily ∅ holds, P = 1, every integer is admissible, and G2 ∅ = 1. The prose says the same (manuscript.md Section 2: \"For the empty prime family, P_S = 1 and G_2(P_S) = 1\").\n\n**Prose.** manuscript.md Theorem 1: \"'Largest' means both that some integer start realizes distance d and that every consecutive survivor gap at every integer start has distance at most d\", and the Section 1 identification paragraph (\"Consequently every integer gap appears with the same distance in the finite collection. Conversely, an attained natural start is an integer start\").\n\n**Kernel check.** `∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → (∃ s : ℤ, IntConsecutive S s (G2 S)) ∧ (∀ (s : ℤ) (d : ℕ), IntConsecutive S s d → d ≤ G2 S) := IntegerMainBinding.integer_maximum_binding`, accepted, with `IntConsecutive` unfolded to `Int.gcd` in the row above.\n\n**Verdict: matches.**\n\n## Declaration 3: `IntegerMainBinding.manuscript_integer_main_goal` (claim `integer_main_eq1`)\n\n**Lean** (IntegerMainBinding.lean:36-41):\n\n```lean\ntheorem manuscript_integer_main_goal :\n    ∃ c : ℝ, 0 < c ∧ ∃ Y : ℝ, ∀ y : ℝ, Y ≤ y →\n      ∃ d : Nat,\n        (∃ s : Int, IntConsecutive (SieveParameters.mainPrimes y) s d) ∧\n        (∀ (s : Int) (e : Nat), IntConsecutive (SieveParameters.mainPrimes y) s e → e ≤ d) ∧\n        c * SieveParameters.mainShape y ≤ (d : ℝ) := by\n```\n\n**Unfolded meaning.** There exist a real c > 0 and a real Y such that for every real y ≥ Y there is a natural d that is attained as a consecutive admissible gap at some integer start for the primes p ≤ y, bounds every such gap at every integer start, and satisfies c · y(log y)^3(log log log y)^2/(log log y)^4 ≤ d. Conditions (attained) and (bounds every gap) determine d, so d is the largest integer gap. The statement does not contain `G2`, so it does not rest on the finite cyclic definition. The proof uses the same c and Y as declaration 1. There are no hypotheses: `PrimeFamily (mainPrimes y)` is discharged inside the proof by `ReserveBudget.fullPrimeFamily`.\n\n**Prose.** manuscript.md Theorem 1: \"There are real constants c > 0 and Y such that, for every real y ≥ Y, an attained largest integer survivor gap d ∈ ℕ exists for S = {p ∈ ℕ : p prime, p ≤ y}, where the last comparison uses the real value of p, and c y(log y)^3(log log log y)^2/(log log y)^4 ≤ d.\"\n\n**Kernel check.** The statement above with `mainPrimes y` replaced by `(Finset.range (⌊y⌋₊ + 1)).filter Nat.Prime` and `mainShape y` by its body is accepted with `IntegerMainBinding.manuscript_integer_main_goal` as its proof.\n\n**Verdict: matches.**\n\n## Mutants\n\n\"Rejected\" below means that Lean does not accept the mapped proof as a proof of the changed statement: the two types are not definitionally equal. It does not mean that the changed statement is false. Some are true: M02, M03 and M04 follow from the mapped theorem with a smaller c, and M11 is trivial (`checks/TrivialOrder.lean`). M15 is false (`checks/PrimeFamilyNeeded.lean`). The rest are false or open, and this file does not decide which. What a rejection shows is that the mapped type is sensitive to that change, so the change is not hidden behind a definition that ignores it.\n\nCommand, run from `statement-map/env` by `scripts/run_mutants.sh` (one Lean process at a time, `LEAN_NUM_THREADS=4`):\n\n```sh\nnice -n 10 lake env lean ../mutants/<file>.lean    # with ELAN_HOME=statement-map/.elan\n```\n\nEach file imports `IntegerMainBinding` (M13 also imports `Mathlib.Analysis.SpecialFunctions.Log.Base` for `Real.logb`) and changes one thing. Each log is `logs/mutants/<file>.log` and ends with the exit code. The whole set of 17 mutants and 3 checks takes 1 min 8 s (`logs/06-run-mutants.log`).\n\n| Mutant | Change (on paper) | Result |\n|---|---|---|\n| `M01_cutoff_sqrt` | family p ≤ √y (the auxiliary sieve family) instead of p ≤ y | rejected: `7:2: error: Type mismatch`, exit 1 |\n| `M02_cutoff_half` | family p ≤ y/2, dropping the reserved primes in (y/2, y] | rejected: `7:2: Type mismatch`, exit 1 |\n| `M03_cutoff_strict` | family p < y (`Finset.range ⌈y⌉₊`) instead of p ≤ y | rejected: `7:2: Type mismatch`, exit 1 |\n| `M04_gap_interior` | `G2 − 1` (excluded-integer count, the A144311 value) instead of G2 | rejected: `7:2: Type mismatch`, exit 1 |\n| `M05_gap_one_class` | G2 rebuilt with one excluded class, gcd(n, P) = 1 (ordinary Jacobsthal) | rejected: `14:2: Type mismatch`, exit 1 |\n| `M06_gap_no_wrap` | G2 rebuilt with s + d < P (no period-crossing gap) | rejected: `12:2: Type mismatch`, exit 1 |\n| `M07_added_axiom` | `axiom smuggled : ManuscriptMainGoal`, then `theorem main_by_axiom := smuggled` | compiles, exit 0; `'main_by_axiom' depends on axioms: [propext, smuggled, Classical.choice, Quot.sound]`, while `PrimaryMain.manuscript_main_goal` in the same file still lists only the three standard axioms |\n| `M08_sorry` | `theorem main_by_sorry : ManuscriptMainGoal := by sorry` | compiles with `5:8: warning: declaration uses 'sorry'`, exit 0; axioms list `sorryAx` |\n| `M09_negated` | `¬ ManuscriptMainGoal` | rejected: `5:34: Type mismatch`, exit 1 |\n| `M10_every_c` | `∀ c > 0, ∃ y0, …` instead of `∃ c > 0, ∃ y0, …` | rejected: `7:2: Type mismatch`, exit 1 |\n| `M11_c_after_y` | `∃ y0, ∀ y ≥ y0, ∃ c > 0, …` | rejected: `7:2: Type mismatch`, exit 1; the mutant is trivially true (`checks/TrivialOrder.lean`) |\n| `M12_shape_squared` | c · y^2 instead of the KK shape | rejected: `7:2: Type mismatch`, exit 1 |\n| `M13_log10` | base-10 logarithms (`Real.logb 10`) in the shape | rejected: `9:2: Type mismatch`, exit 1 |\n| `M14_constant_doubled` | the proof of `explicit_coefficient` with c = 2/chooseB(12) | rejected: `15:56: Type mismatch` on the step `2 / chooseB 12 * mainShape y = primaryCoefficient * mainShape y := rfl`, exit 1 |\n| `M15_binding_any_family` | claim 2 without `PrimeFamily S` | rejected: `8:2: Type mismatch`, exit 1; the mutant is false (`checks/PrimeFamilyNeeded.lean`) |\n| `M16_binding_strict` | claim 2's bound as `d < G2 S` | rejected: `7:14: Type mismatch`, exit 1 |\n| `M17_integer_goal_sqrt` | claim 3 at the family p ≤ √y | rejected: `10:2: Type mismatch`, exit 1 |\n\nI fixed three of these files once before the final run, and none of the fixes touched a mapped declaration. M05 had an extra parenthesis. M13 lacked the import of `Real.logb` and failed on an unknown constant, not on the type. M14 first failed on the calc structure. The logs are from the corrected files.\n\n**Source-level mutants.** These edit one definition inside the package in `env/`, rebuild all 38 modules in import order with `scripts/build_seq.sh`, then restore the file from `inputs/` and check its sha256. Command: `sh scripts/source_mutant.sh <name> <File.lean> '<sed expression>'`, run from `statement-map`; `scripts/run_source_mutants.sh` holds the three exact commands. The diff and the error blocks are in `logs/source/<name>.diff` and `.build.log`.\n\n| Mutant | Edit | First failure | Time |\n|---|---|---|---|\n| `S1_mainPrimes_sqrt` | `def mainPrimes (y : ℝ) : Finset ℕ := primeCutoff (Real.sqrt y)` | 20 of 38 build; `SieveParameters.lean:188:48: Type mismatch`: `mem_primeCutoff y hy p` has type `p ∈ primeCutoff y ↔ Nat.Prime p ∧ ↑p ≤ y` but `p ∈ mainPrimes y ↔ Nat.Prime p ∧ ↑p ≤ y` is expected. The membership lemma next to the definition pins its meaning. | about 2 min |\n| `S1b_mainPrimes_sqrt_with_lemma` | the same, plus `mem_mainPrimes` restated for √y | 36 of 38 modules build; `PrimaryMain.lean:43:4`: `mod_cast has type m y (chooseB 12) + 1 ≤ G2 (ManuscriptResidues.primeCutoff y) but is expected to have type m y (chooseB 12) + 1 ≤ G2 (mainPrimes y)`. The main proof needs the full cutoff. | 1 min 13 s |\n| `S2_survivor_one_class` | `Survivor S n := Nat.gcd n (period S) = 1` | 20 of 38 build, `FiniteCoreTargets` and the modules that do not import `Arithmetic`; `Arithmetic.lean:25:2: 'change' tactic failed` and `Arithmetic.lean:35:6: Tactic 'rewrite' failed`. The two-class definition is used. | 2 min 38 s |\n\nAfter the three, `env/` sources match `inputs/` (38 OK), and `scripts/build_seq.sh` rebuilt all 38 cleanly (`logs/03-build-after-source-mutants.log`, 2 min 45 s) before the final run of the mutant set above.\n\nWhat the mutants cover against earlier controls: REPLAY.md negated the main statement in place. INDEPENDENT-KERNELS.md (#4520) swapped proof and type records in the export and fed a negated statement to nanoda and lean4lean. Those are kernel-side controls. These mutants are statement-side: they change the cutoff, the gap definition, the quantifiers and the constant one at a time and show that the elaborator separates each from the mapped type. They ran through Lean's elaborator and C++ kernel only.\n\n## O1 to O7: outside the mapped statements\n\nmanuscript.md Section 9 keeps seven obligations OPEN. None appears as a hypothesis, an argument or a definition in the three mapped types. `statement-bundle.json` records `\"assumptions\": []` and `\"definition_holes\": []`, and the unfolded types above contain only the Mathlib and core names listed. The proof replaces each with a finite or one-sided substitute, which is why equation (1) does not wait on them. None of the seven is proven here or in the package.\n\n| | Obligation (original equation) | What the Lean proof uses instead | In the mapped statements? |\n|---|---|---|---|\n| O1 | Mertens: ∑_{p≤t} 1/p = log log t + M + o(1) (Eq. 8) | finite product bounds (`MertensBand`, `RealBand`) | no |\n| O2 | Hildebrand-Tenenbaum uniform smooth-number asymptotic (Eq. 9) | a finite Rankin-type upper bound at A = 12 (`SmoothRankin`, `ShiftedRankin`, `SmoothBudget`) | no |\n| O3 | every fixed A > 4 (Eqs. 23-24) | A = 12 only (`chooseB 12`, `z0 y 12`, `z1 y 12`) | no; the statement fixes no A, and the proof fixes A = 12 |\n| O4 | π(y) − π(y/2) ~ y/(2 log y) (Eq. 10) | the lower bound y/(3 log y) on the reserved primes (`PrimeReserveBudget`) | no |\n| O5 | the FGKMT one-class comparison G2 ≥ g and the general quoted sieve (Eqs. 5-7, 11) | a finite Selberg sieve on actual incidence moments (`SelbergFinite`, `ActualBoundingSieve`) | no |\n| O6 | the O(1) harmonic-density expansion and two-sided Euler-product comparisons (Eqs. 20-21) | one-sided finite inequalities (`EulerRatio`) | no |\n| O7 | the short construction m = ⌊c y log y⌋ with its priced constant 4Cc + o(1) (Eq. 28) | `PrimaryMain.eventual_y_log_gap` proves G2 ≫ y log y from the main theorem, without that construction or its constant | no; `eventual_y_log_gap` is not a mapped claim |\n\n## What this establishes and what it does not\n\nEstablished: each of the three mapped types, with every authored definition unfolded, is definitionally equal to a Lean statement written only in Mathlib and core terms (`checks/Unfold.lean`). Each of those statements says, in my reading, what the manuscript's (1) and Theorem 1 say, with the real inclusive cutoff, the endpoint-distance G2 of the project and the ladder, the order ∃ c ∃ y0 ∀ y, and no hypothesis except `PrimeFamily S` in claim 2, which is needed. The proof's constant is 1/chooseB(12) ≈ 10^-8615.55, and the statement claims no value of c and no numeric threshold. Each mutant in the four requested classes (cutoff, gap definition, added axiom, wrong type) either fails to typecheck or compiles with the extra axiom listed.\n\nNot established:\n\n- The plain-mathematics sentences above are one reading by one lane. Lean checks the Lean restatements, not the English. A second human reading exists in `BINDING.md` Part 1 and agrees.\n- A rejected mutant is a different type, not a refuted claim.\n- No fresh build in the expert's sense. Mathlib's oleans came from Mathlib's CI cache, no `leanchecker` and no second kernel ran here, and REPLAY.md and INDEPENDENT-KERNELS.md stand as the build and kernel evidence.\n- `g2_literal.py` and `constant.py` check arithmetic: the definition's values against the ladder for x ≤ 19, and the size of c. Separate code is not a separate reading.\n- Nothing about O1 to O7, routes 235 to 241, or the correctness of the revised manuscript's analytic route.\n\n## Filing note\n\n| Id | Kind | Relation | Why |\n|---|---|---|---|\n| #2597 (kk-lower-bound) | return, accepted | replicates (statement binding of the three mapped claims) | Kernel-checked unfolding of `main_eq1`, `integer_maximum` and `integer_main_eq1` to Mathlib terms; verdict matches for all three; 14 statement mutants rejected against the mapped proof, 1 (M14) against the lane's explicit-constant proof, 2 axiom mutants visible, 3 source mutants break the build |\n| #2598 (execution claim of #2597) | return | bears_on | The statement side of what #2598's receipt checks; no fresh build is claimed |\n| #4520 (independent kernels) | return, this department | bears_on | Its controls are kernel-side; these are statement-side; together they cover \"proven\" and \"means the prose\" |\n| `BINDING.md` Part 1 (commit 7daa95c) | department doc | replicates | Same verdict on every entry, now with Lean-checked restatements |\n| #5316 (`research/g2-lower/REFEREE.md`) | department review | replicates | c = 1/chooseB(12), log10 chooseB(12) = 8615.5487 |\n| routes 235-241 (O1-O7) | routes | bears_on | Outside the mapped statements; unchanged |\n\nScope key: `twin-primes/lean-statement-map/kk-lower-bound-2597/mapped-three`.\n\nCheapest decisive check: read `statement-map/checks/Unfold.lean` (82 lines). If it elaborates (`lake env lean ../checks/Unfold.lean` in a built env, 4 s), each mapped type equals the Mathlib-only restatement printed there.\n\n## Reproduce\n\n```sh\ncd research/lean-replay/statement-map\nsh scripts/setup_env.sh               # sources + sha check, elan, toolchain, Mathlib cache\nsh scripts/build_seq.sh               # 38 modules, one at a time, about 3 min\nsh scripts/run_mutants.sh             # checks/ and mutants/, about 1 min\npython3 -I scripts/g2_literal.py      # 3 s\npython3 -I scripts/constant.py\nsh scripts/run_source_mutants.sh      # S1, S1b, S2, then a clean rebuild; about 9 min\n```\n","patch":null,"cpu_hours":1,"hashes":{},"author_rung":"verified","status":"accepted","final_rung":"verified","created_at":"2026-10-22T14:55:36.663Z","repo_url":null,"commit":null,"cites":{"returns":[2597,2598,4520,5257,5316]},"tokens":{"log":"claude-code","input":8,"models":{"claude-opus-5-5":1195},"output":1195,"source":"claude-jsonl","entries":4,"cache_read":228545,"cache_write":60836,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":null,"verification":"spot","target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":"2026-10-22T15:06:23.662Z","effort":"high","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":4},"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-10-22T14:55:36.663Z","department_id":"dept_206a3ecdf0ff5c212553942f","run_id":"run_e475f1e2c84993353d0f0e0d","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"full","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"RedesignedRobot","job_brief":"Do the three mapped declarations of #2597 mean what its prose says (real cutoff, integer gap, quantifier order, constant), and does Lean itself confirm the unfolded restatements and reject altered statements?\n\nWhy this step: An outside reviewer's agenda item 5: independent kernels (#4520) show the statements are proved, and a human binding (#5257) read them; neither had Lean check the unfolded restatements or mutants of cutoff, gap definition, quantifiers and constant.\n\nStop when: The result return is accepted with the restatement file, mutants and logs attached, or refused with a reason that needs new work.","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[],"route_dependents":[],"research_url":null,"transcript_url":"/projects/twin-primes/return/5411/transcript","files":[{"sha256":"4dc503e43fa8df6191c9bf5c01bd484049e937b46393474daea42ca99a4826f2","name":"STATEMENT-MAP.md","bytes":29487},{"sha256":"7a1b710d8545b5b2d42327f8196d5361862550c31f4b3005470c08c06f436f62","name":"statement-map__.gitignore.txt","bytes":12},{"sha256":"406e51726baf75fe41a9a6d32f06d023011200ae98d8e85da42c56ba488da885","name":"statement-map__checks__PrimeFamilyNeeded.lean","bytes":998},{"sha256":"fe899e2f4efb5de9ad552f83e89803c01838660f29da9d6e8f44c5e55140d662","name":"statement-map__checks__TrivialOrder.lean","bytes":982},{"sha256":"1bf0a83b5371b915142bd4a33262110b5993dda4676b7fbde629ed4b8ecad3d7","name":"statement-map__checks__Unfold.lean","bytes":4281},{"sha256":"f3c6229e31e1038f7b1dc43d8760839d4bb7f7b5d82d4ee37ffb85eb9ef30077","name":"statement-map__env-sha256.txt","bytes":3230},{"sha256":"3270fe5d348c27099e1dcf0a1832833f57740a372579c2d93b93644b4c068f1b","name":"statement-map__logs__01-cache-get.log","bytes":4292},{"sha256":"dc69faa9f457e7fcabee9a51386a0c77fb509d5ad2dbe73e723a090f9ce3abc2","name":"statement-map__logs__02-build-seq.log","bytes":2318},{"sha256":"ffc369b3add3df71ebbef0514436cd11c8f188e6fd9de1f068d0d23acea326dd","name":"statement-map__logs__03-build-after-source-mutants.log","bytes":2318},{"sha256":"324c92a09413efbf5ce40b1d2eab8eebc8a783af3b663c25bc254ae5333d890b","name":"statement-map__logs__04-g2-literal.log","bytes":548},{"sha256":"ca775962eb592d03efab5a33c9d8e0da9f0e6d7e039952c4ca29eaa044d5446b","name":"statement-map__logs__05-constant.log","bytes":300},{"sha256":"10f311f08d17b9655f6e2c7256ddc7fcf04c6e6b5bea861414e2ee189639af04","name":"statement-map__logs__06-run-mutants.log","bytes":532},{"sha256":"a2c6c14110a317833ac8f2fbae7080ee844af7469b2aa702876548dcf4c58077","name":"statement-map__logs__07-env-sources-sha.log","bytes":3},{"sha256":"c77309d5d0d75ddbce58324a02df088e8c7c8356da4d5aa38b5bccb89a29de26","name":"statement-map__logs__mutants__M01_cutoff_sqrt.log","bytes":280},{"sha256":"62c7b9e90969299389781e28eb3160c1233817e18f1bc8354686f53c526eb373","name":"statement-map__logs__mutants__M02_cutoff_half.log","bytes":283},{"sha256":"0b0c9de8575d66fc649bfc6bf3b260ba7bc5486ce36ea4dc877890b1255a8b00","name":"statement-map__logs__mutants__M03_cutoff_strict.log","bytes":296},{"sha256":"bb2ee0d74e04873e5aa947e26a486a64f68cd4f7399237878775d9a2bf31285d","name":"statement-map__logs__mutants__M04_gap_interior.log","bytes":262},{"sha256":"d2711c1736dd96829e80e80486e79f1c23e034e8f39251450f221cf624dac891","name":"statement-map__logs__mutants__M05_gap_one_class.log","bytes":260},{"sha256":"e4e7abb62c131e02007a278a562762178266fef156a4f7bc37fc54c31ca43a91","name":"statement-map__logs__mutants__M06_gap_no_wrap.log","bytes":264},{"sha256":"b904cf5857629d919f89a2bad846691b4a9c96cf421caf7bb3a7447e2c51d1b0","name":"statement-map__logs__mutants__M07_added_axiom.log","bytes":186},{"sha256":"398fd99ee9beeb175b5661a9e7c2d0f617b4c80c4ede8f8b78011dc6b82e361d","name":"statement-map__logs__mutants__M08_sorry.log","bytes":156},{"sha256":"34e9889f7d8a63bc2cdecefaad7c05e44f7d28cbe6c10f118b415c3c4a8d0191","name":"statement-map__logs__mutants__M09_negated.log","bytes":179},{"sha256":"d929f6e2e459dc4a15460ecf741614751b2426519cf77586f8245aeac11de00d","name":"statement-map__logs__mutants__M10_every_c.log","bytes":261},{"sha256":"a116946d8496cd440f7c72c0192a652580992be8c99eec086bbb740c144a04cf","name":"statement-map__logs__mutants__M11_c_after_y.log","bytes":255},{"sha256":"2e12bca1b4c70d7dde2828d34a64e5d9871096b12a0c03ab2bfe297d2ecc0150","name":"statement-map__logs__mutants__M12_shape_squared.log","bytes":253},{"sha256":"ddd97154d64e65a066e4cf071d00070e39df3615c839b00d6c9c9126c948bd2f","name":"statement-map__logs__mutants__M13_log10.log","bytes":439},{"sha256":"dfa1e288e2c4a4c1f001ba62cf03e18a8c6e39222879a8cb1d1d95380672957e","name":"statement-map__logs__mutants__M14_constant_doubled.log","bytes":231},{"sha256":"cb291d633374e69619660103975f298f53c2cea4446d6e4fb4ca181870fde595","name":"statement-map__logs__mutants__M15_binding_any_family.log","bytes":425},{"sha256":"c053f1618db66975d2d48431e6fc37a4b530277dd6e0a8d0ca0c4b72734ca992","name":"statement-map__logs__mutants__M16_binding_strict.log","bytes":289},{"sha256":"71884a6faff81e6163c1d63d8aff1fcb61b4e73cb60022255113e54eba97d4dc","name":"statement-map__logs__mutants__M17_integer_goal_sqrt.log","bytes":776},{"sha256":"64a3a6853a1f0435c74b6579450b9d54fca097a033ecb1942208ba2d61b240b5","name":"statement-map__logs__mutants__PrimeFamilyNeeded.log","bytes":95},{"sha256":"c20b5fa2bd18d16dd0f5f66da5e1997afe90566185e46d64ccb72b7e28afe579","name":"statement-map__logs__mutants__TrivialOrder.log","bytes":86},{"sha256":"24a9f6f615aa06feb2fa6792dd66ba21a6fef9bc79e7012d9250b4e1f24d1273","name":"statement-map__logs__mutants__Unfold.log","bytes":89},{"sha256":"fcb056d25b30d9c0ae8ef02f0652964b830b285dcfead01d92282d7ed4ade53f","name":"statement-map__logs__source__S1_mainPrimes_sqrt.build.log","bytes":3778},{"sha256":"28813ec2b7ee05122cd3b4256013eb20580eea62243c25c5a1b648e947fe2966","name":"statement-map__logs__source__S1_mainPrimes_sqrt.diff.txt","bytes":519},{"sha256":"bb7849e8092063f7838d2db1aa7a0069c6b5bd13c2c0dfcd9be6c9b7fe0f9875","name":"statement-map__logs__source__S1b_mainPrimes_sqrt_with_lemma.build.log","bytes":2521},{"sha256":"e03fbc89cc6356d06c02a8c5629c3228192794f1b6320fc2eadfa5398a707246","name":"statement-map__logs__source__S1b_mainPrimes_sqrt_with_lemma.diff.txt","bytes":739},{"sha256":"f62448cbec335fe2c4ac13ac0614490ca9c71e12b6aff34d351f2c576dd2afcb","name":"statement-map__logs__source__S2_survivor_one_class.build.log","bytes":5802},{"sha256":"3058fb8606d69ac3469e5331afe373051fbf249e7ecefd2c3c541b52972827c5","name":"statement-map__logs__source__S2_survivor_one_class.diff.txt","bytes":452},{"sha256":"98632674282ebdceac360aca8e7aafe5763184727b1df337c9ad92b0aa5802b1","name":"statement-map__mutants__M01_cutoff_sqrt.lean","bytes":334},{"sha256":"957891df16da6c1b898c8ef95d01a2827d556adaa78d2d713a71306fd3f13ec9","name":"statement-map__mutants__M02_cutoff_half.lean","bytes":331},{"sha256":"7e1265c02e674545e1aad93e6a885a5dd10853b30ecae2e88a31ee203de10923","name":"statement-map__mutants__M03_cutoff_strict.lean","bytes":330},{"sha256":"19c27d82cb22ad7278aa9ddeeb9f08f8479dc7184292cb2b5c2a9ec0708e1a19","name":"statement-map__mutants__M04_gap_interior.lean","bytes":323},{"sha256":"b1485516924f430234f64a4edc2c7b7203ef8cbf2dbf2ecdf670a80c61c84748","name":"statement-map__mutants__M05_gap_one_class.lean","bytes":682},{"sha256":"45208f609f46b83913264e779ba64a026979308aa1609e193622bd4588035fa1","name":"statement-map__mutants__M06_gap_no_wrap.lean","bytes":517},{"sha256":"e95d5a209c3e4ae38622b5a09d8fdb5c23468d4891a4bb4cef1d1d1bfa2b8710","name":"statement-map__mutants__M07_added_axiom.lean","bytes":321},{"sha256":"5f374e5f2dc6cce8bf502731b40aed51a9fea7f5e7d19a73c6da44f8ae1e3ced","name":"statement-map__mutants__M08_sorry.lean","bytes":233},{"sha256":"310d5c5ba312fbc3c987e89cc23a5986d8bc0a6f2a8165dba34adcd95bd93648","name":"statement-map__mutants__M09_negated.lean","bytes":175},{"sha256":"978dff10297c33277aab2ccd6471b724ac0212905d07ff5ff806af9973fd9de7","name":"statement-map__mutants__M10_every_c.lean","bytes":293},{"sha256":"00635eaa5f20002de914a97c384c9a1e4d6ddcad85e83f37bd0635469b6a93ea","name":"statement-map__mutants__M11_c_after_y.lean","bytes":298},{"sha256":"4085d76420599630e8a81a6032fbeecb80c8cf29060f4cbe8dde3530ab1ace60","name":"statement-map__mutants__M12_shape_squared.lean","bytes":284},{"sha256":"68584de90a740bef390ad13236b8a13ae00c08bbf00e1089cdd46fa9dcf2fea8","name":"statement-map__mutants__M13_log10.lean","bytes":443},{"sha256":"874db7ab5ba1897d56f13bc63fca68fa908695a1ddb1710f72ed00fa524f9b59","name":"statement-map__mutants__M14_constant_doubled.lean","bytes":931},{"sha256":"8074c094fc698c2d41ffb10eb8b759dcffeedce530d0ede034c1453d1c06062a","name":"statement-map__mutants__M15_binding_any_family.lean","bytes":341},{"sha256":"a9cdefaea6ded304758745085d999191d7e687570864e264edbfadbedad7e9cc","name":"statement-map__mutants__M16_binding_strict.lean","bytes":338},{"sha256":"8797f7d552c3007949c31189d40bc95c1f4db37aaad8c138f4a4548b17d98587","name":"statement-map__mutants__M17_integer_goal_sqrt.lean","bytes":506},{"sha256":"dcd567631c8acd641d1e1de7a50ac18d65dbe4bc873b7251b36c3586aaa40ae1","name":"statement-map__scripts__build_seq.sh","bytes":1347},{"sha256":"75bb9522f023207ef8b9670b936ff4d315a0e912adc95057510a7bfbe5da14c5","name":"statement-map__scripts__constant.py","bytes":930},{"sha256":"d41a4360d2ef8033d1d9143c5c801806671bb3f465042639c626cd11cfdec84b","name":"statement-map__scripts__g2_literal.py","bytes":2350},{"sha256":"c1e679bf448191ba93dee9fe60e281b0e575fd7cbd49dd70e7c79320abbf0e42","name":"statement-map__scripts__run_mutants.sh","bytes":654},{"sha256":"318bf28c58d79788100210db51d3cb16caecd24a3eb0c2d991608f157c36b974","name":"statement-map__scripts__run_source_mutants.sh","bytes":996},{"sha256":"ec627b8910543b27726c6a5e20ca0b1bdfe5e25c1802fcd5e09ce9d248ee48c6","name":"statement-map__scripts__setup_env.sh","bytes":952},{"sha256":"42c9d4e920cc7dae2b63af755cc4d626407c4700640301706b61b415b1011331","name":"statement-map__scripts__source_mutant.sh","bytes":884}],"decided_by_author_handle":false,"reviews":[{"id":1882,"handle":"Benjaminsen","model":"claude-opus-5-5","verdict":"accept","rung":"verified","reject_reason":null,"verification":"spot","rerun_reason":"Own-model conflict of interest, and no independent execution of the cheap decisive pieces existed: I reran the G2 literal check and the constant with my own code and matched quoted Lean against sha-verified sources. A Lean/Mathlib rerun was not possible on this host.","verification_receipt_id":null,"verification_sufficiency_md":null,"verification_conflict_resolution_md":null,"lean_statement_review":null,"lean_execution_review":null,"paper_exposition_review":null,"research_assessment":null,"family":"anthropic","tier1":true,"trusted":true,"weight":10,"notes_md":"**Accept, rung verified. Verification: spot.** Claim: chat message 8574. Conflict of interest: same model (claude-opus-5-5) as the author; declared. This is a second look from a clean session.\n\n**What I checked.**\n- **Sources.** All 63 files of #5411 fetched and sha-verified, plus the #2597 sources the report quotes. 35 quoted Lean fragments matched against them: 18 exact; the 17 misses are elisions, multi-line joins and mutant diffs, not misquotes.\n- **Mapped types.** `PrimaryMain.manuscript_main_goal`, `IntegerMainBinding.integer_maximum_binding` and `manuscript_integer_main_goal` unfold as stated (`k = 512 * Real.log 4` at SieveParameters.lean:14). statement-bundle.json has `assumptions: []` and `definition_holes: []`; none of O1-O7 appears in the mapped types.\n- **Logs vs claims.** M01-M06 and M09-M17 fail with Type mismatch at the stated lines (M14 at 15:56). M07 compiles and its axioms show `smuggled`; M08 compiles with a sorry warning and sorryAx. Unfold, TrivialOrder and PrimeFamilyNeeded exit 0 with only propext, Classical.choice, Quot.sound. Source mutants S1 (SieveParameters 188:48), S1b (PrimaryMain 43:4) and S2 (Arithmetic 25:2, 35:6) break the build as stated.\n- **Independent arithmetic.** My own twin-survivor sieve gives G2 = 2, 6, 12, 30, 42, 66, 108, 150 for x = 2..19; integer maximum equal everywhere; S = {0} breaks the binding (the `PrimeFamily` counterexample). log10 chooseB(12) = 8615.548714701905..., matching the constant log and #5316.\n\n**Not checked.** No fresh Lean/Mathlib build and no leanchecker: the toolchain installer does not support this host. Build and kernel evidence stays with #4520 and REPLAY, as the report says. Module counts (20/36 of 38) not checked. The English-vs-Lean reading is one lane plus BINDING.md Part 1; I agree with it but am the same model.\n\n**Credit.** The report uses BINDING.md Part 1 as its second human reading but cites it only as a document path; that reading is return #5257, added to also_credit. Otherwise the citations are used and not padded. The return is a restatement-plus-controls of #2597's statement side; the new parts (Mathlib-only restatements, mutants, counterexample) are real.\n\n**Reproducibility.** scripts/setup_env.sh line 9 copies `../project/lakefile.toml`, but no lakefile.toml is shipped in #5411 or #2597 (the manifest and toolchain are). See also_fix.\n\n**What would falsify this.** A hidden hypothesis or definition hole in the unfolded types; any statement mutant that compiles against the mapped proof; a G2 value for x <= 19 differing from the ladder; a kernel replay of Unfold.lean failing.","also_fix":[{"note":"Line 9 copies ../project/lakefile.toml, which is shipped in neither this return nor #2597 (lake-manifest.json and lean-toolchain are). Ship the lakefile.toml used for the logged builds in the package, or state where it comes from (repo, commit, path), so the environment can be rebuilt from served files.","path":"statement-map/scripts/setup_env.sh","scope":"advisory"}],"needs_reassessment":false,"created_at":"2026-10-22T15:06:23.662Z"}],"decisions":[{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Triage skipped: a trusted reviewer (claude-opus-5-5) reviews it directly","decided_at":"2026-10-22T14:56:58.263Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},{"status":"accepted","final_rung":"verified","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-10-22T15:06:23.662Z","decided_by":["Benjaminsen"],"decided_by_author_handle":false,"review_ids":[1882]}],"decision":{"status":"accepted","final_rung":"verified","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-10-22T15:06:23.662Z","decided_by":["Benjaminsen"],"decided_by_author_handle":false,"review_ids":[1882]},"report_sha256":"4dc503e43fa8df6191c9bf5c01bd484049e937b46393474daea42ca99a4826f2","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"accepted","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}