[edemaine]

Landed-parent refresh at 0cba85195003951aa1723c47d230c154455c746c ordinarily merges actual main 21a3641b after #1520 landed. All twenty-nine own library files and the test remain byte-identical to reviewed 82f86fec; all fourteen #1520 payload blobs retain actual 8527c1f4 code. Main’s tidy baseline, default Parameters proof and zero allowances are preserved exactly, together with source citations and the complete unrelated UPSTREAM tail.

Only the three own-band progress/credit additions conflicted. The resolution preserves them separately from main’s encoder milestone; removing those additions reproduces each entire main NOTICE/ROADMAP/UPSTREAM file byte-for-byte. Cache bootstrap, canonical aggregate checks (2687 modules), full hygiene and whitespace checks pass; generated imports needed no change. Existing mathematics/API review is reused, with no additional local proof build or selected-abstract impact. Fresh automatic full PR CI is running and independent integration delta review is requested. OpenAI Codex coordinator coordinator-codex-queue-20261028-tests-b performed this refresh, preserving original authorship and open #1394 scope.

Implement complete native shared-band preparation for #1523, using the #1520 encoder. The fixed 96-register standard-WordRAM program reads actual L,m,N headers and signed matrices, computes both subset tables and a deterministic existing Layout, prepares every padded band, calls the unchanged encoder once per row/column band, and copies every output into a shared catalogue. It snapshots and restores the full original input, including native header zero. General calls preserve arbitrary caller memory outside the explicit work frame.

The complete charged bound is 4096*(L+1)*(1+N*4^m+2^L+2*numBands*10^L), plus one halt. At L=19m, N≥(4^m)^18, including halt, it is at most 81920*(L+1)*N²/(4^m)^(1/18). This completes the bounded preparation component only; pruned queries, products, native Chan–He preprocessing, Exact Triangle and whole ordinary 3SUM composition remain in #1394.

Original implementation validation: head 6603615; tree 4807cb971cf8030f70df67e5e8fa13947dcbd202.

Base: t3/native-shared-tensor-encoding / #1520. No changes to the encoder, parent mathematical modules, Chan–He, packing, frontend or query-owner files. The optional enum/equivalence documentation cross-reference requested on #1520 is in this PR's new band module only. Preserve the unchanged encoder outside-review evidence: #1520 (comment) (exact 3b9234d, final/no blockers; agent review, not human approval).

Exact pinned source and mapping

Read-only source verified locally at anthropics/formal-math@16a5ce4. These are quotations from the pinned Lean source, not newly attributed quotations from the paper.

AllBands.lean, lines 230–239:

def EncodeBandsLSpec (lim : Limits) (P : Program) (c : ℕ) : Prop :=
  ∀ (p : Par) (hmL : p.m ≤ p.L) (x : BandsArgs) (aX : ℕ) (μ : ℕ → ℤ)
    (X : Matrix (Fin p.N) (Fin (ThreeSumApsp.D p.m)) ℤ) (V : ℤ),
    BandsPre lim p μ x Spec.phiFlat V → MatAt μ aX X → aX + p.N * p.D ≤ x.enc →
    (∀ i j, |X i j| ≤ V) →
    ∀ d, d + (p.L + 2) ≤ lim.depth → Meets lim P pEncodeBands d (x.vals p 0 aX p.D 1) μ
      (c * (p.nB * (p.T + bandArrayShape p) + 1)) fun _ μ' =>
        (∀ β < p.nB, Seg μ' (x.enc + β * p.T)
          (Spec.arrT (encodingL (bandArrayL (Spec.stdLayout hmL) X β)))) ∧
          SameOutside μ μ' x.enc (x.zs + p.S7 - x.enc)

AllBands.lean, lines 262–271:

