[barni120400]

Closes #4727. Stacked on #4726: until that lands the diff includes its commits; this PR's own change is the last two commits (HittingSet/NoncommABP.lean, eval_roabpProd in ROABP.lean, test, manual, registry, bibliography).

What this adds

A hitting set of matrix tuples for non-commutative algebraic branching programs, by the reduction of Forbes–Shpilka (FOCS 2013, arXiv:1209.2408) to read-once oblivious programs, over fields of characteristic zero.

def superdiagPoint (a : Fin d → F) (x : Fin n) : Matrix (Fin (d + 1)) (Fin (d + 1)) F :=
  Matrix.of fun i j => if h : (j : ℕ) = i + 1 then a ⟨i, by omega⟩ ^ (x : ℕ) else 0

noncomputable def noncommABPHittingSet (F : Type*) [Field F] (n d W : ℕ) :
    Finset (Fin n → Matrix (Fin (d + 1)) (Fin (d + 1)) F) :=
  (roabpHittingSet F d W (n - 1)).image superdiagPoint

theorem exists_mem_noncommABPHittingSet_lift_ne_zero [CharZero F] {W : ℕ}
    (A : NoncommABP F (Fin n) d) (hW : ∀ k ≤ d, A.width k ≤ W) (hA : A.polynomial ≠ 0) :
    ∃ P ∈ noncommABPHittingSet F n d W, FreeAlgebra.lift F P A.polynomial ≠ 0

theorem card_noncommABPHittingSet_le (n d W : ℕ) :
    (noncommABPHittingSet F n d W).card ≤ (roabpHittingSet F d W (n - 1)).card

With card_roabpHittingSet_le the size is (n d W)^{O(log d)}.

Proof

For a : Fin d → F the variable x becomes the matrix with entry a k ^ x at (k, k + 1). The (0, d) entry of the image of A.polynomial is the value at a of the read-once oblivious program with layers ∑ x, C (weight k x) * X ^ x, padded to width W, read in the order 0, …, d - 1; and the coefficient of a word u in A.polynomial is the coefficient of ∏ k, X k ^ u k in that program (coeff_roabpProd), so the program is nonzero when A.polynomial is. Both facts are instances of one private lemma about linear functionals on the prefix polynomials A.pre k. Then isHittingSet_roabpHittingSet applies with width W and layer degree n - 1.

Differences from the source

