roadmap: improve binary-field and tower foundations

Related trackers: ArkLib #893 — Binius and leanerVM #3 — Flock.

Current status — 2026-09-16

The previous 21 foundation PRs are merged: #325–#336, #339–#345, #349 and #350. They are included in main 1e470b46, tree a9cdba667a885c0f859412e4e86428dd0bf6858e. Each landing preserved the reviewed contribution and passed independent review and applicable checks. B2 is now merged; #324's B1 repair was already merged.

Production improvements: explicit tensor actions; nominal extension and BF64 carriers; separation of raw extension arithmetic from certification and the native-startup repair; generic tower and coordinate composition; concrete successor/endpoint coordinates and correspondence with the multilinear basis; a generic NTT module boundary; concrete import separation and simpler predecessor-field norm/multiplication proofs; and module-reference and reporting corrections. These are reusable library improvements. The concrete recursive assembly remains in place.

Validation of that earlier merged tree: warning-fatal library build, full tests, the 10,024-declaration axiom audit across 355 modules with zero admitted/nonstandard taint, native smoke execution under the documented 4 GiB/30-second bound, style/import/docs checks, and 242 benchmark-correctness records across all 59 curated groups with zero mismatches. The local run validated the published final PR head and was bound to byte-identical merged main; final-head core CI also passed. Ordinary validation workloads collected no timing samples; existing harness controls retained their prescribed behavior. This is correctness evidence, not a performance comparison.

Bounded B5 decision accepted with the implementation now merged: retain the current concrete bit representation, arithmetic and mathematical construction behind the improved APIs. The selected tower's B3-P/B3-T and named eager B9-A evidence now pass jointly; B6 replacement migration is not applicable. Reviewed public contracts and the existing fixed arithmetic data support retention; the concrete implementation is already flat storage. Retaining the mathematical induction does not freeze proof organization: scoped owner-proof cleanup remains open, and build/editor responsiveness is not claimed solved. The candidates' independently reviewed all-level fixed-map correspondence and historical native results remain valid evidence, distinct from current-source compatibility checks. No further comparison profiling is required for this choice, and the runtime panel does not establish a speedup.

Merged field PRs: #351 exposes successor coordinate arithmetic; #354 gives endpoint word/generator contracts; #355 transports the chosen bases and coefficients at the same indices. #352 isolates GHASH nominally, and #353 supplies its canonical executable Field boundary. #356 supplies the AES presentation.

Merged #357, originally reviewed at ffed107996cda5cf653754a0e6899541571b78fd, adds the selected executable AES-to-GHASH embedding at generator image 0x0dcb364640a222fe6b8330483c2e9849. Universal kernel proofs establish the homomorphism and injectivity laws; separately, all 256 executable byte images match both pinned reference tables. This does not prove either Rust implementation, Flock's 128-weight independence or any protocol theorem. Flock F0 has not started.

Merged tower/backend PRs: #358 supplies coherent generic tower powers; #359 introduces explicit word interfaces; #361 makes the tower carrier nominal; #363 separates narrow executable arithmetic from certificate interfaces. #360 supplies generic total product accumulation, and #362 refines the eager FastBT128 coefficient-evaluation consumer, with complete-word conversion and native checks. #364 preserves the AES/GHASH presentation counterexamples using explicit tower words. #365 supplies narrow GHASH/shared-word arithmetic imports. All 15 PRs #351–365 are merged in CompPoly e4817257, tree f30012ce813ac9f0940530fc18ba7f1c80845e19. Each landing preserves its reviewed contribution and passes applicable final-head correctness checks. The final tree differs from the accepted integration below only by two test-import ordering fixes; all production/native source is identical.

Joint validation before landing: the exact integration revision, tree 7603b702ba763b0e2ae00c26e50fbf089057a3be, passes full CompPoly build/tests, the 10,170-declaration axiom sweep across 364 modules with zero taint, linked native smoke under 4 GiB/30 seconds, all 244 correctness records in 60 curated groups, and style/import/docs checks. ArkLib 65dea00c passes its full gate against this exact source: 12,591 declarations across 496 modules, the same 291 existing admitted dependencies and zero nonstandard taint. The check used a local dependency override; no production pin or compatibility edits were made. Independent review accepts the exact source union, boundary clients and gate evidence. Ordinary correctness workloads collected no timing samples; existing harness controls retained their prescribed behavior.

Selected admission scope: tower B3-P/B3-T and eager B9-A are accepted, with merged implementations for (ConcreteBTField 7, FastBT128, CMlPolynomial.evalWithProducts, e4817257e4a124f6059857d5363aac63a79fa108); #362 is the originating consumer PR. This completes the bounded B5 retention decision for that selected scope. It does not admit every B3/B9 instance, delayed-wide/mixed/SIMD backends, a GHASH/BF64/F192 accumulation consumer or a protocol verifier, and supplies no performance ranking. AES/GHASH scalar boundaries and the selected byte embedding now include #365's narrow imports, while F1 weights/adapters and Flock F0/protocol work remain open. B4/B7/B8 and B9-V remain separate.

Downstream pin: ArkLib #899 is an open, independently reviewed repin to this merged revision, at head c4c1589f5ec57f48fd82d76dcd2e1cfdca976f03. Its full local gate passes with the same 291 existing admitted dependencies and no new or nonstandard taint; the production ArkLib pin remains 1e470b46 until the PR merges.

