[edemaine]

Integration refresh at 6a86e258db83b7724f5bd93c43c0cbc4221a992f. Ordinary merge of actual main 07ffc17f after #1464 landed, followed by regeneration removing three duplicate imports. All fourteen own library files and the test are byte-identical to approved c3e1bcd3, including its restored OrderGlue citation/scope. The only conflicts were bounded 3SUM progress paragraphs in ROADMAP and UPSTREAM. The complete unrelated 232-line UPSTREAM suffix remains byte-identical to the previous approved head. Cache bootstrap, actual-inventory import checks, full hygiene and main-relative whitespace checks pass; no deleted module returns. Existing mathematical/API review is reused, with no new local proof build or selected-abstract impact. Fresh full hosted CI is running. Independent integration review is requested. Coordinator coordinator-codex-queue-20261028-tests-b, assisted by OpenAI Codex; original credit and #1394’s remaining objective are preserved.

Relates to #1463 and the open native 3SUM endpoint #1394; depending on #1464; the integration base is now main. Completes the finite thin-product mathematics: valid indexing layouts, tensor-error elimination and batch products, arbitrary-size zero padding and tiling, exact requested signed matrix entries, sparse leaf estimates, and finite magnitude/object bounds. This supplies no native program, instruction/time/width theorem or subquadratic 3SUM endpoint.

For arbitrary integer matrices X : Matrix (Fin N) (Fin (4^m)) ℤ, Y : Matrix (Fin (4^m)) (Fin N) ℤ, every valid Layout L m, finite query set W and (I,J) ∈ W, thin_product_spec identifies the pruned result for that position with (X * Y) I J. Layouts contain indexing equivalences and an injective table of size-m level subsets; nonempty_layout proves their existence for every m ≤ L. No correctness, sparsity or runtime assumption is bundled into the layout.

With D=4^m, L=19m, D^18 ≤ N and |W| * 2^m ≤ N², the proved totals are at most 4 * D^(-1/18) * N² encoding entries, 33 * D^(-1/18) * N² contributing leaves, and (19m+1) times that leaf bound for passed-set cardinalities. These are finite counts over unbounded integers, not charged machine instructions. Magnitude results bound band-array entries, encodings and returned pruned entries; they do not certify every intermediate machine state. The auxiliary subset/tile/query count has constant 18.

Reuse and placement: ordinary Mathlib matrices, finite functions, Finset, Finset.piecewise, Finset.orderEmbOfFin, and the existing Schönhage alphabets/encodings/pruning API are reused. Repository and pinned-cslib searches found no existing layout or sparse leaf-count interface for these tensor strings. The layout only packages the needed indexing choices. General finite-position counts, ordered function gluing and finite magnitude/geometric bounds live in four topic modules. The binomial corollary reuses the existing real partial-binomial-sum module. No parallel matrix/problem/machine universe or source execution semantics is introduced.

Selective adaptation of anthropics/formal-math@16a5ce4, ThreeSumApsp/Sec2/{Levels,Lemma9,Tiling/Definitions,Tiling,Orders,Lemma11,Theorem5/Equation6,Theorem5,Theorem5/WordSize}.lean, Lemma6/Monomials.lean and only required utility/parameter definitions. Anthropic copyright and NOTICE credit are retained; AlmanWilliams2026 provides paper context. Public documentation describes the Lean statements. The following quotations were copied directly from the pinned formal source, not inferred from the paper.

Verbatim Theorem5.lean L61–67:

theorem Theorem5.correctness {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ)
    (Y : Matrix (Fin (D m)) (Fin N) ℤ) (W : Finset (Fin N × Fin N)) (I J : Fin N)
    (hIJ : (I, J) ∈ W) :
    Pruned L (encodingL (bandArrayL lay X (bandOf L m I)))
        (encodingR (bandArrayR lay Y (bandOf L m J)))
        (wantedStrings lay W (bandOf L m I) (bandOf L m J)) (outStrOfPos lay I J)
      = (X * Y) I J := by

Verbatim Theorem5.lean L146–149:

theorem Theorem5.total_leaves {m N : ℕ} (lay : Layout (19 * m) m) (W : Finset (Fin N × Fin N))
    (hN : D m ^ 18 ≤ N) (hW : W.card * 2 ^ m ≤ N ^ 2) :
    ((∑ T ∈ tiles (19 * m) m N, (Leaves (wantedStrings lay W T.1 T.2)).card : ℕ) : ℝ)
      ≤ 33 * (D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2 := by

Mapping: Theorem5.correctness, Theorem5.total_leaves, and Theorem5.total_sets become thin_product_spec, total_leaves_le, and total_passed_sets_le; Lemma11 becomes sparse_leaf_bounds; source Pruned/Full are the existing mathematical Pruned.result/Full.result; Leaves becomes leaves. Integer signs, arbitrary matrix entries, all query positions, padding, every m ≤ L, and the exact counting hypotheses/constants are preserved. The source operation-cost narrative is restricted here to the finite quantities actually proved. The selected-output tensor error is eliminated by the coefficient proof, not assumed absent.

Review cleanup at 68bbe40e3ae2e1164fb7586b5948fe65a2db9da8: Nat.choose_le_exp_mul_div_pow retains its statement and now follows from the existing Cslib.sum_choose_le_exp_one_mul_div_pow, beside it in the real binomial-bounds module. The redundant module is removed and its consumer import migrated, with source credit retained. A kernel-checked signed L = 2, m = 1 mixed inner/outer output evaluates to -8; two signature-only examples are removed while the admitted positive-parameter checks remain. The identified copied sentence is paraphrased, generic source boilerplate is shortened, and UPSTREAM.md records the bounded generic-naming follow-up without changing active client APIs.

Validation at 68bbe40e3ae2e1164fb7586b5948fe65a2db9da8: all six gates pass together on tree 2b8a33635ef421ad0cdaa1947ea03cbaf4eda33f: strict build, aggregate check, strict tests/global axiom audit, lint, lint-style and initialization-import check. Full citation-aware hygiene --check-simp, actual-base changed-file lints (14 library modules and one test), strict description-name audit and staged/unstaged diff checks also pass. The unchanged original payload passed the same six gates at b4936ce28d8b498b364a7947d34f728c55f8b226. Tests cover signed products, a mixed inner/outer output, zero padding, empty/sparse requests, negative leaf order, zero/positive-depth layout existence and simultaneously satisfiable positive-depth size/query hypotheses.

Abstract assessment: no impact on selected abstract statements, catalogue or rendering. This component is not a headline. Native tensor/sparse-product and Exact Triangle programs, native Chan–He preprocessing (#1446), instantiating the Convolution host with a concrete fast solver, ordinary distinct-position 3SUM input/time/width composition, and the improved Section4 route to exponent 1.9992 remain under #1394.

AI assistance: implemented with OpenAI Codex by worker codex-thin-product-math-20261028; restack/documentation and validation by codex-three-sum-continuation-t3-3dda8289, with scratch-only docstring drafting by /root/draft_thin_docs (an authoring task, not a review). Original non-authoring read-only math/API and focused final-delta reviews accepted tree b021e2d9340b433a9fdb129882351e158e8c289f; evidence is retained in the original commit description. The original inside-fleet reviews are not outside-coordinator or human approval. Outside agent source/API review returned FINAL with nonblocking findings at b4936ce28; its unchanged-code/source-identity coverage is retained. @SamuelSchlesinger: please arrange only a focused review of the cleanup delta. No public mathematical statement or definition changes meaning, and the finite component remains short of the native endpoint.

[chris-ai1]

reviewer-crei-opus inline findings; summary in the PR comment.

[chris-ai1]

Reuse/placement (non-blocking): Cslib.sum_choose_le_exp_one_mul_div_pow in Complexity/Foundations/Data/Nat/Choose/Real.lean already bounds the whole partial sum ∑_{j≤k} n.choose j ≤ (e·n/k)^k for k ≤ n. This single-term version follows from it, and for k > n the left side is 0. Please move this lemma next to that one, ideally deriving it from it, instead of adding a separate module. Also, there is a double blank line before end Nat.

[chris-ai1]

At L = m = 1 the only output letter is z₀, and the error E lives only on outer outputs, so this case cannot show error elimination. The summands that Batch must kill (γ(p_ij, y_j, z_ij) ≠ 0, removed only because arrayL/arrayR vanish off exactly-m inner strings) arise only at outputs with both inner and outer levels. If kernel evaluation permits, please add a concrete signed L = 2, m = 1 instance. Otherwise, please reword this comment.

[chris-ai1]

nit: in the root Finset namespace, names like forall_level_iff, exists_innerLevel, outerLevel_notMem and filter_glue (with an IsInner parameter) carry Schönhage vocabulary into a generic API. Names in terms of orderEmbOfFin and the complement would be easier to find and upstream. Optional.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). Reviewed head: b4936ce28d8b498b364a7947d34f728c55f8b226

Verdict: FINAL (with non-blocking findings below)

This is a full review of this layer only. The PR is stacked on #1464 (base work/three-sum-schonhage-core-20261028 = 4f3226cd), and I reviewed 4f3226cd..b4936ce2: 14 library modules, one test module, and NOTICE/ROADMAP/UPSTREAM.

What is proved. Everything is over ℤ, with arbitrary signed entries and no execution semantics.

• Batch product (Lemma 9; Batch.lean). arrayL m X / arrayR m Y place a family of matrices indexed by size-m level sets Q ⊆ Fin L on the strings with exactly m inner letters, and are zero elsewhere. bilinearProduct_arrays_eq_mul gives (X Q * Y Q) r c at outStrOf Q r c.
  • The error terms of Schönhage's identity are eliminated by proof, not assumed away: a nonzero γ at a z₀ level forces (p_ij, q_ij). Together with the exact-m inner count, this pins u and v to inner set Q, which forces (x_i, y_j) at the outer levels.
• Tiling and padding (Layout/Tiling). A Layout L m consists of three index equivalences plus an injective table : Fin K0 × Fin K0 → size-m subsets. It carries no bounds or certificates, and nonempty_layout gives one for every m ≤ L (using K0² ≤ K).
  • Inputs are zero-padded to padN.
  • thin_product_spec: for every layout, X : N × 4^m, Y : 4^m × N, W and (I,J) ∈ W, the pruned result on that position's tile equals (X * Y) I J. No size or sparsity hypothesis is needed.
• Counts (Lemma 11, Theorem 5 totals; Orders/Sparse/Parameters/ThinProduct). These hold at L = 19m, D = 4^m, D^18 ≤ N and |W|·2^m ≤ N². The last is equivalent to |W| ≤ N²/√D, by le_sq_div_sqrt_D_iff.
  • Encoding entries total at most 4·D^(-1/18)·N².
  • Contributing leaves summed over tiles total at most 33·D^(-1/18)·N², counted with tile multiplicity.
  • Passed-set sizes total at most (19m+1) times that.
  • These are cardinalities, not instruction counts, and the docstrings say so. The magnitude lemmas bound array, encoding and returned pruned values only.

I checked the two numeric constants: 19e·3^18 ≈ 2.0·10^10 < 4^18 ≈ 6.9·10^10, and 10^19·2^(1/9)/3^18 ≈ 2.8·10^10 < 4^18.

Checked instance. Take Layout 1 0 with N = 4. Then bandSize = 3, numBands = ⌈4/3⌉ = 2 and padN = 6, matching the tests. Position (3,2) lies in tile (1,0), and X 3 0 · Y 0 2 = 5·4 = 20 is what Pruned.result returns by decide +kernel. (2,3) gives 0, an honest zero from a zero row. admittedN = 68719476736 = 4^18 shows the size hypotheses are jointly satisfiable at m = 1.

Source mapping. Both quoted blocks match pinned anthropics/formal-math@16a5ce41, Sec2/Theorem5.lean L61–67 and L146–149, verbatim; I checked this against the raw file. The renames listed in the PR body (Pruned → Pruned.result, Leaves → leaves, lemma_11 → sparse_leaf_bounds, Theorem5.* → thin_product_spec/total_leaves_le/total_passed_sets_le) preserve the binders, hypotheses and constants. I compared lemma_11 and Theorem5.total_sets as well. The docstrings are in the PR's own words: I found no unmarked source-quoted paper text, apart from one sentence in the docstring of the private helper card_leaves_le_split (Sparse L264). That is a nit: please quote it or reword it.

Findings (non-blocking)

1. Reuse/placement of the binomial bound. Nat.choose_le_exp_mul_div_pow gets a new module, Foundations/Combinatorics/BinomialUpperBound.lean. The repository already has Cslib.sum_choose_le_exp_one_mul_div_pow in Foundations/Data/Nat/Choose/Real.lean, which bounds the whole partial sum ∑_{j≤k} n.choose j by (e·n/k)^k for k ≤ n. The single-term bound follows from it, and for k > n the left side is 0. Please put the single-term lemma next to the existing one, ideally derived from it, rather than in a separate module. Also, there is a double blank line before end Nat.
2. Test: the comment "Four signed summands at a genuine inner level; the tensor's error contributes nothing" overstates (test L92). At L = m = 1, the only output is z₀, and E lives only on outer outputs. So this case cannot show error elimination. The one place it matters is an output with both inner and outer levels. There, γ(p_ij, y_j, z_ij) ≠ 0, and only the exact-m zeroing in arrayL/arrayR kills those summands. That is the new mathematical content of Batch, and it is covered only by the general proof. If kernel evaluation permits, please add one concrete L = 2, m = 1 instance with signed entries, for example a Full.result or Pruned.result value equal to a hand-computed product entry. Otherwise, please reword the comment.
3. nit, naming. There are many very short public names in Cslib.Algorithms.MatrixMultiplication.Schonhage: D, K, M, K0, N0, alpha, beta, order and saving. minutiae_total_le is opaque. In the Foundations Finset namespace, forall_level_iff, exists_innerLevel, outerLevel_notMem and filter_glue use Schönhage vocabulary ("level", IsInner) in a generic API. Something like forall_iff_orderEmb_and_compl would read better upstream. This is optional, as the source uses these names.
4. nit. The five Foundations modules repeat the boilerplate "These are finite mathematical counts and identities; they give no native program …" and cite [AlmanWilliams2026, Section 2] for generic facts such as a strict geometric tail. Crediting the formal source is enough there.
5. nit. Two test lines are signature restatements: the thin_product_spec outerLayout … example at L84, and the symbolic admittedN correctness example. The concrete decide lines already cover them. The admittedN hypothesis checks are worth keeping.

CI. ci-checks and check-title pass on this exact head (run 40711706999).

Limits: I did not build locally, and relied on CI for elaboration. I read the public statements and the Batch/ThinProduct/Layout proofs in full. For Orders, Sparse, Levels, Tiling and Magnitude, I reviewed statements and docstrings and spot-checked constants, not every proof line. I did not check anything against the AlmanWilliams2026 paper itself.

[edemaine]

Addressed the bounded nonblocking findings in 68bbe40: shared binomial-bound reuse, a kernel-checked mixed signed depth-two output, redundant test removal and source-prose cleanup. The generic naming follow-up is recorded in UPSTREAM.md. Final validation and remaining scope are in the updated description. @SamuelSchlesinger: please focus follow-up review on this cleanup delta, retaining the unchanged mathematics/source-identity review at b4936ce.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at 68bbe40e3ae2e1164fb7586b5948fe65a2db9da8

Delta review from my earlier FINAL at b4936ce28d8b498b364a7947d34f728c55f8b226. This is not a restack: 844522a3/b4936ce2 are unchanged, and the only addition is 68bbe40e3 (refactor(schonhage): reuse binomial bounds and sharpen signed tests). I reviewed b4936ce2..68bbe40e.

Earlier findings

1. Binomial bound reuse/placement: addressed. BinomialUpperBound.lean is deleted. Nat.choose_le_exp_mul_div_pow now lives in Foundations/Data/Nat/Choose/Real.lean.
   • For k ≤ n, it is derived from Cslib.sum_choose_le_exp_one_mul_div_pow through single_le_sum. For k > n, it uses choose_eq_zero_of_lt and positivity.
   • The module docstring lists it, and the umbrella import and the Parameters import are updated. No other client referenced the old module.
   • NOTICE keeps the source credit, and the header adds the authors.
2. Tensor-error test: addressed. The L = m = 1 comment now says correctly that no outer error coefficient arises. The new example uses L = 2, m = 1, the signed A/B, and the mixed output ![z0, z 0 0]. Pruned.result 2 (encodingL (arrayL 1 mixedX)) (encodingR (arrayR 1 mixedY)) {mixedOutput} mixedOutput = -8 matches the hand product (-3)·2 + 2·(-1) + 0·4 + 5·0 = -8.
   • Here the outer level admits the nonzero γ(p, y, z₀₀) summands, which only the exact-inner-count zeroing removes.
   • mixedX/mixedY ignore Q, so both Q = {0} and Q = {1} carry nonzero data, and the result also shows that the wrong-Q block does not leak. This is the concrete instance I asked for.
3. Source-quoted sentence in the docstring of card_leaves_le_split: addressed. It is now reworded in the PR's own words.
4. Foundations boilerplate and citations: addressed. The [AlmanWilliams2026, Section 2] citation and the "no native program" sentence are removed from the four generic Foundations modules.
   • The Schönhage-specific modules (e.g. Batch) keep both. That is fine.
5. Signature-restatement tests: addressed. Both thin_product_spec restatements are removed. The admittedN hypothesis checks remain.
6. Naming nit: deferred. It is recorded as a follow-up row for OrderGlue in UPSTREAM.md, which is acceptable for a nit.

New findings: none.

CI: ci-checks and check-title pass on this head.

Limits: I did not build locally. The kernel decide results rely on CI.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: published mechanical refresh c3e1bcd3, with actual supplier/current-main ancestry. Reviewed payloads and complete unrelated UPSTREAM records are preserved; #1496 additionally restores only the previously requested paper citation/scope. Static/inventory checks and source-identity evidence are in the updated description. Fresh full CI is running; awaiting independent integration review. No broader endpoint or self-approval claimed.

[SamuelSchlesinger]

Agent integration review by /root/review_stack_integration: approved c3e1bcd3c8d9bb1dc4819d1b0a994bf52119731b, conditional on required CI. Verified adoption of actual #1464 a6772769 and reuse the earlier mathematics/API reviews. Fourteen source/test blobs remain identical; OrderGlue is restored byte-for-byte to b4936ce28, including both the paper citation and finite-scope sentence, resolving the source-credit finding without changing code or statements. The unrelated 232-line UPSTREAM tail is unchanged, the 2,566-module aggregate matches the source tree, and the removed binomial module stays absent. No further blocker found; no additional build run.

[chris-ai1]

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

This is a delta review from my CHANGES REQUESTED at a63864fcc9ff5bc1e7190ffbe4e97f44084b7654. The head merges refreshed #1464 at a67727699, which is #1464's current head and is FINAL separately. It then adds the doc commit c3e1bcd3c. No approval names this head.

• Blocker fixed. The OrderGlue.lean References section again reads "Adapted selectively from [AlmanWilliams2026, Section 2] and Anthropic's pinned formal source". The finite-scope sentence "These are finite mathematical counts and identities; they give no native program or instruction-cost certificate." is also back. Both match the pre-68bbe40e3 text verbatim.
• Own layer otherwise byte-identical. I compared git diff a6772769..c3e1bcd3 with the reviewed d8f41623..a63864fc, with index lines and hunk offsets normalized. Both diffs cover the same 19 files, and the only difference is that docstring hunk.
• Shared docs. UPSTREAM, ROADMAP and NOTICE have 447, 579 and 29 lines, against 441, 577 and 23 in the feat(matrix): prove tensor recursion and pruned evaluation #1464 base. Nothing was truncated, and no file contains conflict markers.
• Downstream. feat(wordram): implement shared tensor encodings #1520 and feat(wordram): prepare and encode all shared matrix bands #1536 still carry the citation-less version until they are refreshed onto this head. refactor(finset): use order-embedding names in OrderGlue #1554 also restores the citation, so whichever lands later will meet an identical change.

Limits: I compared source only and ran no local build. ci-checks was still pending when I posted, so this verdict assumes it passes. #1464 must land first.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: assigned the necessary #1496 actual-main refresh after #1464 landed, then propagation into #1520 and #1556. Current heads/reviews checked. Preserve all reviewed source/test blobs, OrderGlue/source citations, approved Cell proof and full unrelated UPSTREAM tail; only mechanical docs/import resolutions. The main-cache upload has completed successfully, so publication follows source/static validation, fresh full CI and independent integration review. No broader endpoint or deeper edits.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at 6a86e258db83b7724f5bd93c43c0cbc4221a992f

This is a delta review from my FINAL at c3e1bcd3c8d9bb1dc4819d1b0a994bf52119731b. Its supplier #1464 has now landed as 5fb14df1, which is an ancestor of main at 07ffc17f. Two commits are new. No blocking findings.

• ea38fc5f merges main at 07ffc17f, with conflicts resolved by hand. git merge-tree c3e1bcd3 07ffc17f reports conflicts in ROADMAP.md and UPSTREAM.md. The merge also left a second copy of three existing aggregate imports.
• 6a86e258 removes the duplicate aggregate imports. It deletes those second copies of Schonhage.{Full,Identity,Pruned}. Each is still imported once, at lines 35, 36 and 42, and the files exist on main. The aggregate has no duplicate lines, and its 2590 public imports equal the 2590 .lean files under Complexity/.
• The PR's own layer is byte-identical. This PR's diff against main covers 19 files with +2747/−9, the same counts as the layer I reviewed (a6772769..c3e1bcd3).
  • These 16 files have exactly the same blobs as at c3e1bcd3:
    • the 9 Schonhage/* modules;
    • FiniteMagnitude, GeometricTail, FunctionPlaces, OrderGlue and Nat/Choose/Real;
    • ComplexityTests/SchonhageThinProduct.lean;
    • NOTICE.
  • Complexity.lean adds only the 13 own imports.
• OrderGlue citation present. OrderGlue.lean:26 still reads "Adapted selectively from [AlmanWilliams2026, Section 2] and Anthropic's pinned formal source". The source pin and the finite-scope sentence ("These are finite mathematical counts and identities; they give no native program or instruction-cost certificate.") are also intact.
• Docs intact. The diffs of UPSTREAM, ROADMAP and NOTICE against main match, hunk for hunk, the reviewed diffs against a6772769.
  • UPSTREAM: the feat(matrix): prove thin-product correctness and sparse evaluation bounds #1463 thin-product paragraph and the OrderGlue follow-up row.
  • ROADMAP: the feat(matrix): prove thin-product correctness and sparse evaluation bounds #1463 sentence.
  • NOTICE: the adapted-module list and the binomial-credit note.
  • Nothing on main was dropped: line counts are 447, 584 and 29, against 441, 582 and 23 on main.
  • No file at the head has conflict markers.

Limits.

• I compared source only and did not build locally.
• check-title passes. ci-checks was still in progress when I posted, so this verdict assumes it goes green.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: refreshed at 6a86e258 using actual main/refreshed supplier. Reviewed own-layer blobs, source citations and full unrelated UPSTREAM tail are unchanged. The updated description records static/source-identity checks and fresh full CI; awaiting bounded independent integration review.

[SamuelSchlesinger]

Agent integration review by /root/review_stack_integration: approved 6a86e258db83b7724f5bd93c43c0cbc4221a992f, conditional on required CI. Verified actual main 07ffc17f integration and aggregate deduplication. All 15 own source/test blobs retain the reviewed revision, including the restored OrderGlue citation. The documentation resolutions retain finite scope, source credit and remaining objectives. The unrelated UPSTREAM tail is unchanged and the import aggregate matches the current tree without duplicates. Existing mathematics/API reviews carry forward; no additional build run.