[SamuelSchlesinger]

Makes 51 declarations in Circuit/Rational and Circuit/Arithmetic public again (7 API, 44 general mathematics), across 18 files. Earlier passes made them private because nothing outside their module used them (#841 (49), 4bfb0e4 (2)). 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). These belong in Complexity/Foundations and are listed below as follow-ups, not moved here.

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

The 51 declarations

Declaration	File	Class	Reason
binaryMultiplicationCount_bit	Circuit/Arithmetic/Power.lean	API	equation lemma for public binaryMultiplicationCount
totalDegree_booleanSum_le	Circuit/Arithmetic/VNP.lean	API	degree bound on public booleanSum
Circuit.aeval_polynomial_mvPolynomial	Circuit/Arithmetic/VP.lean	API	evaluation lemma for public Circuit.polynomial
polynomial_comp_projectionCircuit	Circuit/Arithmetic/VP.lean	API	polynomial of composition with projectionCircuit
Term.cost_program_toCircuit	Circuit/Arithmetic/Waring/Compilation.lean	API	cost of compiled Waring term circuit
Term.mulCost_toCircuit	Circuit/Arithmetic/Waring/Compilation.lean	API	multiplication cost of Term.toCircuit
Term.addCost_toCircuit	Circuit/Arithmetic/Waring/Compilation.lean	API	addition cost of Term.toCircuit
ratio_num_le	Circuit/Rational/EncodingBounds.lean	GENERAL	general bound on Rat.divInt numerator
ratio_den_le	Circuit/Rational/EncodingBounds.lean	GENERAL	general bound on Rat.divInt denominator
determinant_bound	Circuit/Rational/EncodingBounds.lean	GENERAL	general integer determinant bound
upper_unit	Circuit/Rational/Eval.lean	GENERAL	general block matrix unit fact
lower_unit	Circuit/Rational/Eval.lean	GENERAL	general block matrix unit fact
schur_factor	Circuit/Rational/Eval.lean	GENERAL	general Schur complement factorization
integer_grid	Circuit/Rational/Generator.lean	GENERAL	general polynomial grid nonvanishing fact
scaled_normalization	Circuit/Rational/IntegralLift.lean	GENERAL	general matrix inverse scaling invariance
exists_independent_subfamily	Circuit/Rational/LaurentReduction.lean	GENERAL	general linear algebra independent subfamily
matrix_inverse_left	Circuit/Rational/MatrixEval.lean	GENERAL	general adjugate left inverse
matrix_inverse_right	Circuit/Rational/MatrixEval.lean	GENERAL	general adjugate right inverse
coeff_mul_support_superset	Circuit/Rational/QuantumMatrices.lean	GENERAL	general Hahn series coefficient of product
power_finite_co_support	Circuit/Rational/QuantumSeries.lean	GENERAL	general Hahn series power co-support finiteness
sum_map_drop_range_fin	Circuit/Rational/Runtime/Determinant.lean	GENERAL	general list/Finset sum identity
natAbs_sum_le	Circuit/Rational/Runtime/Determinant.lean	GENERAL	general natAbs bound on list sums
natAbs_take_sum_le	Circuit/Rational/Runtime/Determinant.lean	GENERAL	general natAbs bound on list prefix sums
divInt_num_abs_eq	Circuit/Rational/Runtime/Encode.lean	GENERAL	general Rat.divInt numerator formula
divInt_den_eq	Circuit/Rational/Runtime/Encode.lean	GENERAL	general Rat.divInt denominator formula
divInt_sign_eq	Circuit/Rational/Runtime/Encode.lean	GENERAL	general Rat.divInt sign formula
natAbs_pow_le	Circuit/Rational/Runtime/Lift.lean	GENERAL	general natAbs power bound
val_finEquiv	Circuit/Rational/Runtime/Lift/Defs.lean	GENERAL	general ZMod.finEquiv val fact
sum_range_eq_sum_fin	Circuit/Rational/Runtime/Lift/Defs.lean	GENERAL	general list range sum equals Fin sum
sum_range_eq_sum_zmod	Circuit/Rational/Runtime/Lift/Defs.lean	GENERAL	general list range sum equals ZMod sum
val_sub_eq_mod	Circuit/Rational/Runtime/Lift/Defs.lean	GENERAL	general ZMod subtraction val formula
sum_fin_val_le_square	Circuit/Rational/SmallExpansion.lean	GENERAL	general Fin val sum bound
det_factor_column_orders	Circuit/Rational/Wronskian.lean	GENERAL	general polynomial matrix determinant factoring
coeff_scaled_derivative_at	Circuit/Rational/Wronskian.lean	GENERAL	general scaled derivative coefficient formula
scaled_derivative_order	Circuit/Rational/Wronskian.lean	GENERAL	general polynomial derivative divisibility
exists_degree_echelon_family	Circuit/Rational/Wronskian.lean	GENERAL	general echelon family for polynomial subspaces
order_reflect	Circuit/Rational/Wronskian.lean	GENERAL	general polynomial reflect trailing degree
exists_order_echelon_family	Circuit/Rational/Wronskian.lean	GENERAL	general echelon family for polynomial subspaces
wronskian_linearCombination	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian linear combination
basis_toMatrix_det_ne_zero	Circuit/Rational/Wronskian.lean	GENERAL	general basis change determinant nonzero
wronskian_basis_change	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian basis change
exists_order_echelon_basis	Circuit/Rational/Wronskian.lean	GENERAL	general echelon basis for polynomial subspaces
wronskian_basis_ne_zero	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian nonvanishing
derivative_taylor	Circuit/Rational/Wronskian.lean	GENERAL	general derivative of taylor
iterate_derivative_taylor	Circuit/Rational/Wronskian.lean	GENERAL	general iterated derivative of taylor
wronskian_taylor	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian of taylor
natDegree_wronskian_le	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian degree bound
sum_rootMultiplicity_le_natDegree	Circuit/Rational/Wronskian.lean	GENERAL	general root multiplicity sum bound
wronskian_order_at	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian order at a point
wronskian_basis_rootMultiplicity	Circuit/Rational/Wronskian.lean	GENERAL	general Wronskian root multiplicity
low_coefficients_force_zero	Circuit/Rational/Wronskian.lean	GENERAL	general low-coefficient independence fact

Follow-up: Foundations candidates. These general facts should move to Complexity/Foundations in a later change:
ratio_num_le, ratio_den_le, determinant_bound, upper_unit, lower_unit, schur_factor, integer_grid, scaled_normalization, exists_independent_subfamily, matrix_inverse_left, matrix_inverse_right, coeff_mul_support_superset, power_finite_co_support, sum_map_drop_range_fin, natAbs_sum_le, natAbs_take_sum_le, divInt_num_abs_eq, divInt_den_eq, divInt_sign_eq, natAbs_pow_le, val_finEquiv, sum_range_eq_sum_fin, sum_range_eq_sum_zmod, val_sub_eq_mod, sum_fin_val_le_square, det_factor_column_orders, coeff_scaled_derivative_at, scaled_derivative_order, exists_degree_echelon_family, order_reflect, exists_order_echelon_family, wronskian_linearCombination, basis_toMatrix_det_ne_zero, wronskian_basis_change, exists_order_echelon_basis, wronskian_basis_ne_zero, derivative_taylor, iterate_derivative_taylor, wronskian_taylor, natDegree_wronskian_le, sum_rootMultiplicity_le_natDegree, wronskian_order_at, wronskian_basis_rootMultiplicity, low_coefficients_force_zero.

Re-proof found. Circuits.Rational.sum_range_eq_sum_fin has an alpha-equivalent private copy, AffineDisperser.sum_map_range in Complexity/AffineDisperser/Coordinates.lean. Neither module imports the other, so the copy is left for the Foundations move, which can then delete it.

Validation
At head c1c43e94 (base 36f94d8d), LEAN_NUM_THREADS=6 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 c1c43e94. The change only removes private from the 51 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 c1c43e9.

[SamuelSchlesinger]

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

Evidence: against merge base 36f94d8d, every changed file equals the base with exactly the private keywords removed (whitespace-normalized), giving 51 declarations made public, with nothing else changed. scripts/tidy_surface_baseline.json is untouched, and hosted ci-checks is green at this head, including the ratchet. Agent review, not human approval.
Nonblocking (#926 spot-check): the sampled statements are general mathematics, not plumbing. Examples are block-matrix factorization (Eval.schur_factor, upper_unit), EncodingBounds.determinant_bound (|det A| ≤ d!·Bᵈ), the Schwartz–Zippel grid Generator.integer_grid, and the Wronskian lemmas. They now become public under generic names in the Rational namespace (upper_unit, schur_factor, integer_grid, scaled_normalization, ratio_num_le). A follow-up should move them to Foundations with Mathlib-style names.