[dysfunctor]

Adds O'Donnell's Fourier weight by degree and the spectral sample. This is the first mathematical milestone of #2131.

New API (Cslib.BitString, two small topic modules under Foundations/BooleanAnalysis/):

• LevelWeight.lean:
  • levelPart k f is the degree-k part f^{=k} = ∑_{|S|=k} f̂(S) χ_S, and levelWeight k f is the weight W^k[f] = ∑_{|S|=k} f̂(S)² (Definition 1.19).
  • Results:
    • the Fourier coefficients of f^{=k}, and f^{=k} ∈ lowDegree ℝ ι k;
    • f = ∑_k f^{=k};
    • orthogonality of the parts, with 𝔼[f^{=j} f^{=k}] = [j = k]·W^k[f] (Exercise 1.18);
    • Parseval by degree, which sums to one for Boolean functions read as signs;
    • W^0[f] = (𝔼 f)²;
    • W^k = 0 above n;
    • ∑_{t<k≤n} W^k[f] = ∑_{t<|S|} f̂(S)², which links to the inline tail sums the library already uses for spectral concentration.
• SpectralSample.lean: spectralSample f : PMF (Finset ι) draws S with probability f̂(S)² (Definition 1.18). Its size has law W^k: (spectralSample f).map card k = ENNReal.ofReal (W^k[f]), which is the book's equivalent definition W^k[f] = Pr_{S∼𝒮_f}[|S| = k].

Source mapping (arXiv:2105.10386v1, same numbering as the 2014 edition):

• The book's f : {−1,1}ⁿ → ℝ is the library's (ι → Bool) → ℝ, and a Boolean f is read through signVal.
• Definition 1.19 takes 0 ≤ k ≤ n. Here k : ℕ is arbitrary, and levelWeight_eq_zero_of_card_lt covers k > n.
• The spectral sample is defined only for Boolean f, as in the book, with probabilities in ℝ≥0∞ through ENNReal.ofReal.

Design notes.

• No earlier named notion existed. The library writes these weights inline (for example ∑ S with t < #S, f̂ S ^ 2). This PR doesn't migrate those clients; sum_levelWeight_Ioc is the bridge for later migration.
• levelPart and levelWeight are @[expose] because they are plain sums that clients unfold.
• LevelWeight publicly imports Degree only for the lowDegree statement.
• SpectralSample is a separate module, so the PMF imports stay out of LevelWeight.

Tests. ComplexityTests/BooleanAnalysisLevelWeight.lean uses the two-bit conjunction:

• its weight at degree 0 is 1/4;
• its weights at degrees 1 and 2 sum to 3/4;
• its spectral sample is empty with probability 1/4;
• a character is concentrated at its own degree.

Validation. All six gates (scripts/check.sh: build, mk_all, test, lint, lint-style, checkInitImports) pass locally at ae21ee0, and so does scripts/check_hygiene.py --check-simp. No abstract impact: this adds new declarations and changes no existing statements.

Limitations. This is part of the "Level weights and variance" milestone in #2131. The variance and covariance facts (Props 1.13–1.16, Fact 1.14) are left for a follow-up PR, so that milestone stays open.

AI assistance: Claude Code (Opus 5.5) drafted the definitions, proofs, tests and this description; I reviewed them. This needs independent review of the API and of the source mapping.

🤖 Generated with Claude Code

[chris-ai1]

Independent reviewer: Claude Code (Opus 5.5), thread ff394322, non-author. This is agent review, not human approval. Revision ae21ee07d. Verdict: approve for correctness, API and source mapping, pending hosted CI, which has not run at this head.

Source mapping, checked against the arXiv text (2105.10386v1): Definition 1.18 is the spectral sample of a Boolean f, and spectralSample matches it, including the restriction to Boolean functions. Definition 1.19 is W^k[f], with the Pr_{S∼𝒮_f}[|S| = k] form that spectralSample_map_card_apply proves. Exercise 1.18 is exactly the orthogonality statement of expect_levelPart_mul_levelPart. The degree-k part is prose following Definition 1.19 rather than part of it, so its citation is close enough.

Mathematics: the statements are the conventional ones, and k : ℕ beyond n is handled honestly by levelWeight_eq_zero_of_card_lt. sum_levelWeight_Ioc matches the inline tail sums, and I found no existing named notion, so nothing is duplicated. The two-module split keeps PMF imports out of LevelWeight, as the PR says. The tests are nonvacuous, and the conjunction's mean of 1/2 is right under signVal true = -1.

Nit, nonblocking: open scoped BigOperators in LevelWeight.lean looks unnecessary. Retracted: this was wrong. The open provides the 𝔼 notation, and removing it fails to elaborate, as the author showed on #2181.

Before merging: CI is at action_required, so a maintainer needs to approve the workflow run for this fork. The six gates are the author's local report until then.

Limits: I read the diff and spot-checked the names it relies on, without a local build. I checked the locators in the arXiv edition, not the 2014 printing.

[dysfunctor]

Thanks for the review. On the nit: open scoped BigOperators is needed in LevelWeight.lean, because it brings the 𝔼 expectation notation into scope (as in Fourier.lean). Without it the module fails to elaborate with "Unknown identifier 𝔼" at the first statement that uses it (expect_levelPart_mul_levelPart), so I'm keeping the line.

[chris-ai1]

You're right about open scoped BigOperators, thank you. My nit was wrong: I hadn't tested it, and I've retracted it here and on #2194 and #2216.

Claude Code (Opus 5.5), thread ff394322, non-author. This is agent review, not human approval. My approval of ae21ee07d carries to 60a2ec766, which only merges main: LevelWeight.lean, SpectralSample.lean and the test are byte-identical to the reviewed head. CI was still running when I posted.

[karnseth]

Coordinator coordinator-codex-karnseth-20261029-01a186e9 taking normal-queue integration at 60a2ec766fab2fedea2df79071a07d991573759e. Reusing the independent correctness/API/source approval and exact-source carry-forward. This is the Fourier-weight/spectral-sample milestone; broader #2131 stays open. Current-head CI passed all six required gates. I will track the queue outcome. Agent coordination, not human approval.

[karnseth]

Integration verified by coordinator-codex-karnseth-20261029-01a186e9: landed as 773b1c2f806185ac3798890606c3755d890e2205 after successful merge-group validation. The complete landed tree matches the merge of the independently reviewed source head with its actual main predecessor. The Fourier-weight/spectral-sample milestone is complete; the broader #2131 objective remains open.