[SamuelSchlesinger]

Replace the current D(f) ≤ 8·deg(f)^6 and D(f) ≤ 4·s(f)^9 endpoints with D(f) ≤ 2·deg(f)^3 and D(f) ≤ 2·s(f)^6. The main new theorem is Cslib.DecisionTree.complexity_le_degree_mul_blockSensitivity, proving D(f) ≤ deg(f)·bs(f) for every total Boolean function, including constants and arity zero.

The proof queries a maximum Fourier support, shows that every parallel face contains a sensitive block, and uses the existing native decision-tree composition theorem to induct on block sensitivity. The maximal-support facts live in a reusable foundations module. The restriction lemma is generalized from the existing certificate proof, which remains a client. Superseded endpoint names and all callers are migrated; no compatibility aliases or parallel complexity model are added.

Verified source: Midrijanis, arXiv:quant-ph/0403168v2, Theorem 4, p. 3, states (mathematical typesetting normalized):

For every total Boolean function f holds D(f) ≤ 2deg(f)^3.

Its proof on p. 4 states:

hence D(f) ≤ deg(f) ∗ bs(f).

The paper's total f:{0,1}^N→{0,1} maps to BooleanFunction n; D is minimum worst-case decision-tree depth, deg is the existing exact real multilinear degree with its Fourier characterization, and bs counts pairwise disjoint sensitive blocks. The positive-degree witness corresponds to Lemma 3; the final endpoints handle constants separately. No quantum-query theorem is claimed. The bibliography entry pins version 2 and is in a separate focused commit.

Concrete clients check a sensitive pair where no singleton is sensitive, an irrelevant input coordinate, constants at arbitrary arity, and a conjunction on 100 inputs whose new degree bound is 16 rather than the former 512. All seven affected library modules and all five relevant query-complexity test modules elaborate locally without warnings; source/simp hygiene, bibliography order, aggregate source comparison and whitespace checks pass. Full Lean CI passed for commit 45ed11ede14f, including build, tests, lint, aggregate-import generation, style and Init-import checks. Internal worker cross-checks found no mathematical blocker; independent coordinator review is required before merge. The selected abstract catalogue is unaffected.

Closes #1163.

AI assistance: ChatGPT implemented and self-reviewed this change with parallel workers; the internal checks are not independent coordinator or human review.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-82 (agent review) at 45ed11e.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-82 — APPROVED at 45ed11e

Agent review, not human approval.

1. Source. I fetched arXiv quant-ph/0403168v2, stamped 27 Mar 2004. Both quotations in the PR body appear in it verbatim, apart from the declared normalization of superscripts and spacing. "For every total Boolean function f holds D(f) ≤ 2deg(f)^3." is Theorem 4 on p. 3. "hence D(f) ≤ deg(f) ∗ bs(f)." is in its proof on p. 4. The Lemma 3 locator (p. 3) and the Midrijanis2004 bib entry (version 2) also check out.
2. Mapping. complexity_le_degree_mul_blockSensitivity holds for every f : BooleanFunction n with no hypotheses, matching the paper's total f : {0,1}^N → {0,1}. It uses decision-tree depth, the existing real multilinear degree and disjoint-block bs. Maxonomials of the 0/1 representation are exactly the maximum-cardinality Fourier supports, so the Fourier phrasing is faithful.
   • The Lean "Lemma 3" form is existential (some support of size deg f), while the paper says "every maxonomial". The docstrings say "property of", and the existential form is all the proof needs. exists_ne_on_face_of_fourierCoeff_maximal in fact covers every inclusion-maximal support.
3. Proof structure. The proof uses a uniform induction (bs(f|_a) ≤ bs(f) − 1 for every answer a) instead of the paper's per-input chain. I checked the key step. Sensitive blocks of the restriction, minus S, together with a block B₀ ⊆ S that is sensitive at the filled input, form a sensitive family of f. The degree does not grow under restriction, and the deg = 0 and bs = 0 bases are handled.
4. Strengthening. D ≤ 2 deg³ implies the removed D ≤ 8 deg⁶, and D ≤ 2 s⁶ (Midrijanis together with Huang's theorem, attributed as such) implies the removed D ≤ 4 s⁹. Each is trivial when the measure is 0. The removal without aliases follows the AGENTS rule, and no stale references remain in the library, tests, abstracts or ROADMAP. No quantum claim is made.
5. API. There are no new definitions. The cube-level Fourier facts live in Cslib.BitString (Foundations/BooleanAnalysis/MaximalSupport.lean), per placement rule 6. The generalized blockSensitivityAt_comp_piecewise_add_one_le becomes public; it is a named bound, which fits doc(contributing): privatize by intent, not by current usage #926. The certificate specialization stays a private client.
6. Tests. They exercise the cases that matter:
   • a sensitive pair with no sensitive singleton, so the lemma must produce blocks;
   • D ≤ 4 from the exact deg = bs = 2;
   • AND on 100 inputs, with D ≤ 16 against the former 512;
   • constants at every arity, including n = 0.
7. CI and disclosure. Hosted CI passed at this head (run 40294196720). The head merges cleanly into current main (731c6e9c). AI disclosure and the handoff (Prove Midrijanis's decision-tree bound and sharpen its degree and sensitivity corollaries #1163) are present. The bibliography is in its own commit.

Nonblocking nits:

• a. exists_ne_zero_on_face_of_fourierCoeff_maximal puts f, its hypotheses and x after the colon to serve the induction motive. Using induction S using Finset.induction_on generalizing f would give ordinary binders, matching its sibling theorem.
• b. As a possible follow-up, the inline proof that degree (fun y => f (S.piecewise a y)) ≤ degree f could become a named lemma in QueryComplexity/Degree.lean next to degree_comp_not.