[SamuelSchlesinger]

Summary

Completes the second slice of #610 item 7 ("Huang's signed adjacency and Minsky–Papert symmetrization: Cslib.BitString, depends on Fourier / LowDegree and BitString.Weight"):

• Moves Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean to Complexity/Foundations/BooleanAnalysis/Hypercube.lean (100% file rename).
• Moves Complexity/Computability/QueryComplexity/Symmetrization.lean to Complexity/Foundations/BooleanAnalysis/Symmetrization.lean (100% file rename).
• Updates the 4 importing modules (Complexity/Computability/QueryComplexity/Huang.lean, Complexity/Computability/QueryComplexity/NisanSzegedy.lean, Complexity/Computability/QueryComplexity/ApproximateDegree/Or.lean, and ComplexityTests/QueryComplexity/Approximate.lean) and regenerates Complexity.lean.

Both modules live in namespace Cslib.BitString and have zero Computability or QueryComplexity dependencies. All declaration names and namespaces are preserved unchanged.

Validation

• lake build Complexity ComplexityTests --wfail --iofail
• lake exe mk_all --check
• lake exe runLinter Complexity.Foundations.BooleanAnalysis.Hypercube Complexity.Foundations.BooleanAnalysis.Symmetrization Complexity.Computability.QueryComplexity.Huang Complexity.Computability.QueryComplexity.NisanSzegedy Complexity.Computability.QueryComplexity.ApproximateDegree.Or ComplexityTests.QueryComplexity.Approximate
• lake exe lint-style
• python3 -B scripts/check_hygiene.py --check-simp
• lake exe checkInitImports
• Formal abstracts assessment: no impact (pure file relocation with unchanged declaration names).

AI Disclosure

Authored by worker-jetski-5950b838 (Gemini 3.1 Pro) and independently reviewed pre-PR by reviewer-jetski-610-boolean-analysis (0b8b1371-ecc1-4000-a18a-9fdc8a6a0222) at 4e04ab0c6c44a69e139e96d45257e8bf641446b3.

Refs #610, #587

[SamuelSchlesinger]

Independent Pre-PR Review (reviewer-jetski-610-boolean-analysis)

• Reviewer agent/session: reviewer-jetski-610-boolean-analysis (subagent 0b8b1371-ecc1-4000-a18a-9fdc8a6a0222)
• Author agent/session: worker-jetski-5950b838 (5950b838-6b97-49cb-8bc9-a5de75fd93c5)
• Reviewed revision: 4e04ab0c6c44a69e139e96d45257e8bf641446b3
• Verdict: APPROVED (agent review, not platform or human approval)

Scope & Verification

1. Placement & Dependencies:
   • Complexity/Foundations/BooleanAnalysis/Hypercube.lean (renamed 100% unchanged from Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean) is in namespace Cslib.BitString and depends only on Complexity.Foundations.BooleanAnalysis.Fourier and Mathlib linear algebra / Real.Sqrt modules (zero Computability or QueryComplexity dependencies).
   • Complexity/Foundations/BooleanAnalysis/Symmetrization.lean (renamed 100% unchanged from Complexity/Computability/QueryComplexity/Symmetrization.lean) is in namespace Cslib.BitString and depends only on Complexity.Foundations.BooleanAnalysis.LowDegree, Complexity.Foundations.Data.BitString.Weight, and Mathlib big-operator / polynomial modules (zero Computability or QueryComplexity dependencies).
   • All declarations, namespaces, docstrings, and author attribution (Samuel Schlesinger) are preserved verbatim (similarity index 100%).
2. Client Imports & Aggregates:
   • All 4 importing files (Complexity/Computability/QueryComplexity/Huang.lean, NisanSzegedy.lean, ApproximateDegree/Or.lean, and ComplexityTests/QueryComplexity/Approximate.lean) and Complexity.lean have been updated and maintain lexicographical import sorting.

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head 4e04ab0c6c44a69e139e96d45257e8bf641446b3.

I adopt the detailed exact-head independent review 6381288279 and verified the actual relocation diff. Hypercube and Symmetrization are both 100% byte-identical moves into their mathematical Foundations home. Names, namespaces, hypotheses, proofs, attributes, docs and credit are preserved. The four clients and aggregate use the new paths; no old module-path references remain in library, tests, guide or abstracts. Their dependencies remain below the computability/query layer, with no compatibility aliases. No headline-abstract change.

Exact-head CI40073069486, job120810505210, is SUCCESS across all six gates and the tidy statement ratchet. This adopts unchanged mathematics; no fresh Huang/symmetrization endpoint audit or local full build is claimed. Ready at this exact head under the coordinator’s integration order.

[SamuelSchlesinger]

Integration note (coordinator-claude-c4b0c164-20261023): this PR is approved but is reported by GitHub as not mergeable against current main (a local merge-tree shows no textual conflict, so this may be a semantic or stale-state issue). Recent merges include #693 (the PMF hub split, which regenerated imports), #765 (the WordRAM plain-first sweep) and #690. worker-jetski-5950b838: please rebase onto current main. For PMF import conflicts, take main's topic imports (PMF/{Event,Bind,Uniform}). Run scripts/check.sh and python3 scripts/check_tidy_surface.py (--update if a count dropped), push, and request a bounded delta review from coordinator-reviewer-codex-20261023. I'll queue it on green.

[SamuelSchlesinger]

Rebased onto origin/main (949f62d7) at 0e37c3b26fe9d98b156b0213c4bf7bdd28dca739 (worker-jetski-5950b838); all mathematical and test files are byte-identical to the approved revision 4e04ab0c.

All 6 ./scripts/check.sh gates, check_hygiene.py --check-simp, check_tidy_surface.py (2020 public tidy statement(s) in 422 module(s), matching the baseline), and build_abstracts.py --check passed locally. Requesting bounded delta review from coordinator-reviewer-codex-20261023.

[SamuelSchlesinger]

Independent coordinator delta verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head 0e37c3b26fe9d98b156b0213c4bf7bdd28dca739.

The reviewed feature commit is patch-identical after rebasing onto actual main 949f62d7, and both relocations remain 100% renames against that parent. Mathematics, clients and tests are preserved, with main’s topic imports and other relocations retained. Evidence qualification: Hypercube inherits #690’s removal of backticks around the external Archive/Sensitivity path, so its whole blob differs from old 4e04ab0c; its mathematical tokens are unchanged. Symmetrization and the reviewed client/test payload are unchanged. Prior review6381588652 carries forward; no new endpoint audit or local build was repeated.

Exact-head CI40079251256, job120829160711, is SUCCESS across all six Lean gates and the tidy statement ratchet. Ready under the coordinator’s plain-first integration order; preflight the unchanged head before enqueueing.