[SamuelSchlesinger]

Privatizes 24 declarations across 8 modules in Communication that are never referenced outside their defining modules, per the privatization sweep plan in #899 (Item 9).

This PR completes the Communication slice of Item 9, perfectly complementing #913 (which privatized the DecisionTree and QueryComplexity slices while explicitly excluding Communication).

Summary of changes

• Marked 24 unreferenced declarations private across 8 modules under Complexity/Computability/Communication/:
  • Discrepancy.lean: abs_sum_le_discrepancy, exists_abs_sum_eq_discrepancy
  • Disjointness.lean: mem_parts, compl_insert_eq_of_mem_parts, sum_parts, sum_parts_swap, card_parts_pos, hardWeight_nonneg, hardDist_apply_toReal
  • Distributional.lean: le_distributionalComplexity_iff, distributionalComplexity_anti
  • Functions.lean: card_lt_two_pow_of_run_eq_greaterThan
  • Protocol.lean: exists_solves_depth_eq_ecomplexity, ecomplexity_mono
  • Randomized.lean: errorProb_nonneg, errorProb_pure, solves_pure, ecomplexity_mono, ecomplexityFun_le_protocol, depth_toPublicCoin_le, solves_comap, ecomplexity_mono, ecomplexityFun_le_protocol
  • Rank.lean: rank_communicationMatrix_comp_le, rank_communicationMatrix_le_two_pow, signMatrix_eq_sub
  • RoundProtocol.lean: solvesKW_iff_solves
• Adjusted line breaking where prefixing private would exceed 100 columns.
• Excluded candidates:
  • Complexity.Computability.Communication.Protocol.Solves.of_imp (cited in module docstrings).
  • Complexity.Computability.Communication.Protocol.ecomplexity_ne_top_iff (referenced in Circuit/Monotone/Clique/Essential.lean).
  • Complexity.Computability.Communication.Randomized.PrivateCoin.le_ecomplexity_iff and ecomplexity_anti (used across modules).
  • Yao's minimax principle statements (*_le_iff_forall_distributionalComplexity_le) in Distributional.lean (intended public API).

Validation

Ran full validation on commit fe37d674:

• scripts/check.sh:
  • lake build --wfail --iofail (passed)
  • lake exe mk_all --check (passed)
  • lake test --wfail --iofail (passed)
  • lake lint (passed)
  • lake exe lint-style (passed)
  • lake exe checkInitImports (passed)
• python3 scripts/check_hygiene.py (all checks passed)
• python3 scripts/check_tidy_surface.py (1301 statements in 225 modules, matching baseline)
• python3 scripts/check_docs.py --config-only (consistent)

AI disclosure

Assisted by Jetski (Google internal pair programming agent). All changes verified with Lean compiler, test suite, and repo linters.

Refs #899 (Item 9)

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at fe37d67.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — CHANGES REQUESTED at fe37d67

Agent review, not human approval. Hosted ci-checks is green at this head.

Mechanically the diff is clean: in all 8 files only private is added (27 declarations, counting the duplicated names in PublicCoin and PrivateCoin), and nothing else changes. It also merges cleanly with #934, which touches different names in Discrepancy.lean and Functions.lean.

Blocking: under the privatize-by-intent rule recorded in #926 (CONTRIBUTING, "Public surface under the module system"), most of these are API and must stay public. That rule keeps public, even when currently unused, characterizations, bounds, monotonicity and closure lemmas, simp equations and invariance lemmas stated in terms of public definitions; only proof plumbing and facts about module-local constructions become private. Please drop private from these 19:

• Discrepancy.lean: abs_sum_le_discrepancy, exists_abs_sum_eq_discrepancy (the defining bound and attainment of discrepancy).
• Distributional.lean: le_distributionalComplexity_iff, distributionalComplexity_anti.
• Protocol.lean: exists_solves_depth_eq_ecomplexity, ecomplexity_mono.
• Randomized.lean, PublicCoin: errorProb_nonneg, errorProb_pure, solves_pure, ecomplexity_mono, ecomplexityFun_le_protocol.
• Randomized.lean, PrivateCoin: depth_toPublicCoin_le, solves_comap, ecomplexity_mono, ecomplexityFun_le_protocol.
• Rank.lean: rank_communicationMatrix_comp_le, rank_communicationMatrix_le_two_pow, signMatrix_eq_sub.
• RoundProtocol.lean: solvesKW_iff_solves.

These remain reasonable to privatize, as they are facts about the disjointness and greater-than proof constructions:

• Disjointness.lean: mem_parts, compl_insert_eq_of_mem_parts, sum_parts, sum_parts_swap, card_parts_pos, hardWeight_nonneg, hardDist_apply_toReal.
• Functions.lean: card_lt_two_pow_of_run_eq_greaterThan.

If parts, hardWeight and hardDist are themselves only proof constructions, consider making those definitions private too, in a follow-up.

[SamuelSchlesinger]

Thanks @reviewer-claude-c4b0c164-01 for the careful review and reference to the #926 privatize-by-intent rule.

Updated in 8b8282d:

• Dropped private from all 19 public API declarations across Discrepancy.lean, Distributional.lean, Protocol.lean, Randomized.lean, Rank.lean, and RoundProtocol.lean.
• Retained private strictly on the 8 proof-construction helpers:
  • Disjointness.lean (7): mem_parts, compl_insert_eq_of_mem_parts, sum_parts, sum_parts_swap, card_parts_pos, hardWeight_nonneg, hardDist_apply_toReal
  • Functions.lean (1): card_lt_two_pow_of_run_eq_greaterThan
• Rebased cleanly onto main (759db832).

Full validation on 8b8282d

• lake build --wfail --iofail (ok)
• lake exe mk_all --check (ok)
• lake test --wfail --iofail (ok)
• lake lint (ok)
• lake exe lint-style (ok)
• lake exe checkInitImports (ok)
• python3 scripts/check_hygiene.py (ok)
• python3 scripts/check_tidy_surface.py (1301 statements in 225 modules, matching baseline)
• python3 scripts/check_docs.py --config-only (consistent)

Ready for re-review.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at 8b8282d (agent review, not human approval)

Delta review against reviewer-claude-c4b0c164-01's change request at fe37d67. The request is resolved: all 19 declarations it listed are public again. These are the 2 in Discrepancy, 2 in Distributional, 2 in Protocol, 5 under PublicCoin and 4 under PrivateCoin in Randomized, 3 in Rank and 1 in RoundProtocol. Those files no longer appear in the diff. The diff is now exactly private added to the 8 declarations that review accepted: 7 in Disjointness.lean and card_lt_two_pow_of_run_eq_greaterThan in Functions.lean. No library module, test, abstract, guide page or module docstring outside their own declarations names any of the 8. Hosted ci-checks passed on this head.

Nonblocking. parts, hardWeight and hardDist are public and listed under Main definitions, and public results (card_parts, sum_hardWeight, corrupted_hardDist) are stated about them. So mem_parts, card_parts_pos, hardWeight_nonneg and hardDist_apply_toReal fit #926's wording "characterizations and bounds about public definitions". Since the earlier review accepted them as construction facts, I am not blocking on it. The consistent follow-up is either to keep these four public, or to make the three definitions private, as that review suggested.