research(ehrhart-cube-proven-oq-02): S8 STATE-SYNC — nextSteps cleanup + nextAction realignment + sessions/ bootstrap + knowledge.md handoff (doc-only)

[rjwalters]

Summary

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 research(ehrhart-cube-proven-oq-02): S7 — close crossBall_card via slicing decomposition (build verified) #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/<slug>/state.md (head + S8 entry)
• src/data/research/problems/<slug>.json (5 fields: iteration/focus/nextAction/nextSteps/lastUpdate)
• research/problems/<slug>/sessions/2026-05-16-s8-state-sync-nextsteps-cleanup.md (NEW ~218 LOC)

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).

Test plan

• python3 -c "import json; json.load(open('src/data/research/problems/ehrhart-cube-proven-oq-02.json'))" → JSON OK
• git diff --stat origin/main shows exactly 3 paths
• No .lean files touched
• No problem.md / knowledge.md edits (knowledge.md staleness handoff in S8 memo §3)
• No leanFiles[0] edits (already accurate: 720/22/0/0/2 verified at S8 author time)
• No Docker build needed (zero proof delta)
• No conflict (no open PRs for this slug)
• Verification commands in S8 memo §2 re-runnable on origin/main

Out-of-PR side-effects

• claim-problem.sh update ehrhart-cube-proven-oq-02 completed re-run
  (pool gitignored; second update for this slug — research(ehrhart-cube-proven-oq-02): STATE-SYNC — top-level JSON + state.md to S7 COMPLETED (doc-only) #18953 already ran
  an implicit update, but pool sync script appears to re-mark
  long-completed slugs as available).
• claim-problem.sh release after PR.

🤖 Generated with Claude Code