Repository navigation
feat(wordram): execute sparse pruned tensor queries #1526
Description
Native implementation milestone of #1394, above the complete finite pruning/thin-product mathematics #1459/#1463 and native encoded arrays #1493/#1520. The full ordinary native 3SUM endpoint and exponent1.9992 remain open.
Personally implement the complete native pruned-query evaluator in the existing continuation checkout. Inputs are the two read-only flat ten-symbol encoding arrays from #1520 and an explicit finite list of output-string codes. Compute every child query set, membership/deduplication, prefix/suffix index, term dispatch, recursion/stack decision, encoded product and returned sum with fixed finite native code. Reuse the existing mathematical Pruned.result and contributing-leaf/passed-set bounds; no source Light machine, supplied recursion/layout certificate, assumed fast routine or time/solver field.
Acceptance: fixed finite register count/program independent of depth, query count and word width; actual State.init input and flat halt clients; every requested output equals the existing Pruned.result (and the encoded bilinear product), including empty/zero-depth and repeated-query behavior. Explicit read-only producer/consumer arrays, scratch/frame/fit guarantees, actual stack/control/index work, and a charged bound polynomial in depth times the supplied query count plus the proved visited-leaf/passed-set quantities. A full ten^L scan for every query/tile does not meet the sparse acceptance. All initialization/clearing, deduplication, arithmetic, calls and final reporting must be charged, with enough input-derived width to execute each instruction. Derive fits from ordinary bounds, not an all-state-fit or execution hypothesis.
Coordinate the exact interface with #1523 band preparation: canonical leafIndex ordering, canonical signed words, encoded-array base/lengths, numerical output-string/query encoding, memory footprint and repeated-call scratch contract. Keep producer modules/build outputs separate. A timestamp invariant is permissible only when established by actual initial memory and preserved by actual runs; it must not hide precomputed query sets or free dense per-call clearing.
Provide positive/negative/empty/depth-zero/mixed-query tests, real State.init runs, nonvacuous fit/boundary/frame clients, and tests of shared/deduplicated work. All six strict gates, full citation-aware hygiene and actual-base changed-file/name/diff checks; checked pinned-source quotation and quantifier/model/encoding/resource mapping, source credit, reuse rationale, abstract assessment and independent correctness/API review before publication, with outside coordinator review requested before integration.
Source context (paraphrase): direct selective adaptation of anthropics/formal-math@16a5ce4, ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/{Recursion,Memory,Contract,Slices,Union,Restrict}.lean and existing finite Sec2/Lemma10 mathematics. Native implementation and actual charged bound must be rebuilt against library APIs. Preserve source credit and Complexity-to-Cslib upstreamability.
Owner: worker codex-three-sum-continuation-t3-3dda8289, implementing personally in its existing isolated checkout on work/three-sum-native-pruned-query-20261028 from #1520 head3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6. No additional implementation agent for this scope. #1523 remains with its existing band worker; root owns native Convolution host #1524 and final ordinary composition. Chan–He #1446/#1482/#1512 and packing owners are unchanged. Sparse-product/Exact Triangle composition follows this component, and the improved source branch is still required for1.9992; a simpler1.9993 endpoint is a milestone only.
Activity
edemaine commentedon Oct 28, 2026
active — implementation worker
codex-three-sum-continuation-t3-3dda8289claims #1526 after checking the open native-pruned/query issues and current reviews of the existing stack; no competing native evaluator claim or newly routed review finding was found. I am implementing personally in the existing isolated t3-3dda8289 checkout, branchwork/three-sum-native-pruned-query-20261028, from #1520 at 3b9234d. No additional implementation agent is assigned. Producer/consumer protocol is being agreed with the #1523 worker; root #1524 Convolution and Chan–He/packing/frontend ownership are unchanged.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289, personal #1526 implementation: fixed native DFS/deduplication code is written; actual initialized-input regressions passed for empty/repeated/mixed depth-0/1/2 requests, both signs and an outside-frame sentinel. Checked proofs cover numerical child-set agreement/range, call-count versus passed-set total, nine-instruction timestamp insertion and the charged power loop. General controller execution, fits/frame and sparse potential accounting remain in progress; no PR or full native endpoint is claimed. #1523 band preparation retains its worker; root #1524 Convolution and Chan–He/packing/frontend scopes are unchanged.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289: the complete native timestamped query scan, sparse accumulator clear, frame loader and signed arithmetic/return kernels check locally; the general controller invariant and initialized evaluator/time theorem remain unfinished. Current source is preserved in a local WIP checkpoint while I address the bounded #1496 review delta and run its coordinated all-six slot. #1523 producer ownership is unchanged; full native sparse/ET composition and #1394 remain open.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289: pushed an explicitly partial native checkpoint 87ff44c7a onwork/three-sum-native-pruned-query-20261028. It includes charged native scan, sparse initialization, signed accumulation, frame transitions, query coding and timestamp bounds; the commit description owns validation limits/evidence. The general controller composition, actual initialized full-evaluator theorem and final sparse charged bound remain unfinished. No PR or all-six component claim; complete sparse/ET and ordinary 3SUM composition remain under #1394.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289, branchwork/three-sum-native-pruned-query-20261028: preserving the charged native controller/phase checkpoints while finishing the publication-priority #1523 reuse repair. Actual root-frame stores now have a checked 11-instruction theorem; the full recursive controller/frame/epoch/cost composition is still open. No PR or full-component completion claim. Root #1532 owns raw 0/1 matrix preparation; the eventual product consumer will charge actual doubling during its copy into signed band inputs. Full #1394 remains open.feat(wordram): checkpoint actual pruned-query root-frame stores
feat(wordram): checkpoint complete native pruned-controller phases
edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289: 79c9407a6 preserves the complete native controller-phase proofs and kernel examples on the owned branch. Root setup/reporting, terminal/internal entry, both computed child cases, returned-child accumulation and final return all have clean targeted Lean MCP diagnostics with explicit charged costs and frames. General recursive composition over all depths, initialized-input/flat clients and the total bound are still open; there is no component PR or all-six claim. I am arranging the explicitly requested exact-head #1537 review, then resuming that recursion proof. Whole #1394 remains open.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289, branchwork/three-sum-native-pruned-query-20261028: after the priority #1464 repair, the native node footprint and scan-read/injectivity lemmas now check. Partial-term trace potential and a single original-parameter magnitude/address envelope also check; the signed-fit helper is reused unchanged from #1552. All-depth node induction and complete initialized-input/time/width composition remain open, so no component PR or all-six claim. The prior complete native phase proofs and concrete kernel clients are preserved at 79c9407a6. No aggregate is running here; the shared queue remains #1545 → native #1537 repair → root #1546. Full #1394 remains open.feat(WordRAM): prove all-depth pruned controller execution
edemaine commentedon Oct 28, 2026
Active — codex-three-sum-continuation-t3-3dda8289. Checkpoint a93c0214e includes the checked all-depth native controller induction: computed child lists, existing
Pruned.resultvalues, signed fits, frames and trace-based charged continuation. Root loop exit discharges that continuation. Targeted library diagnostics are clean; the existing VM test commands are still elaborating, so no final test/all-six claim. Next: initialized input, root-list/report/flat-run composition and complete component validation. Aggregate gates remain held for root’s slot. No PR or whole #1394 endpoint claim.feat(wordram): complete initialized sparse pruned-query execution
edemaine commentedon Oct 28, 2026
Active — codex-three-sum-continuation-t3-3dda8289. Complete implementation candidate pushed at 0c2e0ebea: actual initialized/flat runs and charged halt, bilinear-product specialization, reusable pointer/epoch kernel, positive input-derived physical-width threshold, frames and sparse leaf-based instruction bound. All six strict gates pass together, including Smoke/global Axioms; final hygiene and actual-base changed-module/test/name/diff checks pass. Evidence and limits are recorded in the commit description. Handing the exact candidate to root for fresh independent correctness/API/source-mapping review before PR publication. No PR opened or whole #1394 completion claim. Global slot is being returned directly to root after the final metadata readout.
edemaine commentedon Oct 29, 2026
Fresh nonauthoring technical review by
codex /root/pruned_native_reviewat 0c2e0eb (tree bd6e74cce28dbd16c90291b847dac1a311402510), against3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6: no blockers or nits found. This is new substantive native code; this within-fleet review is not outside-coordinator, human or integration approval.The review checked actual filtering/deduplication, child/return invariants and root-exit discharge, canonical signed arithmetic, same-y State.init/prefix/halt/readback, source/output frames, the sparse charged bound and admitted physical width. Ready/progress/result assertions contain no hidden execution/time certificates. The callable kernel's explicit output/workspace frame and returned epoch bound support later calls; preserving a shared catalogue also requires disjoint output placement. Checked witnesses include negative/empty/zero-depth and repeated/shared requests, depth-two [5050,460,55,1,5050], sufficient/failing widths and the nonzero-epoch sentinel client.
Finite Full/Pruned code matches previously reviewed core code outside comments; encoder blobs match reviewed #1520. Signed/Fits is the unchanged #1552 blob. Both displayed quotations match the actual pinned Anthropic Git blob and locators. Source/model/index/cost distinctions, credit and abstract no-impact are accurate. Component width is logarithmic in explicit budgets; whole-3SUM width/asymptotic composition and the native ET/1.9992 endpoint remain open.
Read-only source review: no builds or elaboration rerun, no source/refs modified. It reuses the exact-tree six-gate/static evidence in the candidate commit description. Outside review remains required after publication.
edemaine commentedon Oct 29, 2026
Awaiting outside review/integration — PR #1562 publishes the frozen 0c2e0eb candidate. The exact head/base/draft and reviewed tree are verified; the PR links the fresh technical review and owns final source/model/validation evidence. Samuel is formally requested. Continuation remains implementation owner and retains the downstream queried-product/backend scope. The component is complete for its stated contract; full #1394 remains open.
edemaine commentedon Oct 29, 2026
Active — codex-three-sum-continuation-t3-3dda8289, addressing the outside FINAL findings on the original #1562 branch by ordinary fast-forward. Scope: broken roadmap references, admitted signed
runs_bilinearclient, internal stage-API documentation, topic-module placement rationale, and extension of existing #1553 power consolidation. Native programs/public statements stay unchanged; targeted checks then all six/static and identity audits precede publication. Parent directly assigned the sole audit slot; it returns directly to root after final processes finish. #1561 is preserved at 7772a3497, with its remaining proof gap explicit.fix(wordram): address pruned-query review findings
edemaine commentedon Oct 29, 2026
Awaiting focused outside review — codex-three-sum-continuation-t3-3dda8289 repaired #1562 by normal fast-forward at ce77926c3. Repair/validation record and delta request. The sole global/static slot was explicitly returned directly to root; no audit remains here. #1561's separate checkpoint is preserved. The full #1394 endpoint remains open.
SamuelSchlesinger commentedon Oct 29, 2026
Completed bounded milestone: native pruned-query computation, duplicate-preserving recursion, initialized/callable execution and sparse instruction/resource bounds. Landed through #1615; verified on main with accepted source and credit intact. The broader #1394 objective, ET input adaptation, fast backend and full 1.9992 endpoint remain open.
feat(Schonhage): execute native queried thin matrix products (cslib-c…
feat(WordRAM): compile memory windows for callable thin products (csl…
feat(ExactTriangle): call queried products from prepared native recor…
feat(WordRAM): recover witnesses for native ET record products (cslib…
feat(WordRAM): decide ExactTriangle with the fixed-prime native solver (