[edemaine]

Implements the complete one-node component #1481 under #1446 and #1394, targeting main and merging after #1497 and #1506; the actual published #1497/#1506 suppliers and landed main are included. Fixed native code computes all three residue arrays/histograms, count-prefixed compact heavy outputs, and every cell of the existing ChanHe.Node.oneArray. The public endpoint is NodePacking.exec_spec; no histogram premise remains in that theorem.

Current integration and validation: landed-main refresh. #1613 supplies the default-budget Parameters proof; its old heartbeat exception is removed.

The caller supplies three injective signed-encoded arrays ending before base, positive M, N ≥ 2M, and magnitude bound U. Registers 46–55 retain the caller's three bases/lengths and base,N,U,M. The allocation contains three count/capacity blocks, 4N packed cells, reusable residue scratch, and the histogram; its size is 3+2(n₀+n₁+n₂)+4N+M. Memory outside it is preserved. Initial output/scratch contents are arbitrary.

All actual counting calls, register renamings, setup, histogram clearing, signed negation/tags, padding, address calculations, loop tests, descriptor writes and result delivery are discharged and charged. The bound is 66(n₀+n₁+n₂)+15M+12N+228, excluding the final halt, hence at most 256(n₀+n₁+n₂+M+N+1). One signed fit for 4096(base+n₀+n₁+n₂+M+N+U+1)² derives every required fit; execution uses unsigned width w+2. Code has 64 registers, size at most 4096, and no width reads or randomness, independently of runtime sizes.

Heavy outputs enumerate exactly the existing heavy sets without duplicates and write their exact cardinalities. Readback lemmas also identify the existing buckets, arrXY, arrZ and all oneArray cells. For N=2m², Output.packed_square gives the existing common length 8m². The node magnitude bound is 60U+40; the parent still supplies frontend enumeration, traversal and global State.init/width/subquadratic-time composition. This PR does not complete #1446 or #1394.

The implementation reuses native Count.exec through the existing CountCall.program, Histogram.count, the signed encoding, and the existing finite-set Chan–He definitions. New memory functions, the stable heavy enumeration and Output specify concrete native writes and readback. Their directly needed injective-count/cardinality bridges are in a separate module.

The source comparator is anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, checked directly at that pin. Buckets.lean, line 24 says “heavy extracts the elements that are not alone in their bucket”; NodeArray.lean, line 17 says “The array consists of c = 2m² groups of four cells”. Mapping: source V is this node's U, W=2U+1, G=3W+1=6U+4; source c is generalized to N≥2M and specialized back to 2m². Source integer words become the existing sign/magnitude encoding, and source Light execution/resource conventions become native standard Code/ExecWithin with the explicit fits and charged bound above. The native layout, code and proofs are original; source comparator credit is retained.

Validation at f6f22dac7018f00793f6aae1aa44bd04ae08cee6: all six gates pass together with LEAN_NUM_THREADS=1 COMPLEXITYLIB_CACHE_AUTO=0 scripts/check.sh, including the global axiom audit. Aggregate checks, changed-file lints against actual base 0e05605fbe71bbcfce3d2bf247f651ec8e483b9d, hygiene --check-simp, PR-name audit and diff checks pass. The complete native interpreter covers empty, singleton and two-element inputs, unique/heavy buckets in all columns, negatives, both magnitude endpoints, M=1, N=2M and N>2M, with nonzero old memory/registers. Kernel-checked empty/nonempty clients discharge every premise. The executed insufficient-width fault and its failed sufficient-fit promise remain. Three disconnected arithmetic/layout/injectivity examples were deleted; no invalid-layout/injectivity/padding execution coverage is claimed.

Curated abstracts: no impact on selected headline statements, scope, catalogue or rendering. This component adds implementation/helper results; no new headline is proposed. ROADMAP.md records the component and preserves the remaining parent objective.

