[SamuelSchlesinger]

Makes 41 declarations in Foundations, Probability and Languages public again (28 API, 13 general mathematics), across 29 files. Earlier passes made them private because nothing outside their module used them (#628 (31), d5aa083 (5), ef44ce8 (2), 528d3fe (1), #691 (1), 10c4f69 (1)). Under the privatize-by-intent rule of #926, they are library API or general mathematics, so a later contributor should find them instead of re-proving them. Part of the audit tracked on #587.

Each change deletes the word private; no statement, proof or name changes, and no declaration moves.

Classification rule (#926, CONTRIBUTING "Public surface under the module system"):

• PLUMBING stays private: a step meaningful only inside one proof, or a fact about a module-local construction, encoding or intermediate quantity.
• API becomes public: a fact stated only in terms of public definitions that a user would expect, such as characterizations, bounds, monotonicity and closure, simp and equation lemmas, invariance lemmas and named results.
• GENERAL becomes public: general mathematics (lists, finsets, arithmetic, probability, linear algebra). Those outside Complexity/Foundations belong there; they are listed below as follow-ups, not moved here.

The other privatized declarations in this area were judged PLUMBING and stay private.

The 41 declarations

Declaration	File	Class	Reason
bernoulliWeight_split	Foundations/BooleanAnalysis/Bernoulli.lean	API	product formula for public bernoulliWeight
sum_mul_log_ge	Foundations/BooleanAnalysis/Fibers.lean	GENERAL	general log-sum inequality
expect_log_card_fiber	Foundations/BooleanAnalysis/Fibers.lean	GENERAL	general Finset log fiber bound
projectionAverage_cons_false	Foundations/BooleanAnalysis/HarmonicTransform.lean	API	equation lemma for public projectionAverage
projectionAverage_cons_true	Foundations/BooleanAnalysis/HarmonicTransform.lean	API	equation lemma for public projectionAverage
harmonicTransform_cons_false	Foundations/BooleanAnalysis/HarmonicTransform.lean	API	equation lemma for public harmonicTransform
harmonicTransform_cons_true	Foundations/BooleanAnalysis/HarmonicTransform.lean	API	equation lemma for public harmonicTransform
expect_mul_noiseOp_mul_le	Foundations/BooleanAnalysis/Hypercontractivity.lean	API	noiseOp hypercontractive-type bound
abs_derivative_signVal_rpow	Foundations/BooleanAnalysis/Hypercontractivity/Derivative.lean	API	derivative of signVal power identity
chi_update_not_of_mem	Foundations/BooleanAnalysis/Hypercube.lean	API	chi flip sign property
sum_filter_mem_fourierCoeff_sq_div_card_le_influence	Foundations/BooleanAnalysis/KahnKalaiLinial.lean	API	general Fourier-weight bound by public influence
exists_subset_card_eq_mul_sum_le	Foundations/Combinatorics/AffineDisperser.lean	GENERAL	general Finset averaging subset
eventually_mul_pow_le_two_pow	Foundations/Combinatorics/AffineDisperser/Threshold.lean	GENERAL	general eventual polynomial vs 2^n bound
tendsto_log_two_atTop	Foundations/Combinatorics/AffineDisperser/Threshold.lean	GENERAL	general Nat.log tendsto
card_middle_le	Foundations/Combinatorics/CentralBinomial.lean	GENERAL	general central binomial cardinality bound
expect_walkDart_mk	Foundations/Combinatorics/Expander/Walk.lean	API	expectation lemma for public walkDart
minimalPeriod_eq_of_periodic_iterates	Foundations/Combinatorics/FunctionalGraph/Cycle.lean	GENERAL	general function-iterate minimalPeriod fact
forestPath_step	Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean	API	equation lemma for public forestPath
forestPath_iterate_prefix	Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean	API	prefix property of public forestPath
two_ne_of_maj3_ne	Foundations/Combinatorics/MajorityTree.lean	API	basic property of public maj3
card_filter_extensions_free_eq	Foundations/Data/BitString/PartialAssignment/Counting.lean	API	cardinality of public extensions
card_filter_extensions_not_nonempty_inter	Foundations/Data/BitString/PartialAssignment/Counting.lean	API	cardinality of public extensions
card_filter_extends_withFree	Foundations/Data/BitString/PartialAssignment/Counting.lean	API	cardinality of withFree extensions
card_filter_outside_eq	Foundations/Data/BitString/PartialAssignment/Counting.lean	API	cardinality fiber of outside
shortWords_eq_biUnion	Foundations/Data/BitString/ShortWords.lean	API	characterization of public shortWords
card_filter_filter_ne_eq	Foundations/Data/Code/HammingBound.lean	GENERAL	general Hamming-sphere fiber cardinality
mulPrefix_succ	Foundations/Data/Nat/Bitwise/Multiplication.lean	API	equation lemma for public mulPrefix
mulCarry_succ	Foundations/Data/Nat/Bitwise/Multiplication.lean	API	equation lemma for public mulCarry
listBlank_mk_cons_toList	Foundations/Data/StackTape.lean	API	toList/ListBlank bridge for StackTape
exists_code_irreducible	Foundations/FieldTheory/Finite/BinaryField.lean	API	existence of irreducible code polynomial
linearizedEval_sub_mul	Foundations/FieldTheory/Finite/LinearizedPolynomial.lean	API	linearity property of linearizedEval
span_range_row_submatrix_eq_map	Foundations/LinearAlgebra/Matrix/CutRank.lean	GENERAL	general matrix row span fact
ncard_preimage_add_ncard_preimage_le	Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean	GENERAL	general ncard preimage inequality
eval_extract_ofFn	Languages/Probabilistic/LinearHash.lean	API	eval lemma for public LinearHash.extract
uniform_prefix	Probability/BitString/LinearHash.lean	GENERAL	general uniform PMF prefix map
apply_le_map_fst	Probability/Conditioning.lean	GENERAL	general PMF joint bound
mean_conditionalEntropy_hash_le	Probability/HashIsolation.lean	API	conditional entropy hash bound
conditionalEntropy_map_restrict_le	Probability/Shearer.lean	API	monotonicity of conditional entropy
entropy_map_restrict_univ	Probability/Shearer.lean	API	entropy invariance under restrict
expect_signVal_dotProduct	Probability/SmallBias/Powering.lean	API	dotProduct expectation of signVal
card_filter_sum_pow_eq_zero_le	Probability/SmallBias/Powering.lean	GENERAL	general polynomial root-count style bound

Validation
At head 86669f9f (base 9a1dc195), LEAN_NUM_THREADS=8 scripts/check.sh:

ok    build --wfail --iofail
ok    mk_all --check
ok    test --wfail --iofail
ok    lint
ok    lint-style
ok    checkInitImports

python3 -B scripts/check_tidy_surface.py: 1301 public tidy statements in 225 modules, matching the baseline. python3 -B scripts/check_hygiene.py --check-simp: all hygiene checks passed.

Abstracts. No impact: no statement, definition or curated abstract changes.

AI disclosure. Prepared with Claude Code as worker-claude-privaudit-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Review requested from coordinator-claude-c4b0c164-20261023 at 86669f9f. The change only removes private from the 41 declarations listed in the body, so every statement keeps its meaning; the classification table under #926 is the part to check.

[SamuelSchlesinger]

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

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at 86669f9 (delegated-review exception, AGENTS.md; classification: un-privatization, statement-preserving)

Agent review, not human approval. Against merge base 9a1dc195, every changed file (29) equals the base with exactly the private keywords removed (whitespace-normalized), so 41 declarations become public and nothing else changes. scripts/tidy_surface_baseline.json is untouched, and hosted ci-checks is green at this head.

The #926 spot-check is consistent: these are Foundations and Probability facts stated in terms of public definitions, for example card_middle_le, apply_le_map_fst, uniform_prefix, mulPrefix_succ, two_ne_of_maj3_ne and listBlank_mk_cons_toList.

Nonblocking: AffineDisperser/Threshold.tendsto_log_two_atTop (Tendsto (Nat.log 2) atTop atTop) and eventually_mul_pow_le_two_pow are generic asymptotics. Check Mathlib for an existing Nat.log tendsto lemma before exporting a copy under a combinatorics namespace.