Repository navigation
feat(arithmetic): eliminate one Boolean selector from a permanent #1831
Description
Prove a concrete elimination rule for a Boolean selector occurring in one entry of a generic permanent. Under an explicit half : K with (2 : K) * half = 1, the sum of the selector-0 and selector-1 permanents equals twice the permanent with that entry set to half. Convert this to the existing plain IsProjection with dimension growth from n to n+1, using a constant-2 diagonal block.
This is a bounded prerequisite for the planned two-entry Boolean-sum gadget toward ROADMAP landmark 6. The dimension-n+3 diagonal-pair gadget, general repeated-selector elimination, VP-witness-to-formula conversion and full VNP-hardness remain open. It does not narrow or complete deferred #321. The hypothesis is essential to this construction and is jointly satisfiable over ℚ and ZMod 3; it fails in characteristic two. Existing VNP-membership and formula-simulation statements retain their more general ring/semiring scopes.
Source: Orzel–Srinivasan–Tavenas–Yehudayoff, The Algebraic Cost of a Boolean Sum, FSTTCS 2025, §3.3 Claim 13, p. 47:10. The source allows a nonzero scalar multiplier in projections and therefore states zero extra dimension; Lean's plain substitution-only IsProjection uses one extra scalar block. This resource-convention difference will be explicit. The source's two-entry Claim 8 has a separate verified index typo ({x11,x12} in its statement versus the diagonal pair in its proof); this issue does not claim that two-entry result.
Acceptance: a reusable matrix identity, an elimination theorem using the existing booleanSum/projection/IsProjection, exact n+1 dimension accounting, concrete rational and odd-characteristic instances plus the characteristic-two obstruction, all six validation gates, aggregate regeneration, no-impact abstract assessment, and outside-author-fleet exact-head review.
Worker/session worker-codex-circuits-20261030; branch feat/permanent-single-selector-20261030 planned from reviewed #1813 at the NEW_READY network-backed circuits lane. Fresh issue/PR search found no duplicate owner. This branch will depend on #1813's permanent projection operations and leave both existing approved PR heads unchanged.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
Status: active. Worker/session
worker-codex-circuits-20261030claims the single-entry selector-elimination milestone onfeat/permanent-single-selector-20261030, in the NEW_READY network-backed circuits lane. The explicit half-of-two hypothesis and the one-extra-dimension cost under plain projections are part of the scope. The two-entry gadget and full VNP-hardness remain open; existing reviewed PR heads stay unchanged.SamuelSchlesinger commentedon Oct 30, 2026
Concrete API follow-up: the new client reuses
IsProjection.permanent_mulfromArithmetic/Permanent/Formula, exposing a placement improvement. Move that rule andisProjection_permanent_mono, with their matrix-specialization plumbing, intoArithmetic/Permanent/Projectionshared by the formula and Boolean-sum clients. Keep rooted construction invariants private and preserve the public statements. This follow-up is separate from the current single-entry elimination criterion and from full VNP-hardness.SamuelSchlesinger commentedon Oct 30, 2026
Status: awaiting review. Worker/session
worker-codex-circuits-20261030submitted #1839 as the narrow child of #1813. All six local validation gates and concrete clients pass; source mapping, explicit algebraic/resource assumptions and abstract assessment are recorded in the PR. Outside-author-fleet review was requested. The two-entry gadget, general selector elimination and full VNP-hardness remain open.SamuelSchlesinger commentedon Oct 31, 2026
Milestone completed: #1839 has landed with the reusable matrix identity, explicit-half single-entry elimination and exact
d + 1plain-projection accounting. Concrete positive/characteristic-two clients, validation and reused independent review are linked in the single PR record.The two-entry gadget, repeated-selector elimination, VP-witness-to-formula conversion, uniform construction runtime and full VNP-hardness remain unproved. The existing deferred/not-planned disposition of the broader #321 objective is preserved.