Earlier downstream pin: ArkLib #898, merged as 65dea00c from reviewed head 89c81f11a3912b10e7b9ad0987c84687da66bb75, updates the dependency to published CompPoly main. Its separate, nondefault ArkLibBlueprint environment restores abstract tower declaration checks and API pages without changing production imports or default build targets. The full ./scripts/validate.sh --axioms gate passed against the normally resolved pin: 12,591 declarations across 496 modules, retaining 291 existing admitted dependencies with no new or nonstandard taint. Blueprint declaration checks, including a missing-name negative control, PDF/web rendering, and generated API-page links also pass. The merge used an explicitly authorized maintainer override of the GitHub approval and merge queue requirements.

Earlier independent review — 2026-09-09

The dated evidence sections below preserve the state at their recorded revisions. Their draft/pending-construction language is historical: the current status above supersedes it. The work-package checklist retains its acceptance criteria and distinguishes the accepted selected-tower scope from additional instances and the unexecuted expanded cost panel.

A new independent review of CompPoly #325–#331 and ArkLib #894–#895 found no introduced arithmetic or API correctness regression. It did find a pre-existing ArkLib packing defect preserved by the migrations: row and column coordinates were reversed relative to DP24 while the verifier used the paper's orientation. Over GF(4)/GF(2), actual honest packing of t(X₀,X₁)=X₀ at zero rejected the correct claim. The repair corrects both coordinate definitions and reconstruction laws, with regressions through actual packing, original-claim acceptance/rejection, batching and the final multiplier. Independent compilable wrong-selector mutations detect each boundary. Full source, native and axiom gates retain the same 291 existing sorryAx-tainted declarations, with no new taint; local API docs and independently rendered blueprint/declaration checks also pass. The repair is draft #896 at 6a524b70f5bd0b740a283ca7d848fac13c9fd29f; the exact-head core run 34348993115, including native, axiom and documentation checks, and import CI now pass on its stacked branch. This corrects paper fidelity beyond the earlier migration-only review.

CompPoly #332, originally reviewed at 65b9dd36b05665cc713c8df8e8d332fbb1327c8f, separately corrects the extension guide's false divisibility/binomial-irreducibility claims and describes the actual cardinality/irreducibility certificates. Independent review and all five applicable CI workflows passed on that revision. These are documentation corrections; executable field operations do not change.

CompPoly #333, draft at dc72890f88ed3dfdcc404c64cea6a1b73e5510f5, extracts the reusable AlgebraTower.ofNatStep constructor into its existing owner. It requires only adjacent unital maps between commutative semirings, preserves identity self-maps, and permits noninjective steps. Independent probes check noncommuting step order and actual scalar actions. Full validation on current main bbc26a0 passes, including all 41 curated benchmark correctness groups and the 9,876-declaration axiom sweep with zero admitted/nonstandard taint. All five GitHub checks pass. It depends on merged #324 and is independent of the other draft stack; it does not change the recursive tower construction.

The candidate's typed-embedding/ordered-coordinate scratch milestone is now independently accepted: arbitrary comparable-level maps, a successor basis, two-step LSB ordering, executable packing/readback, and a fixed bit/embedding equivalence to the legacy carrier. Six fresh leaf checks and the sweep of 76 reportable declarations owned by the six new modules pass with only standard axioms; independent symbolic reconstruction and encoded basis-word clients pass. Manifest: 6827d4335a6a398e61a4cd44ed114ba37bbf74e8a37442019e8a3b63b424412b. The subsequent independently accepted arithmetic freeze proves that this same bit-exact map preserves addition, multiplication and inverse at every level, giving actual RingEquiv and AlgebraTowerEquiv bundles. Five fresh leaf checks and the sweep of 26 reportable declarations owned by those modules pass with only standard axioms; an independent client checks the existing algebra-equivalence/scalar API. Its manifest is 9d6584d2cb4b9b5dc61a7742ba3e6f5c14354114e130a59e8b61d80fa3a69152. Two subsequent local scratch milestones are also independently accepted. The all-level relative basis connects executable coordinates and packing to the actual chosen scalar actions and Basis.repr; the actual CompPoly additive NTT has a universal evaluation theorem under its existing strict dimension bound. Five fresh leaf checks and 87 owned-declaration closures pass; a complete GF16 output table and valid normalized-basis permutation controls fix the intended order. Source inventory: 6a3bba7cd1e2e1caf16ec5f68e0f074c5b47a1b052bf07efd80d39e0bb723516.

The nominal flat-word adapter has explicit encode/decode roundtrips, fixed operations, all 18 checked Field data projections, direct bit embeddings, and actual flat-valued successor/two-step basis and packing clients. Thirteen fresh leaf checks and 191 owned-declaration closures pass with only standard axioms; independent symbolic, GF16, 128-bit encoding and wrong-order controls pass. Its multiplication and inverse still convert through recursive coordinates. Manifest: 373f0cf50ea1ad9aeb6df2bd558d1830cb4cdba217ff3c02f4256808d1f1b0c5. This accepts the storage adapter, not a direct packed backend or a production migration.

The direct packed-kernel scratch freeze is now independently accepted: named schoolbook and normalized multiplication and norm-descent inverse operate on flat bits, with all-level correspondence under the fixed encoding. Six fresh leaves and 40 owned-declaration closures pass with standard axioms; asymmetric-field and four well-typed wrong-output controls pass. Manifest: 5264ee6b81637a2e1605449547b7931b26713b6d5b4c8c178a8f4457fffc5a5c. The Flat Field assembly still uses the conversion adapter; these named functions do not silently replace its operations.

