Repository navigation
K2a: initialize and realize single-trial Karger with native deletion #2292
Description
K2a of #2205: replace the initialized single-trial Karger native implementation with the canonical memory/specification stack and K1 realization, deleting the native code it replaces. This follows the released Claude handoff and reuses held #2253–#2255; it is not a parallel memory port. K1 #2287 remains a separate frozen, outside-review dependency. PCP owns the independent K3a bridge in #2289.
Primary worker codex-k2-normalize-20261102, delegated by root, owns isolated branch work/bpl-k2-normalize-20261102 in the private probability lane. Claude’s existing implementation/source histories and the original Karger authors remain credited. The initially authorized leaf is only contract-preserving source normalization: exact existing Memory.scan equations into boundedWhile, and mergeLoop/compactLoop into iterate, reusing canonical held sources and existing loop APIs. It adds no hand-stepped native kernel, second semantics, or replacement memory implementation. Completion of this leaf does not complete K2a.
Full K2a acceptance criteria:
- Initialize the canonical layout from
n :: flattenMatrix W: account for storage, matrix arrangement/copy, degree sums and total, and establish its invariant from the real list input. No assumed prepared invariant may replace initialization. - Realize the existing methods and adaptive contraction client with one fixed emitter/register convention/exchange rate before runtime n, matrix, capacity and width. Include deterministic memory work, query-free/skipped loop control, input installation and halt in the native cost.
- Prove worst-case supported-path halting and at most n−2 primitive random draws, exact joint result/full-memory laws, an actual nontrivial cut witness on every supported result, and success ≥2/(n(n−1)) under the existing positive-min-cut condition. Preserve n=2, disconnected and zero-weight behavior; S=0 contracts without drawing. An expectation bound is insufficient.
- Delete the replaced single-trial native setup/code/proof section and dedicated exact bridge/test glue in the same migration train, updating every client. Preserve or relocate genuinely shared helpers. The remaining amplified/high-probability Karger endpoints and the later K3 native migration stay visible.
- Preserve all current public endpoint/word-width/frame/resource statements unless an exact-resource solution or Samuel’s explicit disposition authorizes a change. Current Program16/22 and numerical instruction constants are not consequences of K1’s existential scratch/exchange theorem; the straightforward held layout also uses two scalar cells beyond the old single-trial writable region. No KargerMinCutAbstract, frame-size or other pinned-statement change is authorized by this issue’s normalization leaf.
- Before a ready deleting PR: strict focused checks, scheduled default all-six/statics, no-impact or authorized abstract/render assessment, preserved source credit, and outside-authoring-fleet correctness/API review of the final public change.
The held sources remain held until a justified deleting train: #2253 layout, #2254 contraction/refinement, #2255 law/expected cost. Their existing outside reviews are reusable after source-identity checks; new native/pathwise claims need review. Canonical K1/loop/frame supplier integration remains a gate. KargerStein.lean still consumes computeDegreesAndTotalAt and contractDownToAt; do not delete Karger/Contract.lean while those consumers remain. K3a retains W₀/part/IsContractionOf and old pathwise contracts; K3 native work still needs a recursive memory-frame stack. This issue does not close #2205 or authorize integration, abstract restatement, or the whole K2/K3 migration.
Activity
SamuelSchlesinger commentedon Nov 2, 2026
Active — primary worker
codex-k2-normalize-20261102, branchwork/bpl-k2-normalize-20261102, private probability lane. Root authorizes only the exact-program normalization leaf now, developing against an ordinary private composition of held #2255 (204a12ab) and reviewed #2270 (15eed512). I will preserve both supplier payloads, stop on substantive conflicts, and bootstrap before focused checks. This supplier composition is not landed or approved as a combined tree. K1 #2287 stays frozen; no abstract, frame, endpoint or hand-stepped kernel changes are in this leaf.SamuelSchlesinger commentedon Nov 2, 2026
codex-k2-normalize-20261102: the checked intermediate normalization leaf is d2be67d5a.scan_eq_boundedWhile,mergeLoop_eq_iterateandcompactLoop_eq_iterateprove exact free-program equalities while leaving the held implementations unchanged. The default six gates pass on that unchanged source, as do compiled tidy-surface, changed-file and hygiene checks. Concrete clients check early-exit query history, zero cutoff and a genuine triangle cut witness. This development supplier composition is not landed or independently approved as a combined tree; source and outputs are now clean/idle for coordinator review and placement.This completes neither K2a nor a native endpoint: input initialization, native realization/pathwise budgets, deletion and the fixed-register/frame/abstract disposition remain open as stated above. No abstract or pinned resource statement changed; K1 #2287 remains frozen awaiting outside review. I am an author and have not approved, opened a new PR for, or integrated this leaf.
SamuelSchlesinger commentedon Nov 2, 2026
Frozen PRIVATE deterministic-wrapper milestone — worker
codex-k2-contract-realization-20261102, branchwork/bpl-k2-contract-realization-20261102, checkpointb6da5e9e0d48acf663a675f5ad111842be937fa3(sole child of frozenae820f6d). Writer and focused producers are closed; source is not published.The new contract-realization leaf composes the ORIGINAL
mergeDegrees,compact/shrinkandcontractthrough existing certificates. It retains exactlyInvplus distinct valid vertex indices, derives reached arithmetic/history obligations, and reuseswp_contractfor full source memory/frontier, footprint frame, graph transform and invariant. The uniform native bound isC*(initial size+1)BODY instructions with a full-data R=0 point law; the ORIGINAL7*k+7MEMORY charge remains a separate currency. Nonedges require no positive-weight premise.Strict focused source/new and earlier clients passed (6,286 jobs); targeted hygiene, canonical imports and focused doc-name/concrete-test checks passed. One emitter handles three layouts/widths: triangle last-slot, weighted nonedge compaction with inactive/exterior markers, and the two-vertex zero-total graph. Alias/out-of-range/corrupt/non-fitting-total cases remain original-domain negatives, not RAM-fault claims. Complete leaf/combined forward-and-inverse checks preserve all prior provider bytes, pins, manuals, abstracts and refs; the immutable evidence packet has been handed to LogsQ.
No full-six grant/run, API/math or held-supplier approval, PR/publication, randomized driver/sampling, initialization/install/halt, legacy deletion, old 16/22-register/clock/space/frame or abstract restatement is claimed. This is the bounded deterministic helper milestone; full K2a/K3/#2205 acceptance remains open. Further implementation awaits coordinator disposition. Original source credit is retained; this new authoring is AI-assisted Codex work, which I cannot approve.