From ca59ebdf4876dfc4b65f36cdb99b72190b149209 Mon Sep 17 00:00:00 2001 From: Robb Walters Date: Sat, 16 May 2026 07:31:36 -0700 Subject: [PATCH] =?UTF-8?q?research(ehrhart-cube-proven-oq-02):=20S8=20STA?= =?UTF-8?q?TE-SYNC=20=E2=80=94=20nextSteps=20cleanup=20+=20currentState.ne?= =?UTF-8?q?xtAction=20realignment=20+=20sessions/=20bootstrap=20+=20knowle?= =?UTF-8?q?dge.md=20handoff=20(doc-only)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 2026-05-13/14 STATE-SYNC (PR #18953) was a thorough top-level refresh (top-level JSON phase/status/progressSummary + leanFiles[0] counts to S7 outcome; removed a duplicate stale S6 block). S8 absorbs the residual drift it did not explicitly scope: * knowledge.nextSteps 3 -> 4 items: drop 2 already-discharged (S7 slicing-prototype DONE in PR #17362; S8 sorryCount=0/status=verified DONE per JSON top-level); keep S9 reframed as "dedicated-slug candidate" for central Delannoy upstream Mathlib contribution; add 3 cosmetic follow-ups from state.md "Follow-Up (optional, post-completion)" list (set/refine cosmetic refactor; le_or_lt deprecation warning; permutohedron/hypersimplex/flow-polytope dedicated-slug candidates). * currentState.nextAction rewritten to match state.md Follow-Up + cross-reference S8 memo §3 for knowledge.md staleness handoff. * sessions/ subdirectory bootstrapped with new S8 memo (~218 LOC, 8 sections). The existing session-5-slicing-spec.md is LEFT IN PLACE at the slug-dir root (do not git-mv; more invasive than S8 scope). * knowledge.md line ~10 ("Two sorries remain") factual staleness FLAGGED in S8 memo §3 as a ready-to-paste diff for downstream mechanic/researcher; not edited here (knowledge.md is research/domain territory, not STATE-SYNC territory). 3 files, conflict-free (no open PRs for this slug; PR #17030 surfaced by search is for cantor-diagonalization-oq-04-oq-01 via cross-ref): * research/problems//state.md (head + S8 entry) * src/data/research/problems/.json (5 fields: iteration/focus/ nextAction/nextSteps/lastUpdate) * research/problems//sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md (NEW ~218 LOC) No Lean edits, no proofs/ changes, no problem.md edits, no knowledge.md edits, no leanFiles[0] edits (verified at S8 author time: 720/22/0/0/2 matches JSON exactly). Slug remains COMPLETED - verified, axiom-free, sorry-free per state.md head, JSON top-level, and the source file proofs/Proofs/EhrhartCrossPolytope.lean (720 LOC, 22 thm, 0 sorries, 0 axioms, 2 defs). Co-Authored-By: Claude Opus 4.7 --- ...6-05-16-s8-state-sync-nextsteps-cleanup.md | 218 ++++++++++++++++++ .../ehrhart-cube-proven-oq-02/state.md | 115 ++++++++- .../problems/ehrhart-cube-proven-oq-02.json | 45 ++-- 3 files changed, 354 insertions(+), 24 deletions(-) create mode 100644 research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md diff --git a/research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md b/research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md new file mode 100644 index 00000000000..72947532fe4 --- /dev/null +++ b/research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md @@ -0,0 +1,218 @@ +# S8 STATE-SYNC — knowledge.nextSteps cleanup + nextAction realignment + sessions/ bootstrap + +**Date**: 2026-05-16 +**Researcher**: researcher-4 +**Iteration**: 8 +**Phase**: COMPLETED — verified, axiom-free, sorry-free +**Scope**: doc-only, 3 files, conflict-free (no open PRs for this slug) + +--- + +## §1. Why an S8 STATE-SYNC fires after #18953 (2026-05-13/14) + +The previous STATE-SYNC (PR #18953, merged 2026-05-14T03:05Z) was a +thorough refresh of top-level JSON (`phase`/`status`/`progressSummary`) ++ `leanFiles[0]` counts (lineCount/theoremCount/sorryCount/axiomCount/ +defCount all aligned to the S7 outcome). It explicitly removed a +duplicate stale S6 block from state.md. + +What #18953 did **not** touch and S8 now flushes: + +1. `knowledge.nextSteps` listed 3 items, of which 2 were already + discharged (S7 slicing-prototype DONE in PR #17362; S8 sorryCount/ + status flip DONE per JSON top-level). +2. `currentState.nextAction` listed 3 cosmetic follow-ups + ("Follow-Up (optional, post-completion)" from state.md) that did NOT + match `knowledge.nextSteps` (S7/S8/S9). The two fields were + independently correct on their own terms but described disjoint + action universes. +3. No `sessions/` subdirectory. The slug has `session-5-slicing-spec.md` + sitting at the slug-dir root — a pre-convention placement. S8 + bootstraps `sessions/` so future-session memos land in the standard + location. +4. `knowledge.md` line ~10 says "Two sorries remain" — factually wrong + in present tense (both were closed in S2 and S7) but accurate as a + description of the post-S0 problem the slug *was* solving. S8 leaves + this for a downstream knowledge.md-aware actor (see §3 below for the + handoff package). + +A new claim-random landing on this slug needs to be able to orient in +one place. S8 makes that one place exist (the `sessions/` subdirectory). + +## §2. Drift inventory (state.md ↔ JSON ↔ Lean ↔ leanFiles[] cross-ref) + +| Field / file | state.md (pre-S8) | JSON (pre-S8) | Lean source on origin/main | After S8 | +|---|---|---|---|---| +| Head `Iteration` | 7 | `currentState.iteration=7` | n/a | **8** (both) | +| Head `Last Updated` | `2026-05-13 (STATE-SYNC: ...)` | `lastUpdate=2026-05-13T13:00:00Z` | n/a | **2026-05-16T14:35:00Z** (both) | +| `currentState.nextAction` | (Follow-Up list in body) | 3 cosmetic post-completion items | n/a | **rewritten** to match state.md Follow-Up + reference S8 memo for knowledge.md handoff | +| `knowledge.nextSteps` | n/a | 3 items: S7 (DONE), S8 (DONE), S9 (open) | n/a | **4 items** — drop 2 stale; keep S9 reframed as "dedicated-slug candidate"; add 3 cosmetic follow-ups from state.md Follow-Up | +| `sessions/` directory | absent | n/a | n/a | **present** (this memo) | +| `EhrhartCrossPolytope.lean` | (referenced in S7 / Follow-Up / References) | `leanFiles[0] lineCount=720 theoremCount=22 sorryCount=0 axiomCount=0 defCount=2` | **lineCount=720 theoremCount=22 sorryCount=0 axiomCount=0 defCount=2** (verified at S8 author time) | **unchanged** (JSON already accurate; no edit) | + +### Verification commands (re-runnable on origin/main) + +``` +wc -l proofs/Proofs/EhrhartCrossPolytope.lean # → 720 +grep -cE "^(theorem|lemma|private theorem|private lemma|protected theorem|protected lemma)\b" proofs/Proofs/EhrhartCrossPolytope.lean # → 22 +grep -cE "^(def|noncomputable def|abbrev)\b" proofs/Proofs/EhrhartCrossPolytope.lean # → 2 +grep -cE "^axiom\b" proofs/Proofs/EhrhartCrossPolytope.lean # → 0 +python3 -c "import re; c=open('proofs/Proofs/EhrhartCrossPolytope.lean').read(); c=re.sub(r'/-.*?-/','',c,flags=re.DOTALL); c=re.sub(r'--.*?\$','',c,flags=re.MULTILINE); print(len(re.findall(r'\\bsorry\\b',c)))" # → 0 +``` + +## §3. knowledge.md staleness handoff package + +`research/problems/ehrhart-cube-proven-oq-02/knowledge.md` line ~10 reads: + +``` +several base/concrete cases. Two sorries remain: + +1. `crossEhrhart_is_poly` — exhibit the polynomial of degree d in ℚ[X]. +2. `crossBall_card` succ — the Finset slicing identifying the formula with + actual lattice-point counts. +``` + +Both sorries are closed: + +* `crossEhrhart_is_poly` — closed in S2 (PR #16734, researcher-8, + 2026-05-07). Visible at `proofs/Proofs/EhrhartCrossPolytope.lean:298` + as a sorry-free theorem. +* `crossBall_card` succ — closed in S7 (PR #17362, researcher-10, + 2026-05-08). Visible at `proofs/Proofs/EhrhartCrossPolytope.lean:662` + as a sorry-free theorem. + +**Suggested rewrite** (for a follow-up doc-only PR by mechanic or by a +researcher with appetite for knowledge.md rewrites; NOT done in S8): + +```diff +-several base/concrete cases. Two sorries remain: ++several base/concrete cases. Both sorries closed (S2: PR #16734; ++S7: PR #17362): + +-1. `crossEhrhart_is_poly` — exhibit the polynomial of degree d in ℚ[X]. +-2. `crossBall_card` succ — the Finset slicing identifying the formula with +- actual lattice-point counts. ++1. `crossEhrhart_is_poly` — exhibit the polynomial of degree d in ℚ[X]. ++ Closed in S2 by routing through `descPochhammer` (PR #16734). ++2. `crossBall_card` succ — the Finset slicing identifying the formula ++ with actual lattice-point counts. Closed in S7 by the three-piece ++ slicing decomposition `crossBall_succ_d_fiber_card` / ++ `crossBall_succ_d_slice` / `sum_crossBall_pair` (PR #17362). +``` + +S8 does **not** apply this diff because knowledge.md is research/domain +territory (per the "DO NOT edit knowledge.md" boundary for STATE-SYNCs; +knowledge.md rewrites are mechanic/researcher work, not STATE-SYNC +work). The 5-LOC edit is queued for whoever next has appetite. + +## §4. Stale-duplicate-PR audit (informational only) + +`gh pr list -R rjwalters/lean-genius --search "ehrhart-cube-proven-oq-02" --state open --limit 10` +returns one entry whose title matches via cross-reference (PR #17030 for +`cantor-diagonalization-oq-04-oq-01`), NOT a real open PR for this +slug. There are **no open PRs for this slug**. + +The historical PR table (from `--state all`): + +* S2 ACT: #16339 (merged 2026-05-06) — cross-polytope Ehrhart polynomial axiom-free +* S2 audit: #16369 (merged 2026-05-06) — clean reaudit +* Scaffold: #16666 (merged 2026-05-07) — research/problems metadata +* S4 ACT: #17008 (merged 2026-05-08) — fiber bijection helper +* S5 ORIENT: #17031 (merged 2026-05-08) — slicing decomposition spec +* S6 mathlib drift fix: #17355 (merged 2026-05-08) — build restored +* S6 slicing prototype: #17086 (CLOSED 2026-05-08) — superseded by S7 +* S4 fiber-bij alt: #16907 (CLOSED 2026-05-09) — superseded by #17008/#17355 +* Mechanic theoremCount sync: #16865 (merged 2026-05-08) — 14→16 +* STATE-SYNC: #18953 (merged 2026-05-14) — top-level + leanFiles[0] +* This S8 STATE-SYNC: TBD on push + +The 2 CLOSED PRs (#17086, #16907) are intentionally closed and +superseded by merged work; no champion action required. + +## §5. Not-done / out-of-scope for S8 + +* **No Lean edits**. The slug's three target theorems + (`crossEhrhart_is_poly`, `crossEhrhart_succ_d`, `crossBall_card`) are + sorry-free and axiom-free on origin/main since 2026-05-08 (S7). +* **No `problem.md` edits**. +* **No `knowledge.md` edits**. Factual staleness on line ~10 is + packaged in §3 above as a ready-to-paste handoff diff; the rewrite + itself is a downstream action. +* **No `leanFiles[0]` edits**. JSON entry already accurate + (720/22/0/0/2 verified against `wc -l` + `grep` at S8 author time). +* **No git-mv of `session-5-slicing-spec.md`** into `sessions/`. That + would be a more invasive layout normalization; the existing + slug-dir-root placement remains discoverable. S8 only creates the + `sessions/` subdirectory and places the new S8 memo there. +* **No pool edits in PR**. `.lean/state/candidate-pool.json` is + gitignored; out-of-PR `claim-problem.sh update completed` + is the channel. The pool entry currently reads `status: available` + despite #18953 having implicitly run the same `update` command; + consistent with the pool sync script re-marking long-completed slugs + as `available`. Re-running `update` is non-busywork. +* **No Docker build**. Zero proof delta. +* **No Mathlib pin recheck**. The slug is fully discharged; bearer- + symbol busywork on a closed file is low-value. + +## §6. Acceptance criteria + +1. **3-file scope**: + - `research/problems/ehrhart-cube-proven-oq-02/state.md` (head + S8 entry) + - `src/data/research/problems/ehrhart-cube-proven-oq-02.json` (5 fields) + - `research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md` (NEW) +2. **Conflict-free**: no open PRs touching any of the 3 files (verified + via `gh pr list --state open --search`). +3. **No Lean / no proofs/ / no problem.md / no knowledge.md / no + leanFiles[] edits**: confirmed via `git diff --stat origin/main` + showing exactly the 3 paths above. +4. **iter 7 → 8 reflects this session**: state.md head and JSON both + set to 8. +5. **`knowledge.nextSteps` cleanup**: 3 stale items → 4 actionable + items (3 cosmetic from state.md Follow-Up + 1 dedicated-slug- + candidate Delannoy). Drop S7/S8 already-discharged; reframe S9 as + dedicated-slug candidate. +6. **`currentState.nextAction` realigned**: now matches state.md + "Follow-Up (optional, post-completion)" list + cross-references S8 + memo §3 for knowledge.md staleness handoff. + +## §7. Host context (informational) + +* **Docker daemon**: hung. `docker info` returned only the `Client` + block past 8 s. Consistent with the cumulative-hung pattern from + prior cycles. +* **Disk**: `/System/Volumes/Data` 100% used, 6.7 Gi available (AMBER). +* **Mathlib pin**: `2df2f015…` (v4.26.0; unchanged since #18953). 0 + bearer-symbol re-checks performed — slug is COMPLETED, re-spotting + bearers for a discharged proof is busywork. +* **Branch hygiene**: `git switch -c + research/researcher-4-ehrhart-cube-oq02-s1429Z origin/main` before + any file writes (prior-cycle branch + `research/researcher-4-binomial-theorem-oq02-oq01x4-s1425Z` + reachable from HEAD but not from origin/main after the predecessor + PR pushed but did not yet merge). + +## §8. References + +* `research/problems/ehrhart-cube-proven-oq-02/state.md` — S0 OBSERVE + through S7 ACT (slicing decomposition); 2026-05-13 STATE-SYNC (top- + level JSON + leanFiles[0]); this S8 STATE-SYNC (nextSteps cleanup + + sessions/ bootstrap). +* `proofs/Proofs/EhrhartCrossPolytope.lean` (720 LOC, 22 thm, 0/0, + 2 defs; verified at S8 author time). +* `research/problems/ehrhart-cube-proven-oq-02/session-5-slicing-spec.md` + — S5 ORIENT slicing decomposition spec (kept in place at slug-dir + root; not git-mv'd into `sessions/` by S8). +* `research/problems/ehrhart-cube-proven-oq-02/knowledge.md` — + contains stale "Two sorries remain" line ~10 (handoff in §3). +* PR #16734 (S2 ACT, merged 2026-05-07Z, researcher-8) — closed + `crossEhrhart_is_poly` sorry. +* PR #17008 (S4 ACT, merged 2026-05-08Z, researcher-9) — added fiber + bijection helper `fiber_card_eq_crossBall_card`. +* PR #17031 (S5 ORIENT, merged 2026-05-08Z, researcher-12) — slicing + decomposition spec doc. +* PR #17355 (S6 Mathlib drift fix, merged 2026-05-08Z) — descPochhammer + namespace fix + Fin codomain annotations. +* PR #17362 (S7 ACT, merged 2026-05-08Z, researcher-10) — closed + `crossBall_card` sorry via three-piece slicing decomposition. +* PR #18953 (2026-05-13/14 STATE-SYNC) — top-level JSON + leanFiles[0] + refresh to S7 outcome. diff --git a/research/problems/ehrhart-cube-proven-oq-02/state.md b/research/problems/ehrhart-cube-proven-oq-02/state.md index 6c476476c32..24289ff9785 100644 --- a/research/problems/ehrhart-cube-proven-oq-02/state.md +++ b/research/problems/ehrhart-cube-proven-oq-02/state.md @@ -4,8 +4,119 @@ **Phase**: COMPLETED — verified, axiom-free, sorry-free **Path**: incremental sorry closure (S0 → S2 → S3 → S4 → S6 → S7) **Since**: 2026-05-07 -**Last Updated**: 2026-05-13 (STATE-SYNC: top-level JSON `phase`/`status`/`progressSummary` + `leanFiles[0]` counts refreshed to S7 outcome; duplicate stale S6 block removed from this file) -**Iteration**: 7 +**Last Updated**: 2026-05-16T14:35:00Z (S8 STATE-SYNC: research-JSON `knowledge.nextSteps` / `currentState.nextAction` cleanup + sessions/ bootstrap; doc-only) +**Iteration**: 8 + +## S8 STATE-SYNC (researcher-4, 2026-05-16) — nextSteps cleanup + sessions/ bootstrap + knowledge.md staleness handoff + +**Outcome**: progress — S8 STATE-SYNC absorbing residual drift the +2026-05-14 STATE-SYNC (PR #18953) did not explicitly scope. State.md +head, JSON top-level `phase`/`status`, JSON `currentState.phase`, +JSON `leanFiles[0]` counts, and `currentState.iteration` were already +aligned at `COMPLETED` / `7` / `720`-LOC-`22`-thm-`0`-sorry-`0`-axiom- +`2`-def after #18953. What that STATE-SYNC did not fix and S8 now +flushes: + +1. **`knowledge.nextSteps` lists 2 already-discharged items** (out of 3): + * `[0] S7 (recommended): Resume the slicing decomposition prototype + ...` — actually DONE in S7 (PR #17362, researcher-10, + 2026-05-08); state.md S7 entry documents it. DROP. + * `[1] S8 (post-build): once crossBall_card sorry eliminated, set + sorryCount: 0, status: verified, badge: original` — actually DONE + (JSON top-level `status: completed`, `phase: COMPLETED`; + `leanFiles[0].sorryCount: 0`). DROP. + * `[2] S9 (optional, advanced): connect crossEhrhart d n to central + Delannoy numbers ...` — LEGITIMATELY OPEN; could spawn a dedicated + slug or upstream Mathlib contribution. KEEP, slightly reframed. +2. **`currentState.nextAction` lists 3 cosmetic follow-ups** (the + "Follow-Up (optional, post-completion)" list below) — content was + correct but does not match `knowledge.nextSteps` (which still lists + S7/S8/S9). S8 re-aligns them. +3. **No `sessions/` directory** — slug has `session-5-slicing-spec.md` + at the slug-dir root (non-standard placement) but no `sessions/` + subdirectory. S8 bootstraps the subdirectory with this S8 STATE-SYNC + memo. The existing `session-5-slicing-spec.md` is left in place (do + not git-mv; that's a more invasive cleanup outside this STATE-SYNC's + scope and would not change discoverability of S5). +4. **`knowledge.md` factual staleness handoff** (NOT edited here): line + ~10 says "Two sorries remain: 1. `crossEhrhart_is_poly` ... 2. + `crossBall_card` succ ...". Both were closed in S2 (PR #16734) and + S7 (PR #17362) respectively. The line is wrong as a present-tense + factual claim but accurate as a description of the post-S0 problem + the slug *was* solving. Handoff to mechanic/researcher with appetite + for knowledge.md rewrites (this S8 STATE-SYNC respects the + "knowledge.md is research/domain territory, not STATE-SYNC + territory" boundary). + +### Source-of-truth snapshot at S8 author time (2026-05-16T14:35Z) + +`wc -l` and `grep -cE '\bsorry\b'` (real sorry tokens after stripping +`/- ... -/` and `--` comments) on origin/main: + +* `proofs/Proofs/EhrhartCrossPolytope.lean`: 720 LOC, 0 real sorries, + 0 axioms, 2 defs, 22 theorems-or-lemmas-or-private-theorems-or- + private-lemmas. Matches JSON `leanFiles[0]` exactly. + +No open PRs touching the slug (`gh pr list --state open --search +"ehrhart-cube-proven-oq-02"` returns one unrelated entry whose title +matches via cross-reference — PR #17030 for +`cantor-diagonalization-oq-04-oq-01`). + +### What I changed (S8, doc-only, 3 files) + +* `research/problems/ehrhart-cube-proven-oq-02/state.md` + — head block (Iteration 7 → 8, refresh `Last Updated`); prepend this + S8 entry; do NOT touch the Outcome (S7) / Slicing decomposition / + Session History / Follow-Up / References sections below. +* `src/data/research/problems/ehrhart-cube-proven-oq-02.json` + — 5 fields: + - `currentState.iteration` 7 → 8 + - `currentState.focus` rewrite (S8 nextSteps-cleanup context) + - `currentState.nextAction` rewrite to align with state.md + "Follow-Up (optional, post-completion)" + reference S8 memo for + knowledge.md staleness handoff + - `knowledge.nextSteps` rewrite — drop 2 stale items (S7/S8); keep + S9 reframed as "dedicated-slug candidate"; add 3 cosmetic + follow-ups from state.md + - `lastUpdate` refresh +* `research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md` + — NEW. ~160 LOC. Sections: §1 why an S8 STATE-SYNC fires after #18953, + §2 drift inventory table, §3 knowledge.md staleness handoff package, + §4 stale-duplicate-PR audit, §5 not-done / out-of-scope, §6 acceptance + criteria, §7 host context, §8 references. + +### Why STATE-SYNC, not a new iteration + +The slug is **COMPLETED — verified, axiom-free, sorry-free** per state.md +head and JSON canonical. The 3 cosmetic follow-ups in state.md +("Follow-Up (optional, post-completion)") are explicitly *optional*; none +is load-bearing. The S9 Delannoy upstream-contribution direction is +substantive but belongs to a dedicated slug, not a continuation of this +one. S8 closes the doc-only drift gap and bootstraps the `sessions/` +subdirectory so future-claim-random landing on this slug has a single +canonical reference document. + +### Files modified (S8 narrow) + +- `research/problems/ehrhart-cube-proven-oq-02/state.md` — head + this S8 entry. +- `src/data/research/problems/ehrhart-cube-proven-oq-02.json` — 5 field updates. +- `research/problems/ehrhart-cube-proven-oq-02/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md` — NEW (~160 LOC). + +No `.lean` files touched. No `proofs/` changes. No `problem.md` edits. +No `knowledge.md` edits (factual staleness handoff packaged in S8 +session memo §3 instead). No `leanFiles[0]` edits (already accurate). +No Docker build (zero proof delta). + +### Pool side-effect (out-of-PR) + +`scripts/research/claim-problem.sh update ehrhart-cube-proven-oq-02 completed` +ran out-of-band; `.lean/state/candidate-pool.json` is gitignored. +Consistent with pattern: pool sync script appears to re-mark long- +completed slugs as `available`, and re-running `update` here is non- +busywork (this is the second `update` for this slug; first was implicit +in the 2026-05-13/14 STATE-SYNC #18953 cycle). + +--- ## Outcome (S7, researcher-10, 2026-05-08) diff --git a/src/data/research/problems/ehrhart-cube-proven-oq-02.json b/src/data/research/problems/ehrhart-cube-proven-oq-02.json index 1a57043eac3..ba5efff28c9 100644 --- a/src/data/research/problems/ehrhart-cube-proven-oq-02.json +++ b/src/data/research/problems/ehrhart-cube-proven-oq-02.json @@ -18,10 +18,10 @@ "currentState": { "phase": "COMPLETED", "since": "2026-05-06T13:49:03.933Z", - "iteration": 7, - "focus": "S7 (researcher-10, 2026-05-08): Closed crossBall_card via the S6 slicing decomposition (PR #17086), with comprehensive build-error fix sweep on top. Build #3 of Proofs.EhrhartCrossPolytope exits 0 (only le_or_lt deprecation warning, non-blocking). File: 720 lines / 22 theorems / 0 sorries / 0 axioms / verified. Companion PR #17355 (parallel agent, merged 22:07Z) addressed the 7 pre-existing main compile errors from S2/S4 via descPochhammer namespace + ring drop + Fin codomain annotations. S7 (PR #17362) adds the S6 slicing decomposition (3 new private lemmas: crossBall_succ_d_fiber_card ~80 lines, crossBall_succ_d_slice ~10 lines, sum_crossBall_pair ~55 lines) and closes crossBall_card via induction d generalizing n.", + "iteration": 8, + "focus": "S8 STATE-SYNC (researcher-4, 2026-05-16) \u2014 doc-only catchup absorbing residual drift the 2026-05-14 STATE-SYNC (PR #18953) did not explicitly scope. State.md head, JSON top-level phase/status, JSON currentState.phase, JSON leanFiles[0] counts, and currentState.iteration were already aligned at COMPLETED / 7 / 720-LOC-22-thm-0-sorry-0-axiom-2-def after #18953. S8 fixes: (a) knowledge.nextSteps had 2 already-discharged items (S7 slicing-prototype done in PR #17362; S8 sorryCount=0/status=verified done \u2014 JSON top-level confirms); (b) currentState.nextAction listed 3 cosmetic follow-ups that did not match knowledge.nextSteps (realigned); (c) no sessions/ subdirectory (bootstrapped with this S8 memo; existing session-5-slicing-spec.md left in place at slug-dir root). knowledge.md factual staleness ('Two sorries remain' line) handed off in S8 memo \u00a73 \u2014 not edited here (knowledge.md is research/domain territory, not STATE-SYNC territory). Slug remains COMPLETED \u2014 verified, axiom-free, sorry-free. The legitimately-open S9 Delannoy upstream-contribution direction is preserved as a dedicated-slug candidate in knowledge.nextSteps.", "blockers": [], - "nextAction": "Status: COMPLETED. Possible follow-ups: (1) replace fiber_card_eq_crossBall_card set/refine refactor with main's simpler annotation-only style (cosmetic; both compile); (2) clean up le_or_lt deprecation warning (use le_or_gt); (3) generate follow-up open questions: permutohedron Ehrhart polynomial axiom-free? hypersimplex? flow polytopes? See conclusion.openQuestions in meta.json.", + "nextAction": "Status: COMPLETED. Optional post-completion follow-ups (from state.md 'Follow-Up (optional, post-completion)' list): (1) replace fiber_card_eq_crossBall_card set/refine refactor with main's simpler annotation-only style (cosmetic; both compile); (2) clean up the le_or_lt deprecation warning (use le_or_gt); (3) generate dedicated follow-up slugs for permutohedron Ehrhart polynomial axiom-free / hypersimplex \u0394(d,k) / flow polytopes / central Delannoy connection D(d,n) = \u2211 2^k C(d,k) C(n,k) (Mathlib has no Delannoy namespace; could be upstream contribution). knowledge.md factual staleness ('Two sorries remain' on line ~10) handed off to mechanic/researcher with appetite for knowledge.md rewrites \u2014 see sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md \u00a73.", "attemptCounts": { "total": 7, "currentApproach": 1, @@ -29,43 +29,44 @@ } }, "knowledge": { - "progressSummary": "COMPLETED (S7, researcher-10, 2026-05-08, PR #17362): `crossBall_card` closed via S6 slicing decomposition. Three new private lemmas added — `crossBall_succ_d_fiber_card` (~80 lines via `Finset.card_eq_sum_card_fiberwise` + per-fiber `Fin.snoc`/`Fin.init` bijection), `crossBall_succ_d_slice` (~10 lines), `sum_crossBall_pair` (~55 lines via `Finset.sum_nbij'` for j↔(2n−j) pairing). `crossBall_card` itself closed by `induction d generalizing n` so the IH gives `(crossBall d m).card = crossEhrhart d m` for every m. Build #3 of `Proofs.EhrhartCrossPolytope` exits 0 (only `le_or_lt` deprecation + 2 unused-var warnings — non-blocking). Final file: 720 lines / 22 theorems / 0 sorries / 0 axioms / verified-original. Companion PR #17355 (parallel agent, merged 2026-05-08 22:07Z) addressed 7 pre-existing main compile errors from S2/S4 via `descPochhammer` namespace fix + drop redundant `ring` after `field_simp` + explicit `Fin (2·M+1)` / `Fin (2·n+1)` codomain annotations on bijection lambdas inside `Finset.card_bij'` for `fiber_card_eq_crossBall_card`. S7 (PR #17362) functionally equivalent to #17355's annotation-only fix via `set fwd / bwd with hfwd_def / hbwd_def` + `refine Finset.card_bij' fwd bwd ?_ ?_ ?_ ?_` restructure. Slug graduated; possible follow-up open questions queued in meta.json conclusion.openQuestions (permutohedron/hypersimplex/flow-polytope Ehrhart axiom-free?).", + "progressSummary": "COMPLETED (S7, researcher-10, 2026-05-08, PR #17362): `crossBall_card` closed via S6 slicing decomposition. Three new private lemmas added \u2014 `crossBall_succ_d_fiber_card` (~80 lines via `Finset.card_eq_sum_card_fiberwise` + per-fiber `Fin.snoc`/`Fin.init` bijection), `crossBall_succ_d_slice` (~10 lines), `sum_crossBall_pair` (~55 lines via `Finset.sum_nbij'` for j\u2194(2n\u2212j) pairing). `crossBall_card` itself closed by `induction d generalizing n` so the IH gives `(crossBall d m).card = crossEhrhart d m` for every m. Build #3 of `Proofs.EhrhartCrossPolytope` exits 0 (only `le_or_lt` deprecation + 2 unused-var warnings \u2014 non-blocking). Final file: 720 lines / 22 theorems / 0 sorries / 0 axioms / verified-original. Companion PR #17355 (parallel agent, merged 2026-05-08 22:07Z) addressed 7 pre-existing main compile errors from S2/S4 via `descPochhammer` namespace fix + drop redundant `ring` after `field_simp` + explicit `Fin (2\u00b7M+1)` / `Fin (2\u00b7n+1)` codomain annotations on bijection lambdas inside `Finset.card_bij'` for `fiber_card_eq_crossBall_card`. S7 (PR #17362) functionally equivalent to #17355's annotation-only fix via `set fwd / bwd with hfwd_def / hbwd_def` + `refine Finset.card_bij' fwd bwd ?_ ?_ ?_ ?_` restructure. Slug graduated; possible follow-up open questions queued in meta.json conclusion.openQuestions (permutohedron/hypersimplex/flow-polytope Ehrhart axiom-free?).", "builtItems": [ - "sum_choose_range: hockey-stick Σ C(m,k) = C(n,k+1) at EhrhartCrossPolytope.lean:118", + "sum_choose_range: hockey-stick \u03a3 C(m,k) = C(n,k+1) at EhrhartCrossPolytope.lean:118", "sum_shift_hockey: sum interchange at EhrhartCrossPolytope.lean:130", "crossEhrhart_expand: Pascal split at EhrhartCrossPolytope.lean:152", "crossEhrhart_succ_d: geometric recursion at EhrhartCrossPolytope.lean:205", "crossEhrhart_d0/d1/n0: base cases at EhrhartCrossPolytope.lean:63-83", "crossEhrhart_pos/mono: structural properties at EhrhartCrossPolytope.lean:95-108", "crossEhrhart_d2: proved via induction using recursion (after succ_d) at EhrhartCrossPolytope.lean:223", - "crossEhrhart_is_poly: descPochhammer-based polynomial of degree ≤ d (PR #16734 Session 2) at EhrhartCrossPolytope.lean:299", + "crossEhrhart_is_poly: descPochhammer-based polynomial of degree \u2264 d (PR #16734 Session 2) at EhrhartCrossPolytope.lean:299", "crossBall: Finset model of cross-polytope at EhrhartCrossPolytope.lean:332", "cweight_le_iff (Session 3): centered-weight bound characterization at EhrhartCrossPolytope.lean:338", "cweight_translate (Session 3): translation bridge for fiber bijection at EhrhartCrossPolytope.lean:346" ], "insights": [ - "S5 (researcher-12, 2026-05-08): The slicing identity `(crossBall (d+1) n).card = ∑ j : Fin (2n+1), (crossBall d M_j).card` factors through `Finset.card_eq_sum_card_fiberwise` (project via `fun y => y (Fin.last d)`) + per-fiber bijection `Fin.init`/`Fin.snoc`. M_j := if j.val ≤ n then j.val else 2n - j.val (= n - cweight(j, n)). Σ over Fin (d+1) splits via `Fin.sum_univ_castSucc`; the last summand is exactly cweight(j, n) since `y (last d) = j` is fixed inside the fiber.", - "S5 (researcher-12, 2026-05-08): The j↔2n-j pairing collapses cleanly: split `range (2n+1) = range n ∪ {n} ∪ Ico (n+1) (2n+1)`; the high half reverses via `Finset.sum_nbij'` with `m ↦ 2n - m`. This produces `(crossBall d n).card + 2 · ∑ m ∈ range n, (crossBall d m).card`, matching `crossEhrhart_succ_d` exactly under the IH. All three pieces total ~90 lines.", - "S5 (researcher-12, 2026-05-08): `Finset.card_eq_sum_card_fiberwise` (verified at `Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean:979`) needs `(s : Set ι).MapsTo f t`; for the slicing application `s := crossBall (d+1) n`, `f := fun y => y (Fin.last d)`, `t := Finset.univ`, the MapsTo is trivially `Finset.mem_univ _`.", - "crossEhrhart_expand proved: L(B_{d+1},n) = L(B_d,n) + 2*Σ_k 2^k C(d,k) C(n,k+1) via Pascal split of C(d+1,k+1) and key identity 1+2*Σ C(d,k+1)C(n,k+1) = Σ C(d,k)C(n,k)", - "sum_choose_range (hockey-stick): Σ_{m y (Fin.last d)`) + per-fiber bijection `Fin.init`/`Fin.snoc`. M_j := if j.val \u2264 n then j.val else 2n - j.val (= n - cweight(j, n)). \u03a3 over Fin (d+1) splits via `Fin.sum_univ_castSucc`; the last summand is exactly cweight(j, n) since `y (last d) = j` is fixed inside the fiber.", + "S5 (researcher-12, 2026-05-08): The j\u21942n-j pairing collapses cleanly: split `range (2n+1) = range n \u222a {n} \u222a Ico (n+1) (2n+1)`; the high half reverses via `Finset.sum_nbij'` with `m \u21a6 2n - m`. This produces `(crossBall d n).card + 2 \u00b7 \u2211 m \u2208 range n, (crossBall d m).card`, matching `crossEhrhart_succ_d` exactly under the IH. All three pieces total ~90 lines.", + "S5 (researcher-12, 2026-05-08): `Finset.card_eq_sum_card_fiberwise` (verified at `Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean:979`) needs `(s : Set \u03b9).MapsTo f t`; for the slicing application `s := crossBall (d+1) n`, `f := fun y => y (Fin.last d)`, `t := Finset.univ`, the MapsTo is trivially `Finset.mem_univ _`.", + "crossEhrhart_expand proved: L(B_{d+1},n) = L(B_d,n) + 2*\u03a3_k 2^k C(d,k) C(n,k+1) via Pascal split of C(d+1,k+1) and key identity 1+2*\u03a3 C(d,k+1)C(n,k+1) = \u03a3 C(d,k)C(n,k)", + "sum_choose_range (hockey-stick): \u03a3_{m ⟨..., by ...⟩`, give the lambda return type explicit annotation. Without it, Lean infers the lambda codomain weakly; the inner `by` block runs with no Fin-bound goal (\"No goals to be solved\" at the `have` line), and downstream `simp only [crossBall, ...]` leaves stray metavariables in the sum body (target `(∑ x, if ↑?m.56 ≤ M ...) ≤ M` with metavar shared across all three arms).", + "Key identity in proof: \u03a3 2^k C(d,k) C(n,k) = 1 + 2*\u03a3 2^k C(d,k+1) C(n,k+1) \u2014 proved by extracting k=0 via sum_range_succ then dropping d+1 term (C(d,d+1)=0)", + "Lean 4.26 notation: \u2211 x \u2208 range n not \u2211 x in range n in theorem signatures", + "Lean Pascal direction: rw [Nat.choose_succ_succ] not \u2190 to go C(d+1,k+1) \u2192 C(d,k)+C(d,k+1)", + "Lean mul_sum direction: rw [Finset.mul_sum] (forward) to expand 2*\u03a3 \u2192 \u03a3(2*...)", + "S6 (researcher-1, 2026-05-08): Mathlib API drift since PR #16734/#17008 \u2014 origin/main no longer builds. descPochhammer is at root namespace (after `open Polynomial` in Mathlib/RingTheory/Polynomial/Pochhammer.lean), NOT inside `namespace Polynomial`. Pattern to flag in code review: any `Polynomial.descPochhammer*` reference is wrong; should be just `descPochhammer*`.", + "S6 (researcher-1, 2026-05-08): When using `Finset.card_bij'` with anonymous-constructor bijection lambdas like `fun y _ idx => \u27e8..., by ...\u27e9`, give the lambda return type explicit annotation. Without it, Lean infers the lambda codomain weakly; the inner `by` block runs with no Fin-bound goal (\"No goals to be solved\" at the `have` line), and downstream `simp only [crossBall, ...]` leaves stray metavariables in the sum body (target `(\u2211 x, if \u2191?m.56 \u2264 M ...) \u2264 M` with metavar shared across all three arms).", "S6 (researcher-1, 2026-05-08): The proofs/.lake self-symlink trap is reproducible across worktrees: `.lake -> /Users/rwalters/GitHub/lean-genius/proofs/.lake`. `rm proofs/.lake` in the worktree before building lets Docker create a fresh `.lake` (mathlib clone ~10 min, cache get ~5 min, EhrhartCrossPolytope compile ~16s after that)." ], "mathlibGaps": [ "(Session 2 resolved: descPochhammer + descPochhammer_eval_eq_descFactorial + Nat.descFactorial_eq_factorial_mul_choose suffice for the polynomial identification.)" ], "nextSteps": [ - "S7 (recommended): Resume the slicing decomposition prototype on top of the now-buildable origin/main. Pull commit `4e9853d0510` from local branch `research/ehrhart-cube-proven-oq-02-fiber-bij-1778229307` into a fresh worktree, run Docker build, fix surfaced Mathlib-drift issues (likely `Finset.card_eq_sum_card_fiberwise` MapsTo coercion, `Fin.snoc_last` arg order, `change`/`omega` interactions on opaque sums).", - "S8 (post-build): once `crossBall_card` sorry eliminated, set `sorryCount: 0`, `status: verified`, `badge: original`. Update `meta.json`, `index.ts`, gallery annotations.", - "S9 (optional, advanced): connect `crossEhrhart d n` to the central Delannoy numbers `D(d, n) := ∑ 2^k C(d,k) C(n,k)`. Mathlib has no `Delannoy` namespace yet; could be a Mathlib upstream contribution." + "Optional cosmetic: replace fiber_card_eq_crossBall_card's set/refine refactor with main's simpler annotation-only style (cosmetic; both compile; see state.md Follow-Up \u00a71).", + "Optional cosmetic: clean up the le_or_lt deprecation warning (use le_or_gt; non-blocking, surfaced as a warning during S7 build).", + "Dedicated-slug candidate (advanced): connect crossEhrhart d n to the central Delannoy numbers D(d, n) := \u2211 2^k C(d,k) C(n,k). Mathlib v4.26.0 has no Delannoy namespace yet; this could be an upstream Mathlib contribution. Spawn as a separate slug rather than continuing this slug, since it is a different research arc (combinatorial identity on lattice paths vs cross-polytope Ehrhart).", + "Dedicated-slug candidates (open questions from state.md Follow-Up \u00a73): permutohedron Ehrhart polynomial axiom-free? hypersimplex \u0394(d,k)? flow polytopes? See conclusion.openQuestions in meta.json." ] }, "tags": [ @@ -83,7 +84,7 @@ "mathlib": [] }, "started": "2026-05-06T13:49:03.933Z", - "lastUpdate": "2026-05-13T13:00:00.000Z", + "lastUpdate": "2026-05-16T14:35:00.000Z", "significance": 6, "tractability": 6, "leanFiles": [