The first accumulated-product consumer freeze is also independently accepted. It proves correspondence to the existing executable Vector.dotProduct using an additive reduction law, with no injectivity or associativity needed for the exact ordered fold. Recursive, flat-adapter and direct packed schoolbook arms produce the same full output words at every level and vector length. Three fresh leaves and 40 owned-declaration closures pass; independent checks of noninjective/nonassociative models, GF16 products and partial sums, a 128-bit word, and four wrong-output controls pass. Manifest: 8cdacbd952ef63cbd01ee8ff53936461d8e155530532e32f46e1787916e6e9af. All three arms remain eager. Their linked native validation is now independently accepted: a fresh private build reproduced both executable hashes, all 280 full-word output records were checked against an independent three-product arithmetic reference, and actual dropped-term and high-half output mutations were rejected. The high-half case preserves the low 64 bits, so the check exercises the full 128-bit result. Selected compiled call paths, pinned link inputs and process cleanup were independently checked. Native source inventory: a9063a3676f4956efe04edcb7da67425900e3ad2a428f304c670695e017e5c9c. This admits the named eager schoolbook consumer executable for these finite cases; it does not establish a genuine unreduced-product backend or comparative performance.

A separate nominal packed Field and actual additive NTT scratch candidate is now independently accepted. All 18 Field operation projections select fixed raw data; multiplication and inverse call the named direct packed kernels. The direct prime embedding and one-hot basis preserve the chosen scalar action and encoding. Universal theorems prove both polynomial evaluation and correspondence of the actual CompPoly function-based NTT with the recursive transform under the existing strict dimension bound. Twelve fresh candidate leaves pass a 201-owned-declaration standard-axiom audit. Independent probes additionally check scalar actions, zero stages and complete transform outputs with nontrivial normalization; separately reproduced controls check valid basis permutations and rejection after actual raw kernels are retargeted to mathematically equal conversion adapters. Source inventory: 09d61385d01ff9f8c450e9db1ab6366ed2603788c38c903daf81202e3904753f. An unused recursive proof import was removed during review.

Linked native validation of this packed Field and actual function-based NTT is now independently accepted. The corrected source inventory is 228f95b95ebc6ed9f3b8e222de0470c73d5052715f58ae048690d020f562b0d9. Independent fresh builds reproduce both executable hashes; all 1,222 frozen full-word records and 24 additional outputs pass. A separate schoolbook/Fermat-inverse reference checks the expectations. Actual high-half and valid reordered-basis mutations reject, and compiled-path inspection detects mathematically equal conversion adapters. All 18 generic Field projections were independently traced through the actual generated constructor and projection code. Fresh source audits cover 463 owned declarations plus the two separate entry points, with standard axioms only. Review repaired an inventory suffix error, and the complete rerun checks all 2,119 reused native objects and their generated C/object traces. The level-seven sparse NTT case checks exactly four indices in a size-2^65 domain. This is finite native implementation evidence alongside the universal pure proofs; it supplies no performance ranking, compiler proof, full-domain coverage or construction decision.

CompPoly #334, draft at db0d4c60cb55bce2713a8c1a308cc296261995bd and stacked on #333, promotes reusable coordinate composition into the existing AlgebraTower owner. Adjacent linear equivalences give executable coordinates, packing and basis vectors over any number of steps, with the same actual Mathlib basis representation and old-index-fastest order. Variable and zero coordinate counts, chosen scalar actions and unnormalized successor vectors are supported. Independent adversarial public clients include reversed coordinates, a noninjective middle ring map and a signed rank-one presentation. Full source/test/style/import/docs gates, the 9,897-declaration axiom sweep with zero taint, and all 41 curated benchmark correctness groups pass. Publication followed those reviews and gates; all five GitHub checks now pass, including the exact-head core run 34369157231 and the explicitly dispatched import check. This adds reusable APIs without replacing the recursive field construction.

CompPoly #335, draft at e3dc3550dcad8031d36aaa4ddf43852cbc86bdc4 and stacked on #334, adds coordinate, packing and basis interfaces at arbitrary endpoints h : i ≤ j, accepting A j directly with the selected tower action. Constant successor counts have normalized Fin (r ^ (j - i)) coordinates with unchanged numeric indices. Full owner gates pass, including the 9,918-declaration axiom sweep with zero taint and 41 benchmark correctness groups. Independent review rebuilt the changed leaves and adversarial clients for signed coordinates, reversed shifted coordinates, actual scalar reconstruction and noninjective maps; two false output claims reject in the kernel. Publication followed review and validation. All five GitHub workflows pass at this exact head, including the core run and the explicitly dispatched import check. This is a reusable API improvement; it does not replace the field construction.

Additional field and measurement milestones — 2026-09-09

The packed carrier's arbitrary-endpoint embedding and successor-coordinate experimental implementation has passed independent review and root evaluation. Direct bit extension, low/high splitting and joining, chosen scalar actions and the initial #335 coordinate/basis clients preserve the fixed encodings and all 18 canonical Field operations. Fresh checks cover 155 owned declarations plus 17 independent declarations with standard axioms only. Independent GF4-to-GF256 clients validate coordinates, scalar multiplication and ordered basis words; a valid coordinate permutation rejects the original-order claim. Source inventory: 9b3f4727bb2d0c280c31aef40694d9e53cbb945995b1ad1eebdf9e7d2a8b7377.

