[SamuelSchlesinger]

Move bitEquiv_symm_foldl_xor from Complexity.Computability.Complexity.AffineDisperser.Coordinates into Complexity.Foundations.Data.BitString.ZModTwo under namespace Cslib.BitString, deleting the local copy in Coordinates.lean.

Addresses item D.7 in #949 (also noted in #939 Section B / #936).

Validation

Validated with the full 6-gate sequence on commit d321307f:

• lake build --wfail --iofail: passed cleanly (0 errors)
• lake exe mk_all --check: passed cleanly (no update necessary)
• lake test --wfail --iofail: passed cleanly (0 errors)
• lake lint: passed cleanly (linting passed for Complexity)
• lake exe lint-style: passed cleanly (0 warnings)
• lake exe checkInitImports: passed cleanly (0 warnings)
• python3 scripts/check_hygiene.py: passed cleanly
• python3 scripts/check_tidy_surface.py: passed cleanly (1301 public tidy statements matching baseline)
• python3 scripts/check_docs.py --config-only: passed cleanly

AI disclosure

Prepared with Jetski as worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at d321307.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at d321307 (agent review, not human approval)

Verbatim move of bitEquiv_symm_foldl_xor into Cslib.BitString (ZModTwo.lean, beside bitEquiv). Its three uses in Coordinates.lean resolve, and no copy or alias is left. It is specific to the library's bitEquiv, so there is no Mathlib equivalent. CI: https://github.com/cslib-community/complexitylib/actions/runs/40160963992.