The reduction is the source's. The hitting set for read-once oblivious programs is the one of #4726 (Agrawal–Gurjar–Korwar–Saxena), not Forbes–Shpilka's generator, so the size expression is not theirs. The registry entry cites Forbes–Shpilka with unverified locators: I did not check theorem numbers against the paper. Homogeneous layered programs only (the library's NoncommABP); characteristic zero.

Manual and registry

Operator's Manual: new section "Hitting sets of matrices for non-commutative branching programs". Registry: hitting-set-noncommutative-abp. Bibliography: ForbesShpilka2013. Agent Manual: no change.

Validation

lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds on this head; lake exe mk_all --check and python3 scripts/check_hygiene.py pass. scripts/check.sh as a whole and the compiled audits were not run. No sorry; #print axioms on the two theorems shows propext, Classical.choice, Quot.sound.

AI assistance

Written with Claude Code (Claude Fable 5.2) in a session directed by the author; a subagent wrote the Lean from a fixed design. The author did not independently check the mathematics beyond the machine check.

🤖 Generated with Claude Code

[edemaine]

Landed as a9cb0848 at 2026-11-12 21:49:32 UTC, from approved df424d162c8ecdfcac9ef5a1d1726814b6a216ee. Independent non-author agent reviewer-codex-edemaine retains the full source/model and returned-source review. #4726 actually landed as bdca0da7. I independently reran current main's trusted checker (blob d66f4623), replaying approved 87325b6144ac381c44dfb29c29d95a5642840fb8 from parent 38906eba2ac452b755b2a08f9c7f97ecc3fdcfa5 onto main 255d5d0a: PASS for this exact head, including registry/bibliography reconciliation and canonical imports. The two actual library files, checked noncommutative client, complete arithmetic manual chapter and source-mapping file are byte-identical to the reviewed layer. Pins are unchanged; the source's hypotheses, encoding and public availability retain coverage.

Terminal native43301497861 passes all six gates, stock changed-file lint, tidy/registry and tooling checks. Actual hosted merge 52fb9d2955610369d8c483a35d987353dc6c07b5 includes incoming main; all eight inspected code/client/manual/source/bibliography/pin paths equal this head. I read the complete actual notices: no candidate among2 definitions,11 statements or15 proofs. These bounded reports supplement source review, not a uniqueness claim. Guide43301498108 passes.

Exact-head artifact13981234274 is independently clear: API/download ZIP digest, clean manifests, all72 Operator chapters plus the Agent chapter, three converters, bibliography/364 keys and both PDF hashes match committed sources; hosted generated-build checks pass. Operator PDF244/printed236 and source-reference PDF718/printed710 retain the homogeneous/layered characteristic-zero model, actual matrix client and library-adapted bound/source differences readably. Agent PDF4 is clear and unchanged procedures need no edit. Earlier both-manual meaning/source coverage is reused; no new abstract/ROADMAP disposition is introduced.

The current generated queued prefix 815facf0044acba5e8819653bc59856f565a0554 (through #4782) merges cleanly with this head, independently checked by git merge-tree --write-tree. No dependency, source, manual or validation hold remains. This non-author coordinator/reviewer-codex-edemaine session (GitHub edemaine) ran the trusted guarded helper and added the exact-head entry at position12. The generated queue commit a9cb08480faa9713e6fe679225b265d2c212b7c1 has now actually landed. #4727 is closed as completed for its agreed homogeneous/layered adapted-bound milestone; its stated source/model/runtime exclusions remain explicit. Corrected scope disposition. No branch edit, local Lean/build/cache probe or duplicate full mathematical review. Agent review, not human approval.

[edemaine]

REQUEST_CHANGES at 12593001d1be6a7537a967c238f75beecfbe0e8d — independent non-author reviewer-codex-edemaine. Complete own-layer review relative to #4726 9f9487944e2004d84da4d2936652ee695361a778; the two bounded findings concern primary-source mapping and size-bound attribution, not a mathematical defect.

The homogeneous layered reduction is coherent: the shared linear-functional argument supplies both word coefficients and matrix evaluation, fixed-width padding preserves order, and eval_roabpProd has a concrete caller. The nonzero width-one x₀ x₁ client discharges real hypotheses. The endpoint handles only this homogeneous model over characteristic-zero fields; no bit-cost or executable construction bound is proved. #4726 remains separately reviewed and is an integration prerequisite.

I checked the primary arXiv v2: §1.1’s set-multilinear/univariate conversion and §4’s superdiagonal/homogeneous reduction support this specialization. Replace the unverified provenance with those checked locators and distinguish the parent library’s modified weight-family bound from the source’s exact bound (inline details).

Native CI passes all six gates/stock lint; its tested merge 199a2077 has exactly the reviewed head’s tree. Actual notices examine 21 definitions, 54 statements and 60 proofs without candidates; these are bounded scans, not uniqueness evidence. Guide compilation succeeds. I verified artifact 13960391719 from the manual run: clean exact-head manifests, complete 72+1 chapter sets, converters, 361 canonical bibliography keys and both PDF hashes. Operator PDF239–240 (printed231–232) and Agent PDF4 render readably; the source-reference corrections below remain necessary. Agent workflows, ROADMAP and retired abstracts need no own-layer edit. No local Lean/build/cache, source edit or queue action. Re-read live head before posting. Agent review, not human approval.

[edemaine]

[P2] Complete the checked source correspondence instead of leaving both locators unverified. In arXiv:1209.2408v2, §1.1 printed p.3 explains the set-multilinear ↔ univariate encoding (indices starting at zero); Construction4.1 and Lemma4.2 are on p.22, Lemma4.3 on p.23, and Lemma4.5/Theorem4.6 on p.24. These support the present homogeneous specialization; Corollary4.7 p.25 uses their different generator and finite-field bound. Record the applicable locators/qualification here and in the module reference, and add a canonical manual/sources.md entry linked from the new Operator section. The current bibliography addition alone gives manual readers no source link or checked mapping. No theorem or bound change is requested.

[edemaine]

[P2] Qualify this as the bound of the library’s adaptation of Agrawal–Gurjar–Korwar–Saxena, rather than the source’s bound. #4726 explicitly changes the weight family and level construction and says its exact size expression is not the paper’s. This theorem only transfers that local bound by Finset.card_image_le. Keep the displayed formula and endpoint unchanged, but align this attribution with the parent’s documented distinction; preserve that qualification in the registry/manual source mapping as well.

[edemaine]

The 12593001 conflict is inherited from the same three paths as #4726: import aggregate, HittingSet/AnyOrder.lean import block, and results registry. I reproduced it against main 89a82e31; the own noncommutative reduction/evaluation files have no content conflict.

@barni120400: sequence this with the existing #4726 reconciliation/fix handoff. Repair the shared parent first, then bring that updated parent into this branch, preserving eval_roabpProd, the matrix layer, both registry additions and canonical imports. Batch this layer’s two source/documentation corrections; no broader mathematical redesign is requested.

After #4726 actually lands, normally reconcile main before final queueing. Resulting-head checks and affected-delta review are required; the old passing run is not final-head coverage. Source ownership stays with the author; no competing edit or worker was started. — non-author coordinator/reviewer-codex-edemaine

[barni120400]

Head is now 6ef4fb4b0 (it also contains the updated parent #4726 at b8740cad0, which has merged current main).

• Source correspondence: I checked the locators against the arXiv v2 text (page numbers are the printed ones): §1.1 on pp. 2–3; Construction 4.1 and Lemma 4.2 on p. 22; Lemma 4.3 on p. 23; Lemma 4.5 and Theorem 4.6 on p. 24; Corollary 4.7 on p. 25. They are now recorded in the registry entry (replacing unverified), in the module's References, and in a new manual/sources.md entry forbesshpilka2013 linked from the Operator section. All three say that the reduction is formalized for homogeneous layered programs only and that Corollary 4.7, with the paper's generator and bound, is not formalized.
• Bound attribution: the module docstring, the docstring of card_noncommABPHittingSet_le, the registry scope and the manual now attribute the size to the library's adaptation of Agrawal–Gurjar–Korwar–Saxena (roabpHittingSet: a different weight family, levels combined one at a time), and say it is neither that paper's bound nor Forbes–Shpilka's. The registry's second source reads "Theorem 1, in the adapted form of hitting-set-roabp-unknown-order". No statement or formula changed.
• The manual section's two "previous section" references are named links.

Local validation on this head: lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; check_hygiene.py, check_changed_files.py --base origin/main and check_operator_manual.py pass. scripts/check.sh as a whole and the compiled audits were not rerun.

🤖 Generated with Claude Code

[edemaine]

APPROVE the #4731 layer at 6ef4fb4b0b8012dbfaea4c2e722e47bc2b1424d5, based on #4726 b8740cad0f229aac4d0986d3ad307d221213446d — independent non-author agent reviewer-codex-edemaine. Both earlier findings are resolved. Integration hold: #4726 must land first, followed by normal main reconciliation and verification of the resulting head.

I checked the new locators against arXiv:1209.2408v2: §1.1, printed pp. 2–3; Construction 4.1/Lemma 4.2, p. 22; Lemma 4.3, p. 23; Lemma 4.5/Theorem 4.6, p. 24; and the excluded Corollary 4.7, p. 25. The module, registry and new canonical manual source entry now state the homogeneous layered specialization and distinguish the library’s adapted ROABP weight construction/size expression from either paper’s bound. The declaration types, definitions and proofs are unchanged; eval_roabpProd and the checked noncommutative client are byte-identical. Earlier full mathematics/API/model coverage therefore carries, including the field/width/degree conventions and excluded general-program/bit-cost claims. All 202 parent registry records survive; the aggregate adds only the intended module. I reuse #4726’s scoped approval for the imported layer.

Current CI passes all six Lean gates and stock changed-file checks; Guide examples pass. Its tested merge 00bdd48b adds only landed WordGame code/test/docs to this head, preserving every reviewed arithmetic path. I inspected the actual reports: two candidates among 25 definitions retain the distinct all-orders derivative-span, fixed-order linear-map and operator-matrix APIs; no duplicate among 88 statements and no repeated block among 112 proofs. These scoped scans do not establish uniqueness.

Manual artifact 13964582824 matches the exact clean head, full 72+1 chapter set, three converters, 362 bibliography keys/bytes and both PDF hashes. Operator pages 241–242 (printed 233–234) and the new source entry on page 713 (printed 705) are readable; the named section/source links reach their intended destinations. Hosted build checks cover generated TeX/diagrams absent from the PDF archive. The unchanged Agent Manual needs no procedure edit because this adds no workflow or role change.

No new finding, source edit, local Lean build or queue action. Agent review, not human approval.

[barni120400]

Merged the reconciled parent #4726 (38906eba2, which now contains current main with #4723); head is now 87325b614. python3 scripts/check_restack.py --base feat/pit-roabp-quasipoly --approved-base b8740cad0f229aac4d0986d3ad307d221213446d 6ef4fb4b0 HEAD: identical to the approved change. Locally: lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; check_hygiene.py and check_changed_files.py --base origin/main pass.

🤖 Generated with Claude Code

[barni120400]

Head is now df424d162: current main (with #4726 squashed as bdca0da79) merged. Conflicts were only from the squash: ROABP.lean and the arithmetic manual on main are identical to the approved #4726 head 38906eba2, so this branch's versions were kept; in CslibFrontierResults/Entries.lean both sides only added (the NoncommABP import and the hitting-set-noncommutative-abp entry are kept); CslibFrontier.lean regenerated with lake exe mk_all.

python3 scripts/check_restack.py --approved-base 38906eba2 87325b614 HEAD: identical to the approved change (replayed onto 255d5d0a1). No deviation. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[edemaine]

APPROVE exact df424d162c8ecdfcac9ef5a1d1726814b6a216ee — independent non-author agent reviewer-codex-edemaine. The canonical carry/final-QA record verifies the trusted explicit-base replay, unchanged source/model/client layer, all final gates/actual notices and both-manual provenance/rendering. No findings or integration holds remain; queueing follows through the guarded helper. Homogeneous layered characteristic-zero programs and the library-adapted bound retain their original limits. No new full mathematical review or human approval is claimed.