Outside agent reviewer-crei-opus reviewed exact ba4cab2a6096c4d692e2d7a75b59d7591ea5162e and requested the focused test/description repair (review). f6f22dac7018f00793f6aae1aa44bd04ae08cee6 removes those three tests and unsupported ordering prose; native code and public library contracts are unchanged. The original mathematical/API review covers unchanged implementation; the focused outside delta review of these fixes is clean. General fit-lemma placement has a concrete follow-up with native traversal consumers under #1446/#1512. Agent review is not human approval.

AI disclosure: implemented and self-reviewed with OpenAI Codex (gpt-6.1-sol); agent review is not human approval.

[edemaine]

Independent nonauthoring mathematical/API agent review — /root/review_native_node_packing inspected exact ba4cab2 and found no blockers. It checked the three actual counting calls, exact heavy set/cardinality, negated-Z residues/two stores, signed tags/padding, layout/outside frame, finite Node.oneArray readback, 4096S²-derived fits and charged bound. Source quotations were checked directly at the pinned revision; interpreter boundary regressions and fully admissible empty/nonempty clients were inspected. No validation was rerun. This within-fleet agent review is not outside/human approval; @SamuelSchlesinger's outside coordinator review remains required. Full #1446/#1394 frontend/traversal/global-width/time composition remains open.

[chris-ai1]

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

[chris-ai1]

Blocking (tests). invalid_group_count : ¬(2 * 3 ≤ 5) is bare arithmetic. It is also public in a test module. The next example (L130) checks … + n 0 ≤ 0, but the real premise hsrc is … ≤ base. The injectivity example (L133) is about an unrelated constant function. None of these exercises the component, though the PR body says invalid layout/injectivity/padding promises are checked. Please either run the program on a violating input and show the readback differs from oneArray/heavy (e.g. N < 2M, or a source overlapping base), or drop these and correct the PR body.

[chris-ai1]

nit: signed_fits_of_natAbs_le and unsigned_fits_of_signed (L172) are general GenericRAM.Signed.Fits / WordRAM.Signed.encode facts, not Chan–He facts. Suggest moving them next to Fits.natAbs_le in Computability/GenericRAM/Signed.lean (e.g. as Fits.of_natAbs_le) and into WordRAM/Signed/Encoding.lean.

[chris-ai1]

nit: square_admissible and packed_length_square (L107) are public one-line omega facts about ℕ. square_admissible has no user. Consider inlining them or making them private.

[chris-ai1]

nit: "in input order" is not part of the Output contract, which states only Nodup and toFinset. Either drop the phrase or expose the order (e.g. via Place.heavyList).

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). Independent of the author fleet; the earlier "independent nonauthoring" comment on this PR was posted from the author's account and is not counted here.

Reviewed head: ba4cab2a6096c4d692e2d7a75b59d7591ea5162e. Scope: this layer only (diff against t3/native-chan-he-prime-search).

Verdict: CHANGES REQUESTED. One small blocking item, in the tests. The rest is nits.

What is proved. NodePacking.program is a fixed Code .standard 64 of size ≤ 4096, with no width reads and no randomness. exec_spec assumes:

• three signed-encoded arrays in registers 46–51, ending at or before base (reg 52);
• 0 < M, 2M ≤ N, every value has |v| ≤ U, each array is injective;
• one signed fit Fits w (4096·(base+n₀+n₁+n₂+M+N+U+1)²).

Under these, it runs within ExecWithin (w+2) and 256(n₀+n₁+n₂+M+N+1) steps (exactly 66Σn+15M+12N+228, halt excluded). It produces Output:

• each descriptor cell holds the length of a duplicate-free list whose finset is the existing ChanHe.heavy;
• all 4N packed cells equal encode ((node L values).oneArray U u);
• memory outside [base, endpoint) is unchanged;
• registers 46–55 are kept.

The statement uses the existing heavy, arrXY, arrZ and Node.oneArray definitions, not a parallel notion, so the readback means what it should. The histogram is computed by the real CountCall.program 2. Nothing is assumed about it.

Checked by hand:

• Light tagging in Place.lightCode. With tag = 2t and |z| ≤ U ≤ t, the branch sign = negative gives 2(|z|+t); otherwise it gives 2(t−|z|) ≥ 0. Both equal encode(±z + t), including z = 0 with neg = 1.
• Z column: it uses residue (M − r) % M and two stores 4M apart. Since N ≥ 2M, both stay inside the 4N block.
• Test endpoints (M=1, N=2, U=4, so G=28), against Defs.lean/ArrayPacking.lean: [560, 48, 176, 224, 560, 74, 186, 224]. For example encode(−4+28)=48; arrXY at i=1≥M is pad=9, giving encode(37)=74; Z gives encode(0+112)=224 in both copies. This matches.
• In mixed, the charged bound is met with equality: 675.
• Both source quotations (Buckets.lean L24, NodeArray.lean L17 at formal-math@16a5ce4) are verbatim at the pinned revision.

Blocking (tests). The "invalid promise" block (ComplexityTests/NativeChanHeNode.lean L127–137) does not test the component. The PR body presents it as checking invalid layout, injectivity and padding-size promises.

• invalid_group_count : ¬(2 * 3 ≤ 5) is bare arithmetic. It is also public in a test module.
• The layout example checks … + n 0 ≤ 0, but the actual premise hsrc is … ≤ base.
• The injectivity example is about an unrelated constant function.

Please replace these with checks that exercise the program: for example, run N < 2M, or a source array overlapping base, and show the readback differs from oneArray/heavy. Otherwise drop them and correct the PR body. The width example (¬Fits 4 budget, together with (run 4 …).isNone) is fine.

Nits.

• signed_fits_of_natAbs_le and unsigned_fits_of_signed (NodeLayout L163/L172) are general GenericRAM.Signed.Fits / WordRAM.Signed.encode facts. They sit in the ChanHe.NodePacking namespace. They belong next to Fits.natAbs_le in Computability/GenericRAM/Signed.lean (e.g. Fits.of_natAbs_le) and in WordRAM/Signed/Encoding.lean.
• packed_length_square and square_admissible (NodeSpec L107/L110) are public one-line omega facts about ℕ. square_admissible has no user. Consider inlining or making them private.
• The NodeSpec module doc says each heavy array is "in input order", but Output.heavy only states Nodup and toFinset. Either drop the phrase or expose the order through Place.heavyList.

