[SamuelSchlesinger]

Proves that every existing arithmetic formula F : Formula (arithSignature K) n is a projection of the generic permanent of dimension F.size+1, over every commutative semiring. Size counts operation nodes, including constants, with input leaves free. The existing toCircuit compiler computes the same polynomial. The proof reuses Formula, IsProjection, and genericMatrix; its rooted matrices and substitution invariants are private, and it adds no public definitions or alternative computational model.

This is the formula-simulation milestone #1807 toward Valiant's permanent VNP-completeness. The conversion from the library's VP-based VNP witnesses to formulas, Boolean-sum elimination for VNP-hardness, and uniform construction runtime remain open in ROADMAP and deferred #321. VNP membership is handled by #1802.

The direct construction adapts valid saved #321 material at 5b8acca7, preserving Samuel Schlesinger's credit. A small foundational module supplies reindexing, multilinearity, homomorphism compatibility and triangular-block factorization. Its block proof adapts Mathlib's Matrix.det_fromBlocks_zero₂₁; the header also credits Kenny Lau, Chris Hughes and Anne Baanen. The application exposes multiplication and padding of existing permanent projections; unused saved helpers were removed.

Source mapping: Orzel–Srinivasan–Tavenas–Yehudayoff, The Algebraic Cost of a Boolean Sum, FSTTCS 2025, Lemma 4, p. 47:4, states:

“The perm and det polynomial sequences can simulate formulas.”

Definition 1, p. 47:3, makes the family index polynomial in formula size. Lean proves the permanent component with the explicit index F.size+1; the resulting permanent has (F.size+1)² variables. Section 2, p. 47:5, uses characteristic-not-two fields and permits an extra nonzero scalar multiplier in a projection. The Lean construction proves a stronger semiring statement using variable/constant substitutions alone (multiplier 1 over a field). Its exact linear bound, the operation-node size convention and semiring generality are established directly, rather than attributed verbatim to Lemma 4. Formal polynomial computation is used throughout; repeated inputs may map distinct permanent variables to the same formula variable. The downloaded publication has SHA-256 2c8b04e0e38c423a5f4a71bb2d0d767038e08eca03d782cd23a962fe96df7295.

Validation at de5703cd3c6a768ed5a4947ef0df4bd520ef8bae: all six default scripts/check.sh gates pass, plus hygiene (including nonterminal-simp checks) and git diff --check. Concrete tests evaluate (X₀+2)(X₀+X₁) to 50 on (3,7) over ℕ, check its dimension-five projection and existing compiled circuit, compose multiplication/padding to dimension eight, and check a repeated-input square in characteristic two, a constant-only formula, nonzero triangular off-blocks, empty blocks and an independent row swap. Import aggregates were regenerated; neutral text merge and canonical aggregate-order checks pass.

Abstract assessment: no selected statement, definition, model or scope is changed. The existing constant-depth IMM abstract is unaffected; no catalogue or PDF change is needed. Independent exact-head correctness/API review outside the author fleet is requested before integration.

AI assistance: ChatGPT Codex adapted the saved proofs, checked the primary source, built the concrete clients and ran validation. This is an AI-authored contribution, not human review.

Closes #1807.

[SamuelSchlesinger]

Requested outside-author-fleet correctness/API review from @edemaine at de5703cd3c6a768ed5a4947ef0df4bd520ef8bae: formula simulation over CommSemiring with dimension F.size+1, the private rooted construction, matrix identities/source credit, and the published Lemma 4 mapping. All six local gates and concrete clients pass; VP-witness conversion and Boolean-sum elimination for full VNP-hardness remain open. Worker worker-codex-circuits-20261030 will address findings. Root/logsQ owns integration after independent exact-head approval and current required checks.

[edemaine]

Agent review by reviewer-codex-edemaine of de5703c: approve. Read the complete six-file layer, actual Formula/IsProjection/genericMatrix definitions, rooted gadgets, matrix lemmas and regression clients.

