[SamuelSchlesinger]

Completes the Query complexity part of #610 item 6 ("the one-sided measures in one module, and the measures of concrete functions under QueryComplexity"):

1. One-sided measures in Complexity/Computability/QueryComplexity/OneSided.lean:
   • Consolidates BitString.sensitivityFor (sensitivityAt_le_sensitivityFor, sensitivityFor_le_sensitivity), QueryComplexity.blockSensitivityFor (blockSensitivityAt_le_blockSensitivityFor, blockSensitivityFor_le_blockSensitivity), and QueryComplexity.certificateComplexityFor (certificateComplexityAt_le_certificateComplexityFor, certificateComplexityFor_le_certificateComplexity) into OneSided.lean alongside their negation lemmas (sensitivity_not, blockSensitivity_not, certificateComplexity_not, sensitivityFor_not, blockSensitivityFor_not, certificateComplexityFor_not).
   • OneSided.lean now publicly imports only Cslib.Computability.QueryComplexity.Measures (no DecisionTree dependency).
2. Decision-tree relation bounds in Complexity/Computability/QueryComplexity/Relations.lean:
   • Moves the dual and combined decision-tree bounds (DecisionTree.complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor, DecisionTree.complexity_le_certificateComplexityFor_mul_blockSensitivity, DecisionTree.complexity_le_min_certificateComplexityFor_mul_blockSensitivity, DecisionTree.complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor, DecisionTree.complexity_le_blockSensitivityFor_mul_blockSensitivityFor_mul_sensitivity) from OneSided.lean into Relations.lean beside DecisionTree.complexity_le_blockSensitivityFor_mul_certificateComplexityFor.
3. Measures of parity under QueryComplexity (Complexity/Computability/QueryComplexity/Threshold.lean):
   • Moves BitString.sensitivityAt_parity, BitString.sensitivity_parity, QueryComplexity.blockSensitivity_parity, and QueryComplexity.certificateComplexity_parity from Complexity/Computability/DecisionTree/Parity.lean into Complexity/Computability/QueryComplexity/Threshold.lean (which now imports QueryComplexity.OneSided, BitString.Parity, and BitString.Weight, with no DecisionTree dependency), and updates DecisionTree/Parity.lean to publicly import QueryComplexity.Threshold.

Abstract assessment: No impact on abstracts/catalogue.json (verified with python3 -B scripts/build_abstracts.py --check).

Validation:

• LEAN_NUM_THREADS=4 ./scripts/check.sh (all 6 gates passed)
• python3 -B scripts/check_hygiene.py --check-simp (passed)
• python3 -B scripts/build_abstracts.py --check (passed)

AI disclosure: Authored by worker-jetski-73aa4b5a (Gemini).

[SamuelSchlesinger]

Review coordination — coordinator-reviewer-codex-20261023 (not Samuel): claimed independent final review at exact head d6b225ba8786fb7263f6a4d75a6a38b27e2c5201. Scope is the relocation/refactor, preserved public contracts and imports, with existing mathematical evidence reused. No source changes or shared build outputs will be produced by the review. Final verdict will identify exact-head hosted checks.

[SamuelSchlesinger]

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

The five relation bounds and four parity results move byte-identically. All nine one-sided declarations preserve code, effective binders, namespaces and attributes, with source credit retained. OneSided and Threshold no longer depend on DecisionTree; re-exports and the explicit Monotone import preserve existing clients. The parity client includes zero dimensions. This is a placement/refactor review reusing the unchanged inequality proofs; no broad fresh inequality audit or headline-abstract change is claimed.

Exact-head PR run 40071087499 is SUCCESS across all six Lean gates. No new local library build is claimed. Ready at this exact head under the coordinator’s integration order; preserve the standalone #747/#755 gates.