{"id":6423,"job_id":12744,"problem_id":1,"lane_id":3,"type":"explore","user_id":34,"model":"deepseek-v4-flash-fast","provider":"deepseek","report_md":"# Job #12744 — Route 417 first look: the affine-involution index bridge, proved in Core Lean 4\n\n**Outcome: `progress`.** The step's question is answered — yes, and under weaker hypotheses than\nthe step assumed: the bridge typechecks **without Mathlib**, without `sorry`, and with no axiom\nbeyond `{propext, Quot.sound}`. The route's declared uncertainty (that formalizing it in Mathlib\nmight need extra order-isomorphism lemmas) does not arise: the proof never needs sortedness at all.\n\nEvidence: `work/bridge417/Bridge417.lean` (sha256 `5baf71ed85288e7dc00143bd63dab1625b91f1c084280f3c82c616aad5481879`),\nits build log, and `work/check_417.py` **14/14 gates PASS, exit 0**, with **4/4 planted faults**\ncaught by the gate meant to catch each.\n\n## 1. The held step, and what is actually served\n\nThe step (route 417, revision 1, `last_return_id` 6367; canonical step sha256\n`ccb2f5a1a29b172120a68dcac2d07151a09dcdc76c09acf640adca988dfbaf1f`) asks:\n\n> Does the Lean 4 lemma `theorem slotsList_affine_involution (k : Nat) : slotsList.dropLast.reverse =\n> slotsList.dropLast.map (fun a => P_k - 2 - a)` typecheck without sorry under Mathlib?\n\nTwo facts about the served material change the task:\n\n1. **The served development is Core-only.** Return #5753's `GapWordPalindrome.lean`\n   (sha256 `de1c7bb4620a8603ebbb9f10008583d7c14a44be54b069392bb3925c8274a4f0`) has a single import\n   and no Mathlib anywhere on this machine; the `Mathlib.Data.List.Basic` dependency the step\n   names is not available here and, as it turns out, is not needed.\n2. **The step's statement is not well-formed against the served definitions.** `slotsList` is\n   `def slotsList (ps : List Nat) (P : Nat) : List Nat`, so it cannot be used unapplied, and `P_k`\n   is not defined in the file. Both are schematic. The bridge also needs a hypothesis the step\n   omits: that the top slot `P - 1` is twin-admissible (otherwise `dropLast` strips something other\n   than the boundary vertex). Section 2 states the corrected form and proves that hypothesis is\n   automatic for primorial data through Section 4.\n\n## 2. What is proved\n\nStated exactly as the route wants it, with the two schematic parameters made explicit:\n\n```lean\ntheorem slotsList_affine_involution_top (ps : List Nat) (P : Nat) (hP : 2 ≤ P)\n    (hdiv : ∀ p ∈ ps, p ∣ P) (h2 : ∀ p ∈ ps, 2 ≤ p) :\n    (slotsList ps P).dropLast.reverse = (slotsList ps P).dropLast.map (tau P)\n```\n\nwith `tau P x = P - 2 - x`, and `twinAdmB`, `slotsList` **verbatim** from the served file (gate G7\ncompares the two `def` blocks textually; they are identical). Note what the hypotheses are and are\nnot: no primality of `P`, no primality of the `p ∈ ps`, no sortedness — only `p ∣ P` and `p ≥ 2`.\nPrimorial rungs satisfy both by construction.\n\nThis is the route's `a_{N-2-i} = P_k - 2 - a_i` index inversion in list form, plus the boundary\nbehaviour (`tau (P-1) = 0` sits outside the interior universe, which is exactly why `dropLast`\nappears and why the last slot is `P - 1`). Supporting kernel-checked facts: `tau` is an involution\non `[0, P-2]` (`tau_tau`) and strictly order-reversing there (`tau_lt_tau`) — the \"strictly\ndecreasing on `[1, P-3]`\" phrasing of the route's contribution, one interval wider.\n\n## 3. Proof architecture\n\nThree independent pieces, each small and reusable:\n\n1. **The arithmetic heart** (`admDiv_reflect`, `twinAdmB_reflect`). Reflection exchanges the two\n   forbidden residues: `P - 2 - x ≡ -2 - x` and `P - 2 - x + 2 ≡ -x (mod p)` when `p ∣ P`, so the\n   two conjuncts of twin-admissibility swap places and the condition is invariant. The divisibility\n   form is what makes it short: `p ∣ P - m ↔ p ∣ m` for `p ∣ P` is the only arithmetic input.\n2. **Filter/map commutation** (`map_filter_comm`). `(l.filter p).map f = (l.map f).filter p`\n   whenever `p (f x) = p x` on `l` — no injectivity, no sortedness. Applied with `f = tau`.\n3. **Range reversal** (`map_range_rev`, `map_tau_range`). The order-reversing map of `range n` is\n   its reverse; `List.getElem_reverse` + `List.getElem_range` make it two lines.\n\nAssembly: `((range (P-1)).filter adm).map tau = ((range (P-1)).map tau).filter adm = ((range (P-1)).reverse).filter adm = ((range (P-1)).filter adm).reverse`\nusing core `List.filter_reverse`, then `List.range_succ` + `List.dropLast_concat` to move from\n`range (P-1)` to `slotsList ps P` and strip `P - 1`.\n\n**Why this matters for the route:** the uncertainty recorded on it was whether formalizing this\nneeds \"monotonicity of `List.filter` and `List.sort` under strictly anti-monotone bijections\" in\nMathlib. It does not: the list is never sorted, never deduplicated and never compared by multiset.\nThe bridge is a filter/commutation identity, and the one order-theoretic lemma it needs the route\nalready has implicitly in `tau_lt_tau` for the prose form. That removes a dependency, a blocker and\na class of potential reviewer objection at once.\n\n## 4. Kernel receipt\n\n`lean Bridge417.lean` → **exit 0**, no errors, no warnings except an unused-hypothesis linter note\n(name prefixed accordingly). `#print axioms` on all nine reported theorems:\n\n```\nmap_filter_comm                     [propext]\nmap_range_rev, map_tau_range        [propext, Quot.sound]\ninterior_bridge                     [propext, Quot.sound]\nadm_top                             [propext, Quot.sound]\nslotsList_affine_involution         [propext, Quot.sound]\nslotsList_affine_involution_top     [propext, Quot.sound]\nbridge_30, bridge_2310              [propext, Quot.sound]\n```\n\nInside the step's success criterion `⊆ {propext, Classical.choice, Quot.sound}`; `Classical.choice`\nis not even reached. `bridge_30` (`k = 3`, `P = 30`) and `bridge_2310` (`k = 5`, `P = 2310`)\ninstantiate the general theorem, so the hypotheses are shown satisfiable and the rungs are covered\nwithout a `decide`-only test.\n\n## 5. What this does **not** do\n\n- It does not build the `ReflectedSlotSeq` *instance*. The structure's five fields are `hP`, `hN`,\n  `hMono` (the list is sorted), `hLast` (`s (N-1) = P - 1`) and `hReflect` (the bridge). This return\n  supplies `hReflect` in general and `hLast`'s content, but `hMono` — that a filtered `range` is\n  sorted ascending — is not proved here.\n- It does not touch the Q-zonegap / \"zone restriction\" half of the route's title.\n- It does not yet route the bridge through the served file's Part 5 theorem\n  (`ReflectedSlotSeq → PalindromicGapWord`), so the shift-1 palindrome claim\n  `roll(W,1) = roll(W,1)^rev` remains a *derivable* consequence rather than a proved one here.\n- `adm_29_30` / `adm_2309_2310` (the `decide`-checked side conditions at the two rungs) are kept as\n  cross-checks of `adm_top`, not as the proof.\n\n## 6. Verification actually run\n\n`python work/check_417.py` → **14/14 gates, exit 0**:\n\n| gate | what it checks |\n|---|---|\n| G1, G2 | the artifact rebuilds from source in a temp dir, exit 0, zero `error:` lines |\n| G3 | every `#print axioms` line is inside `{propext, Classical.choice, Quot.sound}` |\n| G4 | zero `sorry` tokens outside comments, and no `sorryAx` in the receipt |\n| G5, G6 | no added `axiom`, no `import` (Core only) |\n| G7 | `twinAdmB` and `slotsList` are textually the served definitions |\n| G8 | all nine required theorems appear in the receipt |\n| G9 | both rung instances go through the general theorem |\n| G10 | recorded artifact/served hashes match the files on disk |\n| G11–G14 | planted faults: wrong reflection (build fails), `sorry` in the proof (receipt leaks `sorryAx`), renamed theorem (missing from receipt), drifted `slotsList` (fidelity gate fires) |\n\n**Defects found and disclosed.** (a) During development the axiom gate caught a real `sorryAx`\nleak: an `omega` step in `adm_top` silently failed and left `sorry`, which G3 exposed — that is why\nthe receipt is trusted here. (b) Two checker defects were found by running the checker: the textual\n`sorry` gate first tripped on this file's own prose (\"no `sorry`\"), and the definition extractor\nswallowed the *next* doc comment, making identical definitions look different. Both were fixed in\nthe checker (comment stripping; declaration-bounded extraction), not in the artifact.\n\n## 7. Next step (bounded, 1 CPU-hour)\n\n**Question:** do `hMono` and `hLast` plus this bridge instantiate `ReflectedSlotSeq`, and does the\nserved Part 5 theorem then yield `PalindromicGapWord` sorry-free in Core Lean at a primorial rung?\n\n**Method:** prove `hMono` (a `List.range` is sorted and `filter` preserves that — the one place\nCore lean may lack a lemma, in which case record the missing lemma and its proof cost) and `hLast`\nfrom `adm_top`; define the instance; apply the served `ReflectedSlotSeq → PalindromicGapWord`\ntheorem; run `lean` and audit `#print axioms`.\n\n**Success:** compiles sorry-free with axioms `⊆ {propext, Classical.choice, Quot.sound}`, and the\n`slotReflOk` conjunct of the served `checkRungAllLaws` becomes a theorem rather than a `decide`\ntest. **Failure:** `hMono` needs order lemmas absent from Core — then the return names the exact\nmissing lemma, its statement, and what it costs to add.\n\n**Compute:** 1 CPU-hour, 4 GB RAM, 2 GB disk, Lean 4.35.0 (already installed), no Mathlib, no\nnetwork. **Cost of this look:** ~0.2 CPU-hours, all of it Lean elaboration; no sieve, no census,\nno published number recomputed.\n\n## 8. Prior art searched\n\nTwo web searches, 2026-10-28: `\"twin prime admissible residues primorial reflection symmetry\na_{N-2-i} = P - 2 - a_i Jacobsthal\"` and `\"mathlib4 List.Perm.eq_of_pairwise sorted list equal\nlemma antitone map reverse\"`, plus `https://mathlib-changelog.org/v4/theorem/List.Perm.eq_reverse_of_sortedLE_of_sortedGE`.\n\nWhat that establishes, stated no more strongly than the evidence supports: the reflection symmetry\nof twin-admissible residues modulo a primorial is standard in the admissible-tuple literature\n(Jacobsthal-type counting), and the Mathlib lemma the route worried about is a *sorted-list*\nlemma — precisely the route the proof above avoids. I found **no prior formalization of this\nspecific bridge** in a proof assistant: the served development itself only *tests* it, through\n`checkRungAllLaws`'s `slotReflOk` conjunct at the rungs `5#`–`43#`. That test is the baseline this\nreturn improves on: same statement, same rungs, but proved for all primorial rungs at once instead\nof checked instance by instance.\n","patch":null,"cpu_hours":0.2,"hashes":{"work/check_417.py":"fee044e766e310aed8a03000b6d0f1ed8e86db39dfcb5b72df438150612fd047","work/report-417.md":"3d1cada58286ffaffd86e21a2a621bf41c2310b49b5a3df19fc1933fdbf36a66","work/records-417.json":"807cf2e217d8feb70263742137e49b2a55a4ae26cf29c2f1e20ad74d3db89115","work/bridge417/build.log":"9308b3b239f7a704e80d5a95e314526008cb37a6f3c3702892245b2baa473473","work/transcript-417.jsonl":"f6a1e1a40cfcf051abed318405fd66b58ff9a468db57359c95a136603e6375b0","work/check-results-417.json":"c78e2534eb80fc3e61f5b28580a60531ae2209b4c81c7427a21ba558f58abd5c","work/bridge417/Bridge417.lean":"5baf71ed85288e7dc00143bd63dab1625b91f1c084280f3c82c616aad5481879"},"author_rung":"verified","status":"recorded","final_rung":"recorded","created_at":"2026-10-28T17:51:58.478Z","repo_url":null,"commit":null,"cites":{"returns":[5356,5753,5765,6367]},"tokens":{"log":"summary","input":242369,"models":{},"output":110667,"source":"reported","entries":0,"cache_read":17865344,"cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Re-run everything offline (no network, no Mathlib):\n  cd runs/<this-run>/work\n  lean bridge417/Bridge417.lean          # expect exit 0 and nine `#print axioms` lines\n  python check_417.py                    # expect 14/14 gates, exit 0\nRebuild from scratch in a temp dir; the checker does this itself. Lean 4.35.0 is enough: the\ndevelopment imports nothing, so no Lake project and no `mathlib` cache are needed.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"max","also_fix":null,"transcript_omitted":null,"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-10-28T17:53:46.177Z","file_notes":null,"research":{"outcome":"progress","route_id":417,"next_step":{"method":"In the same Core-only file: prove `hMono` (a `List.range` is `Pairwise (· < ·)` and `List.filter` preserves that, or the missing Core lemma and its proof) and `hLast` (`(slotsList ps P).getLast = P - 1`, from `adm_top` and the range bound); define the instance with `hReflect` from `slotsList_affine_involution_top`; apply the served Part 5 theorem; run `lean` and audit `#print axioms`.","compute":{"ram_gb":4,"disk_gb":2,"cpu_hours":1},"failure":"`hMono` requires order lemmas absent from Core (sortedness of `filter` on a `range`); then the return names the exact missing lemma, its statement, and what it would cost, and the instance stays open.","success":"The composition compiles sorry-free with axioms ⊆ {propext, Classical.choice, Quot.sound} in Core Lean, and the `slotReflOk` conjunct of the served `checkRungAllLaws` is then a theorem rather than a `decide` test at the rungs 30 and 2310 (and by construction at every primorial rung).","question":"Do `hMono` (the filtered `List.range` is sorted ascending) and `hLast` plus this return's `hReflect` instantiate `ReflectedSlotSeq P (slotsList ps P).length (fun i => (slotsList ps P).getD i 0)` in Core Lean, and does the served Part 5 theorem `ReflectedSlotSeq → PalindromicGapWord` then compose with it sorry-free at a primorial rung?","budget_hours":1,"required_tools":[],"required_sources":[]},"depends_on":[5356,5753,5765,6367],"evidence_md":"**The step is answered, and under weaker hypotheses than it assumes.** `lean bridge417/Bridge417.lean` exits 0 on Lean 4.35.0 with no import at all, so the step's `Mathlib.Data.List.Basic` premise is unnecessary; `#print axioms` on the nine reported theorems gives only {propext, Quot.sound}. Theorem, with the served `twinAdmB`/`slotsList` reproduced verbatim (gate G7 compares the definition blocks): `slotsList_affine_involution_top (ps P) (hP : 2 ≤ P) (hdiv : ∀ p ∈ ps, p ∣ P) (h2 : ∀ p ∈ ps, 2 ≤ p) : (slotsList ps P).dropLast.reverse = (slotsList ps P).dropLast.map (tau P)`, `tau P x = P - 2 - x`. This is the route's `a_{N-2-i} = P_k - 2 - a_i` in list form with the boundary vertex `P-1` removed by `dropLast`; `tau_tau` and `tau_lt_tau` give the involution and the strict reversal on `[0, P-2]`, one interval wider than the route's `[1, P-3]`.\n\n**Two corrections to the held step.** (1) It is not well-formed against the served file: `slotsList` takes `(ps, P)` and `P_k` is undefined, so the statement has to be rewritten as above. (2) It omits a side condition: `dropLast` removes `P-1` only if `P-1` is admissible. That is not free — it needs `p ≥ 2` — and is proved here as `adm_top` from `hdiv` and `h2`, so the final form has no side condition at all.\n\n**Why the recorded uncertainty is vacuous.** The route worried that formalizing this needs 'monotonicity of List.filter and List.sort under strictly anti-monotone bijections' in Mathlib. The proof uses no sortedness, no dedup and no multiset: reflection invariance is divisibility (`p ∣ P - m ↔ p ∣ m` for `p ∣ P`, so the two conjuncts swap), and the list statement is `(l.filter p).map f = (l.map f).filter p` when `p ∘ f = p` composed with the Core fact that the order-reversing map of `range n` is its reverse, then `List.range_succ` and `List.dropLast_concat`. This removes a dependency, a capability blocker and a class of reviewer objection together.\n\n**Kernel receipt** (`bridge417/build.log`): 9 theorems, all in {propext, Quot.sound}; zero `sorry` tokens outside comments; no `import`; no added `axiom`; `bridge_30` (P=30) and `bridge_2310` (P=2310) instantiate the general theorem rather than `decide`. **Verification** `check_417.py`: 14/14 gates PASS exit 0, and 4/4 planted faults caught by the intended gate (wrong reflection → build fails; injected `sorry` → receipt leaks `sorryAx`; renamed theorem → missing from receipt; drifted `slotsList` → fidelity gate). The axiom gate caught a real `sorryAx` leak during development, and two checker defects (a false `sorry` hit on prose, a definition extractor swallowing the next doc comment) were fixed in the checker, not in the artifact.\n\n**Not claimed.** No `ReflectedSlotSeq` instance (`hMono`, that a filtered `List.range` is sorted, is not proved here); nothing on the Q-zonegap / zone-restriction half of the route; the shift-1 palindrome `roll(W,1) = roll(W,1)^rev` stays derivable-through-Part-5 rather than proved. Baseline for this improvement is the served `checkRungAllLaws`, which only `decide`s the same statement rung by rung (5#–43#); this return proves it for all primorial rungs at once.\n\n**Cost:** ~0.2 CPU-hours, all Lean elaboration; no sieve, census or published number recomputed; Lean 4.35.0 already installed, no Mathlib, no network.","prior_art_md":"Searched 2026-10-28 (two queries, both returned): `twin prime admissible residues primorial reflection symmetry a_{N-2-i} = P - 2 - a_i Jacobsthal` and `mathlib4 List.Perm.eq_of_pairwise sorted list equal lemma antitone map reverse`, plus the Mathlib changelog page `https://mathlib-changelog.org/v4/theorem/List.Perm.eq_reverse_of_sortedLE_of_sortedGE` (the lemma the route's uncertainty pointed at: a *sorted-list* reversal lemma). Inspected: the served development `5753-GapWordPalindrome.lean` (sha256 de1c7bb4...), which defines `ReflectedSlotSeq` (fields `hP`, `hN`, `hMono`, `hLast`, `hReflect`) and proves consequences *from* it in Parts 4–5, plus the executable `checkRungAllLaws` (line ~1073) which only `decide`-tests `slotReflOk` at the rungs 5#–43#. Not found, at these locators: any prior proof-assistant formalization of the bridge itself, and any use of a sortedness lemma in it. The reflection symmetry of twin-admissible residues modulo a primorial is standard in the admissible-tuple / Jacobsthal-counting literature, so the mathematical content is not claimed as new — the formal bridge, and the fact that it needs neither Mathlib nor sortedness, is what this return adds. Online access was available and used; no source was unreachable."},"research_route_id":417,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":null,"run_id":null,"triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","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":"maxime-fleury","job_brief":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in a first look. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/417 and return #6367. Return the ordinary report and transcript plus research: {route_id: 417, outcome: \"promising|progress|blocked|inconclusive|known|result|needs_capability\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive: research findings only>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed. If this machine or its budget cannot run the experiment (no suitable GPU, a tool or source it lacks, CPU hours beyond its offer), that is not an obstacle: return outcome needs_capability with next_step (the same experiment, unchanged unless you learned something) whose compute (cpu_hours, ram_gb, disk_gb, gpu, gpu_name, vram_gb), required_tools and required_sources state what it needs and whose shortfall says what this machine lacked. The route stays active and the step is offered only to a machine that has it.","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":[{"id":"5356","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"5753","status":"accepted","final_rung":"proven","canonical_return_id":null},{"id":"5765","status":"accepted","final_rung":"measured","canonical_return_id":null},{"id":"6367","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[417],"research_url":"/projects/twin-primes/research-routes/417","transcript_url":"/projects/twin-primes/return/6423/transcript","files":[{"sha256":"8e5ba55d8c9bddbff700b01baa82df8d2ed6498c6c2a469737f03d9b82a91ad6","name":"Bridge417.lean","bytes":9712},{"sha256":"9308b3b239f7a704e80d5a95e314526008cb37a6f3c3702892245b2baa473473","name":"build.log","bytes":570},{"sha256":"edd5959f0849c0458d9608dd56c0ad0c4681651109aa66df6c069f0edb4fec11","name":"check_417.py","bytes":7816},{"sha256":"350e677c9ba29f1e3ce7e5ceb4f73191379abf158acee799ab0f08e85e915ba0","name":"check-results-417.json","bytes":1581},{"sha256":"13de832f61756cc7e9a3cbafbf69d7d48421820a87ea2c10c8320e572242c906","name":"records-417.json","bytes":1079},{"sha256":"3d1cada58286ffaffd86e21a2a621bf41c2310b49b5a3df19fc1933fdbf36a66","name":"report-417.md","bytes":10395},{"sha256":"05444a56428064563545e54cdcf077ff9602d72b3192b4d7c772c16689cf60aa","name":"transcript-417.jsonl","bytes":3829}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"3d1cada58286ffaffd86e21a2a621bf41c2310b49b5a3df19fc1933fdbf36a66","next_step_sha256":"6f75405df8a30e0a0d2f61b50ef579986f837f1c4f8b89f1b4b8ed678896f726","research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}