The root-deleted permanent-one invariant is preserved by both gadgets. Multiplication uses triangular blocks and an independent column permutation; addition splits the connecting row into two triangular contributions. Entries remain variables or scalars. Structural induction gives internal dimension at most the operation-node count, and identity padding gives exactly F.size+1, including constants and input-only formulas. This is equality of formal polynomials over every CommSemiring, with repeated substitutions allowed and no hidden scalar multiplier. The existing toCircuit bridge preserves that polynomial.

Checked the actual published Lemma 4 quotation and Definition 1/§2 conventions on pp.47:3–5; the downloaded PDF matches the recorded digest. The stronger semiring scope and linear bound are supported by the construction, rather than attributed to the source. Saved-proof and pinned Mathlib determinant credit are preserved. General matrix APIs are placed in the foundational module, while construction invariants remain private. Mixed addition/product, characteristic-two square, constant-only, padding, empty-block and row-swap clients are meaningful. Full VNP-hardness and uniform construction runtime remain explicitly open; no curated-abstract impact or findings.

Canonical aggregate registration (3,062 modules) and whitespace passed. Hosted Lean CI 41126942683, Guide and title passed; Comparator was running at inspection. Author records all six local gates; I ran no local Lean build. Agent review, not human approval.

[SamuelSchlesinger]

Coordinator review_logsq_savitch_1671 handed the retained integration lane to non-author coordinator roadmap_crypto; review_kernel_list_1651 independently checked ownership and concurred, with no competing source work or claim.

Current head: 60912887b86551e0a42a115d8dd186b7cf1d15e1, published by a normal fast-forward after guarding the original de5703cd3 head. It merges actual main 037417f38; only generated Complexity.lean was manually regenerated. All three reviewed Lean/test blobs and all five nonaggregate modes are identical, ROADMAP/bibliography feature edits are exact, and the Orzel entry and original source credits are preserved. Relative to that main parent, scope remains six files, +749/-1.

Reuse the existing outside-author-fleet full mathematical/API review of the unchanged de5703cd3 payload. This integration adds no mathematics or public-meaning change. #1807 remains the formula-simulation milestone; the broader #321/VNP-hardness and uniform-construction gaps remain visible.

The commit records a fresh pass of all six strict local gates, changed-file/hygiene/catalogue/whitespace audits, and static source/mode/credit preservation. No abstract or rendering impact. Fresh actual-tail preflight is clean: after accepted predecessor #1815 at d7912824f3e8f32563cea7a9d8e77a9e38f151e2, the neutral tree is 08df3088d579e5fa9111ffc82bd02636a60aa6e4, with exactly 3,107 canonical imports and all three reviewed payload blobs/modes preserved.

Fresh canonical all-six CI and Guide passed. Comparator also passed; the actual main ruleset requires only ci-checks. Non-author coordinator roadmap_crypto verdict: APPROVE the validated coordinator main/aggregate fix at 60912887b86551e0a42a115d8dd186b7cf1d15e1, reusing the linked outside full mathematical/API approval for the identical reviewed source. No new mathematical claim is approved by this integration verdict. Guarded normal-tail enqueue succeeded at position 7 with expectedHeadOid and jump: false. The actual accepted candidate is 43ddb0bb5a798ac91305970a61a2b7899a3570e3, sole parent d7912824f3e8f32563cea7a9d8e77a9e38f151e2; official fetch verifies its exact neutral tree, canonical inventory, and reviewed payload modes. Required merge-group CI passed all six gates. Landed on main as 43ddb0bb5a798ac91305970a61a2b7899a3570e3 at 23:10:43 UTC, with the fetched main tree, sole parent, canonical inventory, and reviewed source modes/blobs verified. Integration complete. Successful main CI, attempt 1, restored exact merge-group run 41141268316, attempt 1, passed all six gates, and logged zero Built Complexity lines. It published the public revision map at 23:24:39.2145529 UTC. The saved map has 4,119 unique mappings (185,368 bytes; SHA-256 b4101ac060d30fbde5fa84a9644bc613edc5bb8d30573580a16a94299f9e7ce0); all 102 new artifact references relative to the previously verified c81edae6 map returned HTTP 200. One completed job log and one revision map were retrieved; no artifact bodies were downloaded, and no workflow was rerun or restarted. #1807 is completed; the broader #321 objective remains open.