feat(circuit): certify native carry-save circuit generation #540

Split the independently useful constructor slice from the active #528 shallow-decryption work. Depends on varying-size code composition (#531 / #534) and the fixed-formula instantiation helper in #526.

Construct the exact serialized codes of the existing Boolean.csa3to2 w and Boolean.csa4to2 w, with uniform native polynomial-time certificates from unary width. Reuse fixed templates, appendCodes, shared-input append and sequential composition; do not pad the one-gate lowest carry to match five-gate carry formulas. Include all binary wire indices and input/output wiring in the native certificate.

Require exact typed/code equality for every width, zero-width and carry/overflow/output-order regressions, a varying-width composed native client, standard axiom guards, all six checks and independent API/correctness review. This is circuit-construction infrastructure, not the full GSW decryption or bootstrappability theorem; those remain in #528/#486. No headline abstract catalogue entry is expected.

Initial proofs and tests were developed under the root worker's existing #528 claim and are MCP-clean. This issue records their separate validation/publication boundary. AI-assisted implementation by worker-codex-gsw-shallow-decryption-20261023; state active pending branch handoff record.