feat(arithmetic): prove permanent VNP membership via Ryser witnesses #1799

Prove that the existing generic permanent family belongs to the existing nonuniform VNP over every commutative ring, using a concrete Ryser Boolean-sum witness. This is a bounded prerequisite for ROADMAP landmark 6 (Valiant's VNP-completeness of the permanent); it does not prove VNP-hardness, Valiant's counting completeness, or Kabanets–Impagliazzo (#891). The earlier broad #321 was deferred, with saved source at 5b8acca7; reuse its valid Ryser argument with original source credit, while replacing its standalone circuit combinators with the current synthesis API.

Acceptance criteria: a reusable Boolean-indicator Ryser identity in the matrix foundations; an explicit witness polynomial in n²+n variables with degree ≤ 3n and polynomial gate bound; permFamily_mem_VNP for the existing permFamily/VNP; checked zero-dimension, nontrivial integer matrix and characteristic-two instances; full six-gate validation, aggregate regeneration, abstract assessment, and independent exact-revision correctness/API review outside the author fleet.

Source mapping: Uwe Schauz, Colorings and orientations of matrices and graphs, EJC 13 (2006), #R61, Theorem 1.2, p. 3, published PDF. Its Boolean-vector Ryser formula uses d ∈ {0,1}^V, sign (-1)^{|d⁻¹(0)|} and product of row sums Π(Ad). Lean uses e : ι → Bool, product of if e j then 1 else -1, and row sums selected by e. The new proof works algebraically over CommRing, strengthening that paper's section-wide integral-domain/characteristic-zero convention. The VNP witness is (∏j (2Yj−1)) * ∏i (∑j Yj Xij); Boolean substitution is the existing booleanSum. No certified uniform construction runtime is claimed.

Worker/session: worker-codex-circuits-20261030, delegated by the ten-lane roadmap coordinator. Branch planned: feat/permanent-vnp-20261030; isolated Extra-drive lane will be linked in the claim when provisioned. No active owner or open PR covers this bounded milestone.