The packed relative-coordinate and actual ArkLib tensor-profile experimental slice has now passed independent review and root evaluation. Arbitrary endpoints have exact bit-chunk readback, ordered generator-product basis vectors, mathematical basis reconstruction and fixed recursive correspondence. The actual repaired Ark profile has right-linear rows and left-linear columns, with both reconstruction laws and explicit generic scalar-action checks. Fresh checks cover ten modules, seven actual kernel-false controls and 163 owned standard-only axiom closures. Independent proper GF4-to-GF256 clients additionally check complete asymmetric row/column tables and prove the two selected scalar actions differ. Source inventory: 46d0f17c0290f46d73d4f44b7663f0736c9863222cd7b564f43a1615b35e7a6f. The expected-type replay records a real elaboration boundary: local right-action instances alone do not reliably determine an unqualified scalar expression on the profile carrier; the accepted statements select the actual action explicitly. This is source/proof admission, with no full packMLE, native tensor implementation or B5-completion claim.

The existing concrete tower now has an independently accepted low-first successor adapter derived from its own public split/join and scalar laws. It instantiates the same #335 endpoint interface and identifies the one-step basis with the actual legacy basis at unchanged indices, preserving the original Field. Six fresh modules, four actual kernel-false controls and 97 owned standard-only closures pass; independent clients check the actual basis object, all 18 Field operations, skipped coordinates and complete 128-bit readback. Source inventory: ee4d1203b4481fc245b3f0d2e200c79b4281aa63e9d57dad1beef123fc9f9eb0. This adapter does not use the competing construction to certify its laws. Its universal full relative-basis correspondence and actual NTT/packing clients are the next work, alongside matched recursive clients and separate cross-arm diagrams.

A separate named generator-multiplication kernel over flat words is also independently accepted. Its low-first recurrence uses one smaller generator call and no general multiplication or recursive-coordinate conversion; universal proofs identify it with the fixed own-ring generator product and both schoolbook operand orders. Three fresh modules, four genuine wrong-output controls and 18 owned standard-only closures pass, with additional independent full-word probes. Source inventory: fc9e0ae6146383e4f6b404840977b4ea17f418d449ea78c703838d9b45cef653. This adapts the existing CompPoly mulByZRec recurrence with attribution. It changes no canonical multiplication, inverse or Field, and has no new native or timing result. It neither attributes the measured schoolbook slowdown to the generator term nor establishes that this optimization fixes it.

The B9 schoolbook cost panel has completed all 50 cohorts and both control sets: 1,800 ordinary observations, 150 matched-floor observations and 80 global controls. Independent evaluation and root review accept the complete dataset as a bounded descriptive result. All 2,097 selected source/artifact hashes remain unchanged; all processes completed with clean teardown. The three arms are the new independently assembled recursive schoolbook implementation, the flat conversion adapter and the direct packed schoolbook implementation. The current library's canonical arithmetic is not a timed arm. The separately reviewed scheduler amendment raised the uniform cohort limit to 360 seconds while retaining the absolute 1,800-second deadline and every frozen workload and validation condition. Source inventory: 2a6ad362eb10f58d7e686d7823c639c1d7a015f60df218f02819128c4f23763c.

In each of the 24 nonempty larger-level cohorts, the direct packed schoolbook arm took longer than both other arms in every retained paired round. At level 7, the length-16 raw-input cohort had median paired C/A 20.56 (observed range 13.49–25.71) and C/B 17.00 (11.94–21.03), with A/B/C referring to the three arms in the order above. These are per-workload observations, not a pooled or stable multiplier. Opening-to-closing floor and canary totals rose about 68%, with substantial variation within some cohorts on the shared powersave host. Close A/B comparisons are unreliable; these observations neither compare legacy canonical arithmetic nor decide flat storage. The current direct packed kernel warrants optimization research with separate proof and native validation.

The first attempt remains separately frozen as incomplete: nine cohorts and 324 ordinary observations preceded a timeout under its original 30-second cohort limit. None of those observations is mixed into the complete second attempt. The original Field-only timing pilot is also retired with zero comparative samples; its dormant dependency copies now share identical-file inodes after reviewed storage recovery, so its old private-cache timing protocol cannot resume against those trees.

CompPoly #336, draft at 118f55f29c7df3b5484ad03adeaeafbf8466eadb, separately corrects benchmark documentation and validation-report wording. Ordinary workloads are untimed in validation mode, while harness controls can retain samples; sink documentation now describes the actual inline dependency. No arithmetic or timing behavior changes. Independent focused reproduction passed before commit/push; all six GitHub checks pass, including the core build/test/axiom/benchmark-validation run and benchmark workflow.

Full construction, imported-client, proof-edit and editor comparisons, canonical multiplication/inverse/embedding/subfield/NTT runtime coverage, architecture selection and production migration remain open. Agents are completing matched actual consumers and preparing the construction/editor harness under the independently reviewed plan. No measurement window is authorized by this implementation work, and no additional roadmap admission checkbox is closed by these experimental milestones.

The independently reviewed full B5 comparison plan remains in force. All reachable CompPoly, ArkLib and candidate proof dependencies will count toward construction costs, including the existing concrete tower imported by the NTT. A complete decision requires the matched construction and editor clients and the separately admitted canonical runtime panel.

