Repository navigation
K3a: derive Karger–Stein recursive bounds through a specification bridge #2289
Description
K3a of #2205: transfer and finish the Karger–Stein specification bridge, using the released Claude design and recommended route B. This is a bounded bridge-and-delete milestone, not the K2/K3 native realization migration.
Primary worker codex-k3a-pcp-20261102 owns the released implementation on isolated branch work/karger-stein-k3a-pcp-20261102 / Extra worktree .worktrees/karger-stein-k3a-pcp-20261102. The released feat/karger-stein-bridge remote has no commits; the handoff records design only. Start from outside-reviewed #2286 at 92893fbe; LogsQ retains that PR's refresh/integration. Preserve the existing library authors and credit the ksbridge-claude-015dlg8k design. K1/#2287 remains BPL's separate ownership; shared tooling remains Crypto's.
Acceptance criteria:
- Define the recursive FastCut oracle client using the existing contraction specification and independent
evalWithanswers. Establish its exact law, cut-support and success/amplification results by reusing the existing contraction and probability APIs. - Thread exact result laws through the existing frame-loop machine, with pathwise time and random-call bounds retained. Derive the existing public program statements from the specification and delete the replaced machine-state probability reasoning in the same change.
- Follow route B: retain
W₀,partandIsContractionOfwhere needed by existing execution/bridge clients. Preserve public theorem meanings, program definitions, frames, encodings, dirty-memory hypotheses and worst-case supported-path halt/random-call budgets. No expected-cost substitute or second native model. - Keep curated abstracts unchanged without Samuel's approval. Demonstrate nonvacuous existing weighted/zero-weight clients, strict focused validation, a scheduled full-six run before a ready PR, and outside-authoring-fleet review of public changes.
Remaining objective: native K2/K3 must still absorb the held memory sources, use K1's exact laws/pathwise budgets, implement the explicit recursive frame stack, and delete the corresponding hand-stepped native modules. This milestone does not claim that endpoint, arbitrary-client automation or the broader #2205 gate complete. The queue witness is finished and remains with #2284/1730.
Transfer records: state, drafts and release, final transfer, full plan.
Activity
SamuelSchlesinger commentedon Nov 2, 2026
Active claim — primary worker
codex-k3a-pcp-20261102, branchwork/karger-stein-k3a-pcp-20261102, isolated Extra worktree.worktrees/karger-stein-k3a-pcp-20261102. I read the transfer records and exact outside review of #2286; the released K3a branch contains no pushed implementation. Starting from92893fbe, I will follow route B, retainW₀/IsContractionOfand public pathwise halt/random-call contracts, and preserve all source authors and the released Claude design credit. LogsQ owns #2286 integration; K1/#2287 is BPL's separate dependency. First checkpoint: reusable PMF/loop-law interfaces and the exact FastCut specification, then the machine-law bridge with replaced probability reasoning deleted. Abstracts remain unchanged; native K2/K3 and the broader objective remain open.SamuelSchlesinger commentedon Nov 2, 2026
Active — worker
codex-k3a-pcp-20261102onwork/karger-stein-k3a-pcp-20261102. The recursive specification now checks its exact branch law, original-graph cut support, depth success bound and independent amplification bound; connected-triangle and zero-weight examples pass focused checks. Native base-case and branch contraction now expose exact laws, with the existing bridge-facing specifications derived from them. Next: compose the recursive native segments and replace the remaining machine-local probability proofs. The existing abstract statements and strict native time/random-call bounds are unchanged; this does not complete the later K2/K3 native realization objective. Parent #2286 has actually landed, and its integration/cache remains with LogsQ.SamuelSchlesinger commentedon Nov 2, 2026
Active/frozen validation checkpoint —
codex-k3a-pcp-20261102has completed the specification/native law bridge and deleted the replaced machine probability recurrences. The existing native and unchanged abstract bridge clients pass strict focused checks; the new triangle, recursive seven-vertex, zero-weight and paid-loop fixtures pass too. Static guards retain all 41 native definitions, every retained theorem signature and all abstract sources. The unused ProbComp-specific event module is replaced by the shared PMF rule; compiled output-law transport is shared with basic Karger.Local checkpoint
7c168e659ordinarily merges the actually landed #2286 parentb1c5ef1e, preserving all unrelated main entries and pins. The branch remainswork/karger-stein-k3a-pcp-20261102; full-six capacity is requested before publication/outside review. Source is frozen while I also handle coordinator-assigned read-only preservation audits. K2/K3 memory-oracle native realization and the broader #2205 objective remain open.SamuelSchlesinger commentedon Nov 2, 2026
Milestone completed — worker
codex-k3a-pcp-20261102: PR #2296 landed asb32952d0on 2026-11-02 at 19:29:45 UTC, and bounded #2289 completed automatically. Independent source/manual review, fresh source/MQ/main validation and usable public-cache publication are complete; the canonical PR evidence record owns the exact results and limits.The completed deliverable is the Karger–Stein specification-law bridge with the existing native correspondence. K2/K3 memory-oracle contraction, randomized adapters, explicit recursive frame-stack migration and broader #2205 remain open. This update performs no new closure, review request, source or queue action.
SamuelSchlesinger commentedon Nov 2, 2026
Awaiting independent preservation/manual review — original worker
codex-k3a-pcp-20261102, refresh sessioncodex-k3a-main-pcp-20261102, branchwork/karger-stein-k3a-main-pcp-20261102in the new isolated no-output worktree. PR #2296 retains its approved publicc2c8441asource and validation. The local source-only ordinary refresh isc292a01ebover fixed actual3d1370a6, with separate manual-only child6549fd3a9; source/index are clean and frozen, and LogsQ has the complete preservation/render packet for non-author review.The PR’s existing worker record owns validation and manual-impact details. No Lean/full run, canonical publication, retarget or queue action occurred; the old lane/public refs are unchanged. LogsQ retains integration and short-core #2281/#2300 priority. K2/K3 and broader #2205 remain open.
refactor(Algorithms/WordRAM/Karger): derive Karger–Stein bounds from …