feat(arithmetic): project arithmetic formulas to the permanent #1807

Prove that every formula F : Formula (arithSignature K) n is a projection of the (F.size+1) × (F.size+1) generic permanent, over every commutative semiring. Reuse the existing Formula, formal-polynomial evaluation, IsProjection, and genericMatrix; rooted gadget representations remain private proof invariants. Add the reusable matrix reindexing/block identities in a small foundational module, retaining the Mathlib determinant proof's source credit where adapted.

This is the formula-simulation prerequisite for ROADMAP landmark 6. It does not prove Valiant's full VNP-hardness reduction, elimination of Boolean sums, or certified construction runtime. Deferred #321 preserves the broader objective; #1799/#1802 independently supplies VNP membership.

Acceptance criteria: the formula projection theorem and its existing toCircuit specialization, a checked explicit dimension bound with constants counted by Formula.size, useful permanent block/reindex lemmas, nontrivial addition/product/repeated-input/constant examples over ℕ and characteristic two, full six-gate validation, aggregate regeneration, abstract assessment, and independent exact-head API/correctness review outside the author fleet.

Source plan: Orzel–Srinivasan–Tavenas–Yehudayoff, The Algebraic Cost of a Boolean Sum, FSTTCS 2025, published version, Lemma 4 and Definition 1, states formula simulation by the permanent. Lean's explicit size+1 bound and semiring generality are quantitative/model strengthenings proved directly, rather than verbatim source claims. Source-to-Lean mapping will distinguish the paper's characteristic-not-two field convention and its scalar-permitting projections from Lean's stronger plain substitution projection. Valid saved proof material at 5b8acca7 will retain credit.

Worker/session worker-codex-circuits-20261030; planned branch feat/permanent-formulas-20261030 in the READY Extra circuits lane. Fresh issue/PR search found no duplicate active owner.