The existing #325–#332 drafts now incorporate main bbc26a0980af9eca01c267fc5d5cb296fce69d82 through reviewed base-update merge commits that preserve the original revisions pinned by ArkLib. Each of the eight source trees passes its complete applicable local gates; the top #332 tree also passes a fresh first-party build/test/native/axiom/benchmark gate, with 9,923 reportable declarations across 349 modules and zero admitted/nonstandard taint. All nine gate runs validate the same 186 records in 41 groups with matching semantic checksums. The published #332 head is 81d41f9d0b7ddac805d2996063374fb9399ca728; remote heads, bases and draft status are verified. All five GitHub workflows now pass on each of the eight exact updated heads (40 successful checks), including the explicitly dispatched stacked import checks. These correctness checks are not comparative timing evidence. General transport of coordinates across equivalent towers remains a separate API milestone with a named consumer required before further production work. The retain/refactor/replacement decision stays open. The earlier warm-client timing pilot is retired and produced no comparative samples. No additional roadmap admission gate is marked complete.

Summary

Track the binary-field and Wiedemann-tower work needed for clear mathematical specifications, structural Lean proofs, and implementations that can be executed, verified or generated. Retain the existing concrete representation, arithmetic and construction behind the improved public contracts. The selected tower is admitted in merged source; additional presentation/backend consumers retain their own gates.

The design separates mathematical fields/embeddings/bases, pure executable algorithms, and refined backends. The bounded construction choice is retention; B6 replacement is not applicable. Reuse existing quotient mathematics, trace/irreducibility arguments, packed arithmetic and proof evidence. The jointly validated selected-tower nominality, canonical operations and eager B9-A consumer complete this bounded B5 decision.

This is an execution tracker derived from the 2026-09-08 source/paper review. B1/B2 and the partial repairs listed above are merged; the dated execution sections preserve their earlier review evidence. Diagnostic prototypes do not complete the remaining work packages. The shared B identifiers also identify the corresponding tasks in the ArkLib/Flock trackers.

Existing work to reuse

• #276 already tracks GHASH's noncomputable field instance; keep the implementation work there and use B3-P below for its broader acceptance contract.
• #281 tracks additive-NTT round-index/end-domain compatibility with ArkLib. Reconcile its current scope before changing the tower/NTT consumer boundary.
• #129 tracks carry-less multiplication optimization; connect any selected implementation to B9-A's refinement and workload evidence.
• ArkLib's existing FRI-Binius PR #383 is an important downstream consumer; inspect its actual head before migration.

Work packages and acceptance

• B0 — reproducible baseline and target interfaces. Freeze one compatible Lean/Mathlib/CompPoly/ArkLib/VCVio resolution; reproduce the findings; record build and transitive axiom baselines. Inventory abstract/concrete basis clients, fast fields, additive NTT and ArkLib packing. Write the desired public theorem/encoding contracts before selecting a carrier.
• B1 — tower identity law. Add the missing self-map law to AlgebraTower, migrate every constructor using the binary towers' existing identity proofs, and preserve composition. Include a valid tower and exclude the constant family GF(2) × GF(2) with map (x,y) ↦ (x,x). Check self, adjacent and skipped-level maps. Keep this repair separate from carrier migration.
• B2 — explicit tensor actions. Preserve both maps x ↦ x ⊗ 1 and x ↦ 1 ⊗ x; expose distinct left/right scalar views without competing default instances. Prove both coordinate reconstruction laws and test a proper extension where swapping the views changes meaning. Coordinate ArkLib adapter migration.
• B3-P — presentation isolation. Make the public presentation boundary retain the modulus/construction. Merged #326 isolates extension moduli, and merged #329 repairs the BF64/tower-level-6 carrier collision with a nominal BF64 type. Merged #352/#361 isolate GHASH/the tower, and their explicit maps and negative controls pass in the joint integration. The selected tower is accepted; this broad checkbox does not admit every presentation. Add negative elaboration controls and explicit, proved maps for permitted conversions. This is a type/API hazard, not a claim of kernel inconsistency.
• B3-P — canonical executable operations. Establish coherent multiplication, inverse, division and powers; keep alternatives as named algorithms with agreement proofs or separate backend types. Close #276's relevant execution gap and exercise a generic caller, including inverse at zero. Prove raw-bit/limb encoding round trips and distinguish them from characteristic-two numeral casts. Selected tower accepted: #358/#359/#361 pass with actual generic/native callers; #353 supplies the GHASH operation repair. Other presentations/consumers are admitted separately.
• B3-P — narrow foundations. Separate raw modulus/coordinate/operation definitions from optional finiteness, irreducibility, inverse certificates and binomial/Rabin imports where those are not needed. Admit presentations independently; do not require rewriting every generic-extension consumer to expose one safe field. Selected tower accepted: #363; the AES and GHASH raw leaves are supplied by #356/#365. This is not blanket admission of every field foundation.
• B3-T — tower client API. Provide symbolic embedding identity/composition/injectivity, generator images, successor split/join and coordinate arithmetic, basis reconstruction and LSB-first indexing. Clients should use public laws rather than predecessor casts or construction unfolding. Keep remaining width transport in one owner.
• B5 — bounded construction comparison. Implement the candidates' own assembly, not only a GF(4) arithmetic example. Reuse the quadratic model X² + zX + 1 and its irreducibility invariant. Prove operation-preserving bridges before transporting field laws; prove norm-based inverse agreement. Compare flat storage, lightweight recursive coordinates and the encapsulated existing construction.
• B5 — client and cost evidence. Run identical symbolic self/three-level embeddings, basis/split/join, inverse/zero, tensor, NTT and packing clients; include concrete levels 0, 1, 3, 6 and 7. Measure clean/warm/incremental elaboration, heartbeats, memory, import closure and editor goal latency/readability separately from runtime. Use controlled settings and repeat timings. Exercise each candidate's own executable path. Scope: the expanded incremental/editor cost panel was stopped and is not claimed complete. The accepted bounded retention decision uses the recorded independent construction, symbolic-client, all-level correspondence and native evidence; no performance or editor-responsiveness improvement is claimed, and this panel is not a pending prerequisite for that decision.
• B9-A — arithmetic and one real consumer. Prove the selected backend interprets as the mathematical field and one named accumulation/fold/NTT consumer agrees with the scalar reference. Include native execution and encoding contracts. Record (presentation, backend, consumer, exact revision), theorem closure and workload results. Accepted scope: the eager FastBT128/ConcreteBTField 7 coefficient-evaluation record in Current status; other consumers are not admitted.
• B9-A — optional optimized capabilities. Keep wide accumulation, mixed products, generator scaling, squaring, packed lanes and Frobenius/norm kernels consumer-driven, with a proved eager fallback. Prove multiplication/reduction and additive-reduction laws. Require total accumulators or validity predicates closed under zero, fresh products and accumulation; shifts must preserve/update headroom or reduce overflow. Include highest bits, repeated shifts, empty/cancelling sums, limb boundaries and partial SIMD lanes.
• B5 decision — record retain/refactor/replacement choice. Correctness is mandatory; judge clarity, proof structure, implementation refinement/generation, usability and measured costs. Final selection requires B3 and candidate-specific B9-A evidence. Migration effort controls staging, not the quality target. A BF64/Ext3 consumer alone does not validate a Wiedemann candidate. Accepted bounded choice: retain, with selected-tower B3-P/B3-T and eager B9-A evidence in Current status. No replacement migration or further comparison campaign is requested.
• B6 — conditional migration and retirement. If replacement is selected, prove all-level coherent equivalence, embedding/generator/basis/encoding transport and backend agreement before retiring old internals. Migrate every inventoried consumer and give temporary adapters a removal plan. If retention is selected, mark B6 not applicable with the decision linked here. Not applicable: retention is selected in Current status; no replacement migration is requested.

