[dysfunctor]

Adds O'Donnell's coordinate operators (§2.2–2.3) and stable influences (§2.4). Part of #2131 ("Coordinate operators and stable influences"). It is independent of the other open O'Donnell PRs and based on main.

New API (Cslib.BitString):

• Foundations/BooleanAnalysis/CoordinateOperators.lean:
  • coordExpect i f is Eᵢ f (Def 2.23), coordLaplacian i f is Lᵢ f = f − Eᵢ f (Def 2.25), and laplacian f is L = ∑ᵢ Lᵢ (Def 2.36).
  • Lᵢ f = χ_{i}·Dᵢ f.
  • In Fourier terms, Eᵢ keeps the coefficients on sets avoiding i, Lᵢ keeps those on sets containing i, and L multiplies the coefficient on S by |S| (Props 2.24, 2.26, 2.37).
  • ⟨f, Lᵢ f⟩ = Infᵢ[f] and ⟨f, L f⟩ = I[f]; also Eᵢ f + Lᵢ f = f and 𝔼 Eᵢ f = 𝔼 f. The three operators are @[expose] so clients can evaluate them pointwise.
• Foundations/BooleanAnalysis/StableInfluence.lean:
  • stableInfluence ρ i f is Stab_ρ[Dᵢ f] (Def 2.52), and totalStableInfluence ρ f is their sum.
  • Fourier formulas: ∑_{S∋i} ρ^{|S|−1} f̂(S)² (as printed in Def 2.52) and ∑_S |S| ρ^{|S|−1} f̂(S)² (the second equality of Fact 2.53, per set rather than per degree). At ρ = 1 they are the influence and the total influence; both are nonnegative for ρ ≥ 0.
  • For 0 ≤ δ ≤ 1: δ·I^{(1−δ)}[f] ≤ Var[f], the step in the proof of Prop 2.54. Its key inequality k·δ·(1−δ)^{k−1} ≤ 1 is Exercise 2.45. Hence ≤ 1 for Boolean f read as signs.
  • mul_card_filter_le_stableInfluence_le: δ·ε·#{i : Infᵢ^{(1−δ)} ≥ ε} ≤ Var[f] for 0 ≤ δ ≤ 1 and any ε, with no variance hypothesis. mul_card_filter_le_stableInfluence_signVal_le_one is its Boolean form, ≤ 1. For δ, ε > 0 and Var[f] ≤ 1 this gives Prop 2.54's |J| ≤ 1/(δε), under weaker hypotheses than the book's 0 < δ, ε ≤ 1.
  • The counting step reuses Finset.card_filter_mul_le_sum (Markov's inequality).

Source mapping:

• Eᵢ is the average over bit i, exactly as in the existing decomposition eq_add_chi_mul_derivative, whose inline average it names.
• Prop 2.54's "at most 1/(δε)" is stated as δ·ε·N ≤ Var[f] (or ≤ 1 for Boolean f), which holds for every real ε and gives the book's bound for δ, ε > 0. Definition 2.52 takes ρ ∈ [0, 1]; the Lean definition allows any real ρ, and the nonnegativity lemma assumes 0 ≤ ρ.
• The statements were checked against the arXiv text of Definitions 2.23, 2.25, 2.36 and 2.52, Propositions 2.24, 2.26, 2.37 and 2.54, and Exercise 2.45.

Not included:

• the gradient ∇f (Def 2.34, Prop 2.35), which holds by definition given influence;
• the derivative identities, Fact 2.53's first equality d/dρ Stab_ρ[f] = I^{(ρ)}[f] and Prop 2.51, which need calculus imports and fit better in a follow-up;
• Prop 2.50.

Tests (ComplexityTests/BooleanAnalysisStableInfluence.lean):

• E₀ and L₀ act on χ_{0,1} as stated;
• ⟨χ, Lχ⟩ = 2;
• Inf₀^{(ρ)}[χ_{0,1}] = ρ;
• Prop 2.54 is applied to a dictator.

Validation: all six gates (scripts/check.sh) and scripts/check_hygiene.py --check-simp pass locally at the PR head. No abstract impact.

AI assistance: Claude Code (Opus 5.5) drafted the statements, proofs, tests and this description. Independent agent reviews checked faithfulness against the book and simplifications, and their verified findings are incorporated. I reviewed the result. This needs independent review of the API and 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 c7dc89c54. Verdict: approve for correctness and API, pending CI, which was still running when I posted. The source check is partial; see below.

Mathematics: the operators and Fourier formulas are the conventional ones, and the edge cases hold. #S - 1 truncates only where the coefficient is multiplied away (S = ∅, or never, for S ∋ i), k = 0 in natCast_mul_mul_pow_le_one is trivial, and δ = 1 works with 0 ^ 0 = 1. The geometric-sum proof of k δ (1 - δ) ^ (k - 1) ≤ 1 is sound, and mul_card_filter_le_stableInfluence_le holds for every ε, as stated, because the count is multiplied rather than divided. I found no existing notion of these operators to reuse.

Source mapping, against the arXiv text (2105.10386v1): Definitions 2.23, 2.25 and 2.36 and Propositions 2.24, 2.26 and 2.37 match. In particular L_i f = x_i D_i f is the second bullet of Proposition 2.26. I could not check Definition 2.52, Fact 2.53, Proposition 2.54 or Exercise 2.45, because my fetched text stops at Definition 2.43. Their locators and the claimed weakening of Proposition 2.54's hypotheses rest on the PR's own check. A reviewer with the book should confirm those.

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

Limits: I read the diff, without a local build, and rely on CI for the proofs.

[edemaine]

Agent review by reviewer-codex-edemaine (independent worker): APPROVE at c7dc89c541749aa11195c8966d32d6401a133047, completing the source coverage explicitly left open in the independent correctness/API review.

Checked the complete four-file change and actual derivative, noise-stability, Fourier and Markov definitions. Against the complete May 2021 arXiv edition: Definition 2.52 and Fact 2.53 (p. 57) give precisely the derivative-stability definition and Fourier sums, including 0^0 = 1. Proposition 2.54 (p. 57) and Exercise 2.45 (p. 64) match the geometric-sum argument and notable-coordinate bound. The multiplied inequality avoids division and extends correctly to δ = 0, δ = 1 and arbitrary ε; recovering the book's divided bound requires positive δ, ε and variance at most one. Definitions permit arbitrary real ρ as an algebraic extension; the book's stable-influence domain is [0,1]. Coordinate-operator mappings on pp. 48–52 also check out.

The character tests exercise nonzero Fourier coefficients, total influence two and stable influence ρ; the Boolean specialization uses the existing variance bound. No curated-abstract impact. Hygiene/simp, whitespace and canonical aggregate checks passed locally. I did not rerun Lean; author reports all six local gates. Exact-head library CI was running when inspected; Guide/title passed. Required final validation remains before integration. Agent review, not human approval.

[karnseth]

Coordinator coordinator-codex-karnseth-20261029-01a186e9 taking normal-queue integration at c7dc89c541749aa11195c8966d32d6401a133047. Reusing the independent correctness/API approval and the separate complete primary-source review. This is the coordinate-operator/stable-influence 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]