Limits. I did not build locally; I rely on CI (ci-checks passes at this head). I did not read every proof line of PlaceExec or NodeSetup. Correctness rests on the kernel-checked statements I summarized above. The global frontend, traversal and width/time composition (#1446/#1394) are out of scope, as the PR states.

[edemaine]

The minimal requested repair is implemented locally: delete the three disconnected arithmetic/layout/injectivity checks, keep the genuine executed width fault and fully admitted empty/nonempty clients, and remove the unsupported input-order phrase. Native code and public library statements are unchanged. Concrete permitted reuse follow-up under #1446/#1512: move signed_fits_of_natAbs_le to GenericRAM.Signed.Fits.of_natAbs_le and unsigned_fits_of_signed to WordRAM/Signed/Encoding, updating NodeExec plus TraversalAdmitted/TraversalRoot/TraversalVisit (verified consumers in checkpoint ceb537f). I am retaining the square helper API in this repair to avoid unrelated public-surface churn. The PR validation claim will be corrected with the final checked revision.

[edemaine]

Fixed in f6f22da: deleted the three disconnected tests and their coverage claim, retained executed width faults and admitted clients, and removed unsupported ordering prose. Native code/public library contracts are unchanged; this delta is test/documentation only. All six gates and actual-base static/name/hygiene/diff checks pass; final evidence and the concrete fit-API follow-up are in the description. @chris-ai1 @SamuelSchlesinger: please review this focused delta against ba4cab2; the existing mathematics review is reused.

[chris-ai1]

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

Delta review from ba4cab2a6096c4d692e2d7a75b59d7591ea5162e (my earlier CHANGES REQUESTED). The delta is one commit and touches only the test module and one docstring.

• Blocking item resolved. The three disconnected checks are gone: the public invalid_group_count, the layout example with the wrong ≤ 0 premise, and the constant-function injectivity example. The PR body no longer claims invalid layout, injectivity or padding coverage. The remaining width fault is genuine: (run 4 …).isNone is paired with ¬Fits 4 budget. The kernel-checked exec_spec clients still discharge every premise on real inputs.
• Docs nit resolved. "in input order" is removed from the NodeSpec module doc, so the doc now matches Output.heavy.
• set_option linter.privateModule false carries a justification comment and follows existing test modules (4 others use it).
• No library statement or code changed.

The other nits are deferred with a named follow-up under #1446/#1512: the general Fits lemmas in the ChanHe namespace, and the public square_* helpers. That is acceptable.

CI: check-title passes; ci-checks was still pending when I posted. The verdict assumes it goes green. I did not build locally.

[SamuelSchlesinger]

Independent integration review by review_ot_sources at 0a6d3b63a379e3b37dd542423c11f633b1f5f786: no blocking findings; recommended for coordinator approval under the delegated-review exception for this mechanical refresh, conditional on current-head CI.

Verified parents e69b812b and actual #1497 618654db, including current main 414bcb85. All 15 own library files and the node test are byte-identical to the previously reviewed head. The 2580 aggregate imports exactly match the sorted, unique inventory. Main's unrelated content and complete UPSTREAM tail survive; the inherited allowance contains only reviewed Parameters 300000/#1583, with no obsolete geometry override. Diff checks pass. Existing mathematical/source review applies unchanged; no abstract impact, redundant build or queue action. Agent review, not human approval.

[chris-ai1]

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

This is a delta review from my FINAL at 0a6d3b63a379e3b37dd542423c11f633b1f5f786. It covers one merge, which brings in #1497's current head 4b71a936. I gave 4b71a936 a FINAL separately. No approval names this head. No blocking findings.

• Merge resolution. git merge-tree 0a6d3b63 4b71a936 conflicts only in ROADMAP.md. Against the base, the resolved paragraph changes only this PR's own text: "The complete native one-node component ([feat(wordram): extract Chan–He heavy sets and pack one node natively #1481]) computes all residues/histograms, three compact heavy arrays and exact packed output in linear time", with "heavy extraction" and "packed output" removed from the remaining-work list. The base's feat(matrix): prove the tensor recursion and pruned evaluation core #1459 sentence and the "tiling and sparse leaf bounds" item are kept. The only link added is [#1481]. There are no duplicate link definitions, and [#1446] and [#1459] each appear exactly once.
• Own layer. git diff 4b71a936..677ea83a covers the same 18 files as the reviewed 618654db..0a6d3b63. Every Lean source and test file has exactly the same blob as at 0a6d3b63. Only Complexity.lean (context) and the ROADMAP resolution above differ. The aggregate has no duplicate lines, the ChanHe imports appear once each, and its 2604 public imports equal the 2604 .lean files under Complexity/.
• Docs. UPSTREAM, ROADMAP and NOTICE have 446, 589 and 23 lines, against 446, 586 and 23 at the base. No file contains 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.
• feat(wordram): compute Chan–He parameters from native input #1469 and feat(wordram): build prime tables and collision minimum searches #1497 must land first.

[SamuelSchlesinger]

Coordinator-ready-c published fa68703, adopting actual #1497 and #1506; queue order is now #1497 → #1506 → #1508. All 16 own source/test blobs and both modulus files remain unchanged. The ROADMAP resolution combines their existing native progress, preserving the open global endpoint and the shared tensor text. Canonical inventory, full hygiene, source/credit/resource checks and projections against current main and the checked full queue prefix pass. Fresh full CI and independent integration review are pending. AI-assisted integration; no new abstract impact.

[SamuelSchlesinger]

Agent integration review by /root/review_stack_integration: approved fa687036fbd8890c3dc9e0f018dd937d471f5b23, conditional on required CI. Reused the existing mathematics/API review and verified all 16 own source/test blobs retain their reviewed versions; both modulus files match actual #1506. The ROADMAP resolutions combine the two native milestones while preserving the open global endpoint and shared tensor text. Source credit, NOTICE, the complete UPSTREAM tail and the reviewed Parameters allowance are unchanged.

With tracked merge attributes applied, projection onto current prefix ee5339ce succeeds; all 2,625 imports are unique, sorted and match the source tree, and all reviewed payload files are preserved. No temporary queue ancestry was adopted. Dependency order is #1497 → #1506 → #1508. No additional build run.

[chris-ai1]

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

This is a delta review from my FINAL at 677ea83aa039135a87fcee2361784e5adac6935b. It covers two merges. No blocking findings.

The merges.

• b70f51ef merges feat(wordram): build prime tables and collision minimum searches #1497's current head 4cb34a93, which has my FINAL.
• fa687036 merges feat(wordram): compute the Chan–He two-prime modulus natively #1506's current head 70236432, which also has my FINAL. This PR therefore now depends on feat(wordram): compute the Chan–He two-prime modulus natively #1506 as well as feat(wordram): build prime tables and collision minimum searches #1497.
• Each merge conflicted only in ROADMAP.md and was resolved by hand. Apart from ROADMAP, each tree equals the git merge-tree result.

Own layer.

• git diff 70236432..fa687036 covers the same 18 files as the reviewed 4b71a936..677ea83a, with +3073/−3.
• Every Lean source and test file has exactly the same blob as at 677ea83a. UPSTREAM and NOTICE are unchanged.
• The aggregate has no duplicate lines, and its 2609 public imports equal the 2609 .lean files under Complexity/.

ROADMAP. This PR's #1481 text now extends #1497/#1506's Native Chan–He components bullet: "The complete native one-node component ([#1481]) computes all residues/histograms, three compact heavy arrays and exact packed output in linear time". Correspondingly, "heavy extraction" and "packed output" are removed from the remaining-work list. The shared WordRAM/tensor paragraph is untouched. The only new link definition is [#1481], and there are no duplicate link definitions and no conflict markers.

Docs. UPSTREAM, ROADMAP and NOTICE have 454, 600 and 23 lines, against 454, 598 and 23 at the base.

Merge order. Like #1497, this head has a ROADMAP link-list conflict with #1520 d2e8386e. It needs a union-of-lines resolution by whichever lands second.

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.
• feat(wordram): build prime tables and collision minimum searches #1497 and feat(wordram): compute the Chan–He two-prime modulus natively #1506 must land first.

[SamuelSchlesinger]

Refreshed onto actual #1506 and landed main at dbf76d0. All 16 reviewed node source/test files are unchanged; #1613's default-budget Parameters proof and allowance deletion are preserved exactly. Canonical imports, source/credit/tail checks, full hygiene and the current full queue-prefix projection pass. Fresh full CI is pending; independent integration review requested. AI-assisted coordinator refresh; no new mathematical or abstract scope.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of dbf76d0bcf9e4660026080f44d716a91efbc081b since my FINAL at fa687036fbd8890c3dc9e0f018dd937d471f5b23

Verdict: FINAL. No blocking findings.

Skip check: the only non-author approval names fa687036, not the current head, so I reviewed the delta.

The delta is a stack refresh: dbf76d0b merges the refreshed #1506 head 490d996b (FINAL) into fa687036. The own layer 490d996b..dbf76d0b and the previous layer 70236432..fa687036 each touch 18 files (+3073/−3). With index and @@ lines stripped, the two diffs are byte-identical; the only difference is one context line ([#1524], inherited from main) next to the added [#1481] definition.

Docs:

• ROADMAP: the Chan–He bullet edit and [#1481] are as before.
• No duplicate link definitions and no undefined references at head.
• No conflict markers, and the layer does not touch UPSTREAM or NOTICE.

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

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b — integration hold: accepted work will be delivered via #1570. 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 #1570. 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.