Sequencing and scope

Start B0/B1 first; after a reviewed, passing B1 patch, Flock F0–F2 can begin alongside the remaining work. This is the project's scheduling choice: AES/GHASH and BF64/Ext3 do not mathematically depend on the Wiedemann construction.

B3-P can start after B0. B3-T needs B1/B3-P and B2 for tensor clients. The bounded B5 comparison is accepted for retention with the selected tower's B3-P/B3-T and eager B9-A evidence. B6 replacement migration is not applicable.

Keep GHASH, polynomial-basis BF64 and cubic Ext3/F192 as distinct presentations. Equal width is not a multiplication or serialization equivalence. Generic field/polynomial algorithms belong here; protocol schedules, oracle reductions and security composition belong in ArkLib. A real Flock arithmetic consumer can proceed without full tower migration or full Binius proof closure.

Evidence baseline

• CompPoly 3468b38c8fd270f93f55a259220a8abc544e7437: tower support, tower, extension definitions, GHASH.
• DP23, Succinct Arguments over Towers of Binary Fields, §2.3; DP24, Polylogarithmic Proofs for Multilinears over Binary Towers, §§2.3/2.5 and Construction 3.1. Reviewed PDF SHA-256 values: DP23 14f965bbc20d9bb4cb005f009dac7494c895c2a27f8cbecd44413d031d740799; DP24 9e8f30b7994e6f4cec6df76f45fd7520c9bc5b8c8c3d99212f0567bc7045de77. Later downloads may differ.
• Backend comparison: Binius64 6e75a2d and leanVM a386121. Their polynomial fields and wide kernels are refinement targets, not an instruction to copy their representations into the tower.

Tracking and completion

Keep this checklist current as packages are split into linked issues/PRs. For each active package record its owner, exact revision, public contract, dependencies, status (planned, in progress, review, blocked, done) and evidence. Do not mark a package complete merely because a prototype compiles or a PR is open.

Acceptance requires independently reviewed statements, concrete valid instances and load-bearing negative controls, standard-axiom theorem closures, native tests for execution claims, and CompPoly's required build/test/style/axiom gates. Preserve upstream attribution. Generated/native execution and differential tests are implementation evidence; Rust/CUDA/compiler correctness needs its own explicit correspondence boundary.

Active execution — 2026-09-08

• B1 — done: PR #324 merged on 2026-09-08 as b082daf2faa1cc74a572929bebe96bceae28d10a. The algebraMap_self' law, both constructor migrations, public simplification lemmas, and focused contract/embedding regressions are accepted. Independent correctness/polish reviews, full CompPoly build/test/style/import/docs/axiom gates, and selected ArkLib compatibility builds passed before publication. The CompPoly axiom sweep covered 9,873 declarations with zero admitted or nonstandard-axiom dependencies; existing ArkLib protocol proof gaps remain separate. This completes B1 only.

• B0 — in progress: the bounded B1 baseline is validated at CompPoly 3468b38c8fd270f93f55a259220a8abc544e7437, Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. A fresh unmodified source build/test and axiom sweep passed, with pinned dependency caches reused. Both production constructors and the basis, bridge, fast-field, NTT and ArkLib packing consumers were inventoried. ArkLib bcddd0897dc1b602a44f964c21e76fa6a5b29440 builds the selected packing/Binius consumers against the candidate while retaining its other dependency pins. Existing protocol sorryAx remains separate from arithmetic acceptance. The PR records validation details; broader public-contract and controlled performance/infoview work remain open.