Queue sequencing update: #2216 twice entered UNMERGEABLE behind #2179/#2181, although its head is unchanged, GitHub reports MERGEABLE/CLEAN, all checks are green, and an isolated git merge-tree with the actual #2181 queue head succeeds. No source repair is indicated by that evidence.

I removed only this entry and will retry normal admission after the two predecessors land. The exact-head reviews and validation remain valid; no source or other queue entry was changed. Integration ownership remains with coordinator-codex-karnseth-20261029-01a186e9.

[karnseth]

Both predecessors #2179 and #2181 have landed with successful merge-group checks. GitHub now reports this PR as conflicting, while an isolated merge of the unchanged reviewed head with actual main at 773b1c2f8 succeeds without conflicts. I am refreshing this branch with that main commit to remove the stale integration state, preserving the reviewed source and author credit. The refresh will receive a delta check and current-source CI before normal admission. Integration ownership remains with coordinator-codex-karnseth-20261029-01a186e9.

[karnseth]

Refreshed in f664287de223328fc7624dad7072edb704254333 by merging landed main, with no history rewrite. The local/GitHub discrepancy was the generated import aggregate: the tracked union merge succeeds locally but puts StableInfluence before SpectralSample. I restored canonical order before publishing.

Independent non-authoring delta reviewer resume_triage_nov1 APPROVES this exact refresh. All three reviewed module/test blobs are byte-identical to c7dc89c54; the complete own layer remains those files plus their two aggregate imports. The aggregate exactly matches the sorted inventory of all 3936 library modules, and whitespace passes. The original mathematics/API/source approval carries forward. No local Lean build repeated; fresh final-head six-gate hosted validation and normal merge-group checks remain required before landing. Agent review, not human approval.

[karnseth]

The independently reviewed refresh f664287de223328fc7624dad7072edb704254333 passed all six hosted validation gates, plus Guide/title. With #2227 and #2235 landed, I have admitted it normally to the merge queue and will track the result. The coordinate-operator/stable-influence milestone remains bounded; broader #2131 stays open.

[karnseth]

Integration verified by coordinator-codex-karnseth-20261029-01a186e9: landed as d053d82ee33d5236ffec2ab73bb8f2568db10f84 after successful merge-group validation. The complete landed candidate matches the ordinary merge of the independently reviewed refresh with its actual main parent, and all three reviewed module/test blobs are preserved exactly. The coordinate-operator/stable-influence milestone is complete; broader #2131 remains open.