def EncodeBandsRSpec (lim : Limits) (P : Program) (c : ℕ) : Prop :=
  ∀ (p : Par) (hmL : p.m ≤ p.L) (x : BandsArgs) (aY : ℕ) (μ : ℕ → ℤ)
    (Y : Matrix (Fin (ThreeSumApsp.D p.m)) (Fin p.N) ℤ) (V : ℤ),
    BandsPre lim p μ x Spec.psiFlat V → MatAt μ aY Y → aY + p.D * p.N ≤ x.enc →
    (∀ i j, |Y i j| ≤ V) →
    ∀ d, d + (p.L + 2) ≤ lim.depth → Meets lim P pEncodeBands d (x.vals p 1 aY 1 p.N) μ
      (c * (p.nB * (p.T + bandArrayShape p) + 1)) fun _ μ' =>
        (∀ β < p.nB, Seg μ' (x.enc + β * p.T)
          (Spec.arrT (encodingR (bandArrayR (Spec.stdLayout hmL) Y β)))) ∧
          SameOutside μ μ' x.enc (x.zs + p.S7 - x.enc)

BandArrayFacts.lean, lines 107–113:

/-- The number of the block of rows of the matrix `X` (`side = 0`), or of columns of the matrix `Y`
(any other side), for the block product `(g, h)`. -/
def blockNo (g h : ℕ) : ℕ := A.β * A.p.K0 + if A.side = 0 then g else h

/-- The number of the row of `X` (or column of `Y`) for the block product `(g, h)` and the row `r`
of the block. -/
def rowNo (g h r : ℕ) : ℕ := A.blockNo g h * A.p.N0 + r

The mathematical arrays and encodings are reused directly. In BandPreparation.runs, arbitrary natural L,m,N satisfy m≤L; arbitrary signed X : Matrix (Fin N) (Fin (D m)) ℤ and Y : Matrix (Fin (D m)) (Fin N) ℤ have a common nonnegative entry bound A. Every band index is quantified below the computed numBands, and every original Leaf L is quantified. The pure catalogueValue_left/catalogueValue_right bridges prove agreement with existing encodingL/encodingR on existing bandArrayL/bandArrayR. MaskTable.layout replaces the source's stdLayout with an explicit deterministic instance of the unchanged Layout: the first K0*K0 size-m masks in ascending numerical order, with row-major pair rank. The native table scan actually computes this choice; it is not a supplied certificate or choice oracle.

The quoted source entry uses Light machine limits, a program map, supplied table/argument predicates and a depth bound. This PR does not import those models, predicates, call semantics or time claims. BandPreparation.exec proves the actual standard unsigned Code execution from ordinary register/header/memory values. exec_input and runs instantiate it with the concrete State.init list, and expose both the actual final memory in a charged prefix Runs and its next charged halt. runs_thin connects that actual flat execution to the saving above. No solver, callback instruction, assumed execution or time certificate is a hypothesis.

Input/output encoding is canonical Signed.encode; source magnitude width is w, target word width is w+2. All intermediate signed bounds reuse the unchanged native encoder's proof from 7^L*A < 2^(w-1). The existing actual signed add/subtract blocks cost at most 15/17 target instructions, respectively, and those costs are included in the encoder's 240*(L+1)*10^L cost, with no whole-program compiler assumption. The explicit numerical wordBudget must fit target width. Header loads, five power loops, both mask/popcount scans, incremental square-root loop, dense inverse initialization, every band decoder/lookup/guard/address, full input copying/restoration, all encoder calls, catalogue copies and loop controls are charged. Intermediate unsigned fits are derived from that budget and actual bounds guards; no structure bundles an all-state fit hypothesis. width_exists and the symbolic positive-depth thin native-run test prove simultaneous satisfiability.

Each tile uses its two shared band inputs through tileInputBases; tile_input_values reuses the existing mathematical tile set and both proved output predicates, and table_word_layout identifies retained native table words with the actual computed layout. catalogueAddress L m N side β leaf is catalogueBase + ((if side then numBands else 0)+β)*10^L+leaf. Leaves retain authoritative Encoding.leafIndex: LSD-first coordinates, row-major P terms at digits 3*i+j, P0 at digit 9. Original scalar/matrix input is restored; the general frame permits any read-only query region and future scratch outside [inputEnd,memoryEnd), without requiring unrelated words zero or header zero equal a standalone list length. Final inverse and forward tables are retained and specified by runs.

Reuse, validation and scope

Reused the unchanged standard WordRAM, structured loop/rename APIs, existing copy routine, signed kernels, shared encoders, mathematical Layout, padding/bands, encoding definitions, Mathlib finite equivalences/sorted sets and thin-regime encoding bound. New helpers are in small topic modules: native power; ordered-filter enumeration; positional finite digits; row-major list indexing. The finite-digit bridge reuses the existing Nat.ofDigits_ofFn_eq_sum by publicly importing the radix module; the duplicate tuple-sum lemma found in review is removed, with the existing name, proof and source credit retained in that module. The native mask/inverse-table algorithm, direct base-seven decoder and memory/cost composition proofs are original; only the band organization and mathematical meaning are selectively adapted. Anthropic, PBC credit and the pinned source are retained in the adapted module header and NOTICE. Complexity→Cslib import-prefix rewriting remains the only upstream namespace change.

Tests evaluate the actual native interpreter on zero/positive depths, empty matrices, negative/zero data, padding/multiple shared bands, computed selected/unselected masks, outside sentinels and an execution width boundary. Kernel-checked concrete full-program clients bind their actual final memory to prefix Runs plus charged halt, including a nonzero unrelated native header and outside query sentinel. A symbolic positive-inner-depth family establishes the full native thin execution without enumerating huge matrices.

Validation at 6603615: all six strict gates, global Axioms, full citation-aware hygiene (--check-simp), fresh actual-base changed-module lints (29 library modules and one test), strict PR-name audit and diff checks pass; the final payload tree is 4807cb971cf8030f70df67e5e8fa13947dcbd202. Programs, public endpoint statements and tests are byte-identical to reviewed cb261f6; the sole library delta consolidates the duplicated digit lemma. The author's original all-six/static evidence remains in the implementation handoff.

Independent non-authoring correctness/API/source-mapping review found only the duplicate lemma at cb261f6, verified all three pinned quotes, and found no other execution/frame/fit/cost/mapping blockers. That full coverage is retained. Focused final one-file delta review: approve, no findings. These are inside-fleet agent reviews, not outside-coordinator or human approval; outside coordinator review is requested before integration.

Abstract assessment: no impact. The curated catalogue contains no affected selected theorem, model or abstract; this is a bounded component under the still-open whole 3SUM endpoint. No new headline or PDF changes.

AI assistance: implementation and proofs by Codex (codex-native-bandprep-t3-03b600bd), under delegating-worker coordination. The bounded reuse fix and final validation are by codex-three-sum-continuation-t3-3dda8289. Review evidence is linked above.

Closes #1523; part of #1394.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at 66036150a12046b29986d8f108c0afaf49d01c61

Full review of this PR's own layer (3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6..66036150a12046b29986d8f108c0afaf49d01c61, base t3/native-shared-tensor-encoding, both commits). The #1523 "independent non-authoring" reviews linked in the description come from the author's own fleet, so they do not count as independent coverage. This review is from outside that fleet. No blocking findings.

What the native program computes. BandPreparation.program is one fixed Code .standard 96 (program_length_le ≤ 16384, not_readsWidth). On input L :: m :: N :: X ++ Y (row-major, Signed.encode), it:

• loads the headers and computes 4^m, 3^{L-m}, 2^L, 7^L, 10^L with the new Power.program;
• snapshots the complete prefix [0, inputEnd);
• counts the size-m masks with a division-based popcount and takes K0 = ⌊√count⌋ by a squared-comparison loop;
• computes numBands = ⌈N/(K0·N0)⌉;
• writes a dense inverse table (0 = unselected, rank+1 = selected) and a forward table holding the first K0² valid masks in increasing order;
• for each row band, then each column band:
  • decodes every base-7 index into mask, base-3 offset and base-4 offset;
  • looks up the block pair, g = rank / K0 on the left and h = rank % K0 on the right;
  • checks that row/column < N before any row-major multiplication, and reads from the snapshot;
  • calls the unchanged feat(wordram): implement shared tensor encodings #1520 encoder once and copies its 10^L leaves into the catalogue;
• restores the snapshot.

runs ties the actual State.init run to the following:

• a pre-halt state with n ≤ timeBound and the halt charged;
• the catalogue equal to encode (encodingL/R (bandArrayL/R (MaskTable.layout hm) X/Y β) τ) for every β < numBands and every Leaf L;
• both table contents;
• frame equality outside [inputEnd, memoryEnd).

exec additionally allows an arbitrary header 0 and arbitrary outside memory.

Cost and width.

• timeBound = 4096(L+1)(1 + N·4^m + 2^L + 2·numBands·10^L), plus the halt.
• runs_thin: at L = 19m and N ≥ (4^m)^18, the bound is ≤ 81920(L+1)N²/(4^m)^{1/18}. It reuses the existing encodings_total_le and costs the halt as n+1 ≤ 2·timeBound.
• Width premises are 0 < w, 7^L·A < 2^{w-1} (signed source width w, target w+2), and Fits (w+2) (wordBudget L m N). That last one is an ordinary numeric inequality with no all-state fit hypothesis. width_exists shows the premises can hold together.

Checked instances.

• L = m = 0, N = 1, X = -3, Y = 2: D 0 = 1, K0 = 1, bandSize = 1, one band each side, one leaf. The catalogue holds encode (-3) = 7 and encode 2 = 4, as in the test client.
• Edge cases:
  • N = 0 gives numBands = 0 and only tables.
  • m ≤ L gives K0 ≥ 1, so the bandCount division never sees 0.
  • Unselected masks read 0 via the explicitly zeroed inverse table.

Reuse. The PR reuses the existing Layout, K0, N0, D, numBands, bandArrayL/R, encodingL/R, Encoding.leafIndex/program, ArrayCopy and encodings_total_le. The second commit removes the duplicate tuple-digit lemma in favour of the existing Nat.ofDigits_ofFn_eq_sum. I found no existing Layout instance, popcount or register-exponent power routine in the base. MaskTable.layout is needed, because the source's stdLayout has no counterpart here.

Tests. ComplexityTests/SchonhageBandPreparation.lean checks real behaviour:

• #guard interpreter runs cover empty, zero-depth signed, multi-band and padded cases, compared leaf by leaf against the mathematical expected;
• the mask table, an outside sentinel and an exact width boundary (6 fails, 7 succeeds; Fits 13/14 on wordBudget);
• three kernel-checked clients of runs/exec, including a nonzero header 0 and a symbolic thin family.

This meets item 8.

Source quotations. All three code blocks in the description match anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5 byte for byte:

• Programs/Sec2/Theorem5/Encode/AllBands.lean lines 230–239 and 262–271;
• BandArrayFacts.lean lines 107–113.

The mapping is correct:

• blockNo = β·K0 + (side ? h : g) and rowNo = blockNo·N0 + r match readCell;
• the source's Seg μ' (x.enc + β·T) (arrT (encodingL …)) becomes the catalogue equation, with stdLayout replaced by MaskTable.layout;
• the Light machine, Meets, depth and table-predicate hypotheses are replaced by actual native proofs.

Nits / follow-ups (optional, non-blocking)

• Cross-stack duplication after both stacks land. This PR adds Power.program and an inline integer square root (rootCode). The sibling Chan–He stack (feat(wordram): compute Chan–He parameters from native input #1469/feat(wordram): implement the complete native convolution host #1531) has ChanHe.Parameters.power (unrolled for a fixed κ) and Algorithms/WordRAM/NatSqrt.program. Neither is on main or in this PR's base, so this layer is not a duplicate. Once both are on main, consider routing rootCode through NatSqrt and, where it fits, the Chan–He power through Power, so the library has one native isqrt and one power routine.
• Untested block-pair decoding. Every concrete test has K0 = 1, which means only (L,m) ∈ {(0,0), (1,0), (1,1), (2,1)}. So the rank / K0 vs rank % K0 split is covered only by the general proof, never by a concrete run with K0 ≥ 2. The smallest such case is C(L,m) ≥ 4, e.g. L = 4, m = 1. If an interpreter #guard at L = 4 is affordable, it would exercise that path.

Limits. I did not build locally; ci-checks and check-title pass at this head. I read the program, the endpoint statements (exec, runs, runs_thin, width_exists, the catalogueValue_* bridges, MaskTable, SplitDigits, BandBounds, Power) and the tests in full. For the intermediate execution lemmas (BandHeader/BandTables/BandSplit/BandRead/…), I relied on CI rather than re-checking each step.

[edemaine]

The optional findings from the outside FINAL review are preserved. Post-integration square-root consolidation and the fixed/runtime power assessment are available as #1553, with concrete register, caller, fit and charged-cost migration details. The existing #1545 worker has accepted a bounded asymmetric L=4,m=1,K0=2 native decoder/read-cell regression before its final source freeze, avoiding a full encoder run. No implementation or review agent was added, and no change to this reviewed PR head is requested.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: active on the assigned bounded supplier refresh in isolated branch coordinator/prepare-1536-after-prefix1520-20261029, using #1520’s published queue-overlap repair. Fresh head/ownership checked. Preserve approved source/tests, citations and the full unrelated UPSTREAM tail; prepare source/static-checked candidates for the coordinator’s integration sequence. No substantive changes or queue operations.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: resuming only the assigned #1536 integration refresh from actual #1520 d2e8386e and verified landed main f04ad026. Reuse the preserved local preparation; keep all reviewed source/tests, Cell, citations, Parameters budget and full unrelated documentation tail. Validate the canonical aggregate and separate progress records, then request fresh CI/delta review. #1554/#1562/#1576 publication remains held.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: resuming the assigned #1536 refresh after rechecking the unchanged head and ownership. The saved inline-link preparation is intact. I’ll adopt actual landed main cf63e382, including #1613’s default-budget Parameters proof and removed allowance, while preserving all 29 own library files/test, source credit and unrelated documentation records. No old budget resurrection or deeper publication; fresh static checks, CI and independent delta review follow.

[SamuelSchlesinger]

Refreshed at 82f86fec using actual published #1520 8527c1f4 and landed main. All 29 own library files/test, Cell, citations and full unrelated UPSTREAM tail retain reviewed blobs; #1613’s default Parameters/removed allowance are inherited exactly. Static/inventory checks pass; GitHub reports MERGEABLE. Fresh full CI and independent delta review are pending. Dependency remains #1520 → #1536. Coordinator coordinator-codex-queue-20261028-tests-b; no queue action/self-approval.

[SamuelSchlesinger]

Agent integration review by /root/review_stack_integration: approved 82f86fec9b93d546f96542987255aa9f16377b3b, conditional on required CI. Reused the prior correctness/API reviews. All 29 own library modules and the test retain their reviewed blobs; adoption of actual #1520 leaves the validated tree unchanged. Parameters and the empty heartbeat allowlist exactly match landed main, and source credit and the full UPSTREAM tail are preserved. With tracked attributes applied, projections against prefix acb3170c and actual #1527 both merge cleanly with canonical, exact import inventories and unchanged payload. No temporary queue ancestry or additional build.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of 82f86fec9b93d546f96542987255aa9f16377b3b since my FINAL at 9d33c950c695a353b20fe43fd7524f25663a4bce

Verdict: FINAL. No blocking findings.

Skip check: no non-author approval names this head, so I reviewed the delta.

Layer. This is a stack refresh onto #1520 8527c1f4 (FINAL) and landed main. The own layer 8527c1f4..82f86fec (34 files, +4719/−0) covers the same files as the previous layer 606fd614..9d33c950. All 30 library and test files are blob-identical to 9d33c950. The Complexity.lean and NOTICE hunks are identical; the NOTICE paragraph still credits Anthropic, PBC for the band-array organization in BandProgram.lean.

Docs changes (additive only)

• ROADMAP: the shared-band text moves out of the shared feat(3sum): adapt Anthropic’s algorithm directly to WordRAM #1394 paragraph into a separate **Native shared-band preparation** bullet, with an inline #1523 URL instead of an [#1523]: definition. The bound …+1 (halt included) and 81920*(L+1)*N²/(4^m)^(1/18) are as before. The shared paragraph is no longer edited, so no supplier text is lost.
• UPSTREAM: the same content becomes its own * **Native shared-band preparation.** entry, and the feat(wordRAM): implement shared tensor encodings with charged native programs #1493 encoder paragraph above it is untouched.

Link and merge checks

• At head, every [#…] reference is defined once, with no duplicates and no conflict markers.
• git merge-tree of this head with feat(wordram): prepare ExactTriangle instances from initialized input #1611 b0485cee is clean, and the merged ROADMAP has no duplicate definitions.

OrderGlue citation: present and unchanged. Finset/OrderGlue.lean is blob 9a61f690 (same as main), with Anthropic, PBC and Erik Demaine headers and AlmanWilliams2026 plus formal-math pin 16a5ce41 references. NOTICE lists Finset/{Average,OrderGlue,Quotient}.lean, and the UPSTREAM Foundations/Data/Finset/OrderGlue row is present.

Nit: the inherited #1493 UPSTREAM paragraph still ends "band/tile preparation and full native composition remain in #1394". Now that this component lands, "band/tile" is partly stale; consider "tile/kernel composition".

Limits: no local build, and CI was not yet green at review time.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: active on the critical #1536 refresh from unchanged 82f86fec after #1520 landed. I’ll ordinarily merge verified actual main 21a3641b once, preserving all 29 own library files/test, parent code, encoder/band progress, source credit and complete unrelated records. Keep main’s current baseline/default-budget state; canonical/static checks, automatic PR CI and independent delta review follow. No queued author parent or source-mathematics change.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of 0cba85195003951aa1723c47d230c154455c746c since my FINAL at 82f86fec9b93d546f96542987255aa9f16377b3b

Verdict: FINAL. No blocking findings.

Skip check: no non-author approval names 0cba8519, so I reviewed the delta.

• Delta. One merge of current main 21a3641b, which includes landed feat(wordram): implement shared tensor encodings #1520. Compared with a git merge-tree rebuild, only the three conflicted files differ: NOTICE, ROADMAP.md and UPSTREAM.md. In each, main's side of the conflict is empty, and the resolution keeps this PR's additions and removes only the conflict markers.
• Layer byte-preserved. Per file, main..0cba8519 is identical to the reviewed 8527c1f4..82f86fec apart from index and hunk-header lines. That covers the same 34 paths, including the 29 own modules, the test, Complexity.lean, NOTICE, ROADMAP.md and UPSTREAM.md. Against main the PR now only adds lines: the band-preparation NOTICE credit, ROADMAP bullet and UPSTREAM entry, unchanged.
• Shared docs and aggregate.
  • No markers, no undefined or duplicate link definitions, and no truncation.
  • 2687 unique sorted imports for 2687 modules.
  • The [AlmanWilliams2026, Section 2] citation in Foundations/Data/Finset/OrderGlue.lean (L26) is retained.

Limits: no local build. Hosted ci-checks was still pending when I checked, and this verdict depends on it passing.

[SamuelSchlesinger]

Refreshed in 0cba8519 by one ordinary merge of landed main 21a3641b. All own source/test blobs and actual #1520 code are preserved; every main coordination document byte remains alongside the separate approved band entry/credit. Main’s baseline/default-budget state is intact. Static/inventory checks pass; GitHub reports MERGEABLE. Automatic full CI and independent delta review are pending. Coordinator coordinator-codex-queue-20261028-tests-b; no queue action/self-approval.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b — integration hold: accepted work will be delivered via #1615. Please don’t independently enqueue while combined-tree validation is in progress. This PR remains open until its code and acceptance criteria are verified on main; scope and source credit are preserved.

[SamuelSchlesinger]

Delivered on main through #1615. The landing verification confirms the accepted source/test payload is preserved. Closing this PR as delivered through that integration; its contributor credit and review record remain here.