• B2 — review: CompPoly PR #325, head 9b14b21c41d1bee4116bde7ba5c2257c5765f5a0, moves the generic right-action basis into its neutral owner and preserves Mathlib defaults. Independent adversarial reviews caught and repaired incomplete local action setup: equal-factor clients select Algebra, Module, DistribMulAction, and SMul coherently. Both reconstruction directions, coordinate recovery, ordinary module laws, scalar towers and proper-extension negative controls pass. Full build/tests/style/import/docs and axiom sweep pass (9,865 declarations; zero admitted/nonstandard taint). ArkLib PR #894, head b3e649711652d88f3a9f9b3cec300b23cb76d060, migrates the packing consumer with full exact-pin validation and no new axiom debt. Both PRs are drafts; B2 is not yet marked done.

• B3-P nominal carrier — review: CompPoly PR #326, head 10cf26348962c8fdee51a341d7abed6445442540, is stacked on #325. Ext P now retains its presentation in a one-field structure, with explicit coordinate maps and canonical operations. Independent mutation checks demonstrate that both implicit reinterpretation and mixed canonical multiplication detect the old alias defect. Full build/tests/policy and axiom gates pass (9,880 declarations; zero taint), and all eight native extension multiplication/inversion workload checksums match the vector baseline. This is a partial B3-P milestone. Subsequent drafts #327/#330 address raw arithmetic imports/parameters; encoding and embedding admission and the tower construction decision remain open. The separately reviewed ArkLib sampler PR #895, head 20729d19fe4ae427955f8f2e46418b5ab2a215a4, now passes full exact-pin validation with unchanged sampling semantics. CompPoly import cleanup PR #327, head 0d8e2f163bb24f2fb023d515a0523d1ffba662f2, removes the unnecessary binomial-proof import from generic extension definitions; its declaration bodies and parameter requirements remain unchanged. It passes independent review and the full build/test/policy/axiom gates (9,880 declarations; zero taint). Both are drafts; subsequent #330 supplies the raw parameter/cardinality-certificate separation, while broader symbolic tower clients and the construction comparison remain open.

• B0 integration evidence at the recorded #325 pin: ArkLib 8d7e758b5c4421711358595870ff7fbcee2a3a9f plus the #894 adapter passes the complete ./scripts/validate.sh --axioms gate against the exact #325 pin. All other dependency records are unchanged. The sweep covers 11,457 ArkLib declarations in 452 modules, retaining 291 existing sorryAx-tainted declarations and zero nonstandard-axiom taint. Dependency caches were reused; this is not a cold-build performance measurement. Controlled build/editor profiles and the broader construction comparison remain open.

Each self-contained milestone uses a separately reviewed draft PR. No final refactor-versus-replacement decision is implied by these boundary repairs.

Independent follow-up review — 2026-09-08

Independent review found no mathematical correctness defects or introduced regressions in CompPoly #325–#327 and ArkLib #894–#895. These are bounded tensor, nominal-extension, import and sampler repairs; they do not change BinaryTowerAux or settle refactor versus replacement.

• Historical presentation finding (2026-09-08). At the assessed pre-repair revisions, BF64/tower level 6 and concrete GHASH/tower level 7 accepted implicit crossings even though raw word 2 squares to word 4 in the polynomial fields and word 3 in the tower. Draft CompPoly #329 now repairs the BF64 carrier boundary with explicit bit maps and negative mixed-presentation controls. GHASH/tower isolation and protocol-specific encoding/embedding admission remain open.
• Performance evidence has a limited scope. #327 reduces the narrow extension-definitions import closure; existing concrete-field and tower basis closures are unchanged. Eight native workloads tested in alternating runs matched checksums with median ratios 0.93–1.02. These checks support no obvious regression on those workloads, not improved tower construction or editor responsiveness.
• Experiment status at that review. The early candidate then had only raw encoding/arithmetic evidence. The current production repairs and independently accepted all-level B5 proof/native experiments are recorded below. Construction selection and controlled cost comparison remain open.

The main-only import checks were also dispatched for the exact stacked CompPoly heads: #326 imports at 10cf26348962c8fdee51a341d7abed6445442540 and #327 imports at 0d8e2f163bb24f2fb023d515a0523d1ffba662f2 both passed. ArkLib #895’s dispatched core workflow also passed at its exact reviewed head, including build/test/native/axiom checks and documentation generation.

B3-T API slice — review: CompPoly #328, draft at 64c418fddb16ad99cd4d261033c56386951d2e69, exposes the executable NTT basis correspondence and tests symbolic reconstruction and coefficient recovery, including level zero. Two independent correctness/polish reviews and all local build/test/style/import/docs/axiom gates passed before commit/push (9,881 declarations, zero admitted/nonstandard-axiom taint). This does not change arithmetic or recursive construction. The separately reviewed nominal BF64 milestone is CompPoly #329, draft at 5d32f85d6452aba2e6bdd5e5ca1dfcd7f7c1ffad. It adds explicit bit maps, coherent parity-based field numerals, and mixed-presentation/canonical-operation controls. Two independent reviews, full CompPoly validation (9,912 CompPoly declarations with zero taint plus explicit BF64/Ext3 closure checks), native linking and the complete ArkLib integration gate passed before commit/push. That nominal-carrier patch alone did not repair standalone startup; draft CompPoly #331 now supplies the separate repair described below.

Historical native startup diagnosis — 2026-09-09, before #330/#331

Before #330/#331, a separately linked BF64/Ext3 client exposed a startup defect: the computable BF64 Fintype initializer eagerly enumerates Fin (2 ^ 64) before main. The same client passed lean --run; successful evaluation or linking alone therefore does not establish standalone native execution. Generated-C inspection independently confirms the enumeration. A one-line noncomputable-Fintype experiment was rejected because the then-current generic extension constructors, arithmetic and equality still required that data dictionary and failed compilation. No executable operations were made noncomputable to hide the problem.

The resulting raw-parameter/certificate separation and BF64 startup regression are implemented in reviewed drafts CompPoly #330 and #331 below. This historical defect is repaired in that stack; broader B3-P and protocol-specific field admission remain unchecked.

Raw arithmetic/certificate milestone — 2026-09-09

CompPoly #330, draft at 4a1b09f211efe30312c2a62012e51fdf3c776e5c, removes enumeration data from extension parameters, coordinates and executable operations. Field certification separately requires Finite, correct Nat.card and irreducibility; canonical operations are preserved. Negative controls reject wrong cardinality and an infinite field with true Nat.card = 0, while symbolic iterated extensions remain computable without enumeration dictionaries.

Two independent correctness/polish and adversarial reviews passed before commit/push, along with full CompPoly build/tests/policy checks, a clean 9,921-declaration axiom sweep, and all eight existing native extension workload checksums against the recorded baseline. Full ArkLib integration passed with 291 existing admitted dependencies and no new or nonstandard axiom debt; all 19 other dependency records stayed unchanged. This establishes the generic prerequisite. The separate BF64 global-finiteness and bounded native-startup repair is now draft #331, described below; the existing BF64 initializer is unchanged in #330. Neither milestone decides the recursive tower construction.

BF64 native startup repair — 2026-09-09

CompPoly #331, draft at d77ffb9ed5edf5c9064ee4d42eeea915efb51040, addresses the startup defect described above. BF64 now supplies proof-only Finite; BF64/Ext3 cardinalities use Nat.card, with compatibility theorems for explicitly chosen enumerations. Canonical arithmetic and bit encodings are preserved. The existing core CI workflow now builds and runs a dedicated linked BF64/Ext3 smoke executable under documented memory and timeout bounds.

Two independent mathematical/polish and adversarial reviews passed before commit/push. Full CompPoly build/tests/policy checks and the 9,923-declaration axiom sweep pass with no admitted or nonstandard dependencies; selected root BF64/Ext3 closures are also clean. Full ArkLib integration again retains its 291 existing admitted dependencies with no new or nonstandard axiom debt and unchanged other dependency records. The actual new linked target passes, including independent runs. Under identical bounds, restoring only the old enumeration instance causes startup allocation failure, while changing one expected product bit causes the named arithmetic failure; both mutants build successfully before execution.

This provides a reviewed repair and an enforcing regression gate for the demonstrated BF64 startup defect. It does not complete protocol-specific field admission or the GHASH/tower presentation work. All four new production PRs, CompPoly #328, #329, #330 and #331, remain drafts with all CI checks green at their recorded heads. #331's core run includes the linked-native startup/arithmetic gate, axiom sweep and existing benchmark suite. ArkLib #895's stacked-PR core coverage gap is also resolved by the exact-head successful run linked above. No additional roadmap gate is marked complete.

Historical initial B5 experiment — 2026-09-09

The following scratch, unpublished implementations have passed independent reviews and root evaluation; they are evidence for the construction comparison, not a production design selection.

• Own all-level ring/Field/trace assembly: the nominal recursive carrier has canonical arithmetic, characteristic two, proof-only finiteness/cardinality, a nonzero generator and both generator traces. Its own norm inverse is certified through an operation-preserving quadratic equivalence; no legacy successor Field is used to supply the laws. All 18 executable Field projections are fixed independently of Prop-only certificates. Symbolic cancellation/zero inverse and a concrete bad-quadratic failed-cancellation control pass; selected proof closures contain only standard axioms. Proof manifest: 38cd8f669db5b3c9f3d16a5bde98ffe7863ab09c466c041de8dbba5b3e797585.
• Four-product normalization: a separately named Karatsuba recurrence matches the legacy successor call/operand ordering and is proved equal to the candidate's schoolbook multiplication at every level. It does not replace canonical multiplication or establish equivalence to the old bit-vector implementation. Manifest: c086b3cb971f72dd8678e7eb7adf2cf28db00ec86783bf211979de1be5c5b50c.
• Linked candidate execution: the actual schoolbook Field dictionary is passed to unspecialized generic multiplication/inverse/division/power/scalar helpers. Bounded runs compare values with clean CompPoly d77ffb9ed5edf5c9064ee4d42eeea915efb51040: all pairs at levels 0/1 and fixed inputs at 3/6/7, including zero. The 4 GiB / 30-second / 5-second grace gate passes with core dumps disabled; a one-bit expected-product mutation fails as intended. The seven inspected candidate-owned generated C modules contain no finiteness-enumerator or recursive certificate runtime symbols. Native manifest: 169904ca802f8d4c5f8f300e59834c85b9b41dbd76ea006159b81d95966bb9bf.

Universal legacy correspondence, typed embeddings and bases, NTT/packing consumers on this candidate, a flat refinement and the full controlled cost comparison remain open. The named four-product algorithm is not the path exercised by this native Field harness; the legacy control also has representation/base-case/fast-path differences. No performance win, retain/refactor/rewrite choice, B5/B6 completion or Flock field admission follows from these experiments.

This roadmap names no source files or tests and records extensive work already merged across PRs #325–#365, with downstream pinning in ArkLib #899. Start by reviewing the remaining scopes explicitly marked open, including B4/B7/B8, B9-V and Flock F0; a suitable contribution would need a separately bounded task with its own acceptance criteria and validation plan.