[SamuelSchlesinger]

Makes 53 declarations in the Circuit Frontier, Fusion, Monotone, Cyclic, Encoding and root modules public again (47 API, 6 general mathematics), across 32 files. Earlier passes made them private because nothing outside their module used them (#841 (53)). 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 53 declarations

Declaration	File	Class	Reason
card_programExceptions_le	Circuit/Approximation.lean	API	cardinality bound on public programExceptions
circuit_correct	Circuit/Approximation.lean	API	correctness of approximation scheme circuit
card_le_of_contains_ofColoring	Circuit/Clique.lean	API	bound for public Clique.Contains ofColoring
elim_feedbackWire	Circuit/Cyclic/Feedback.lean	API	simp lemma for public feedbackWire
Line.code_mapOp	Circuit/Encoding/MapOp.lean	API	equation lemma for public mapOp
Program.code_mapOp	Circuit/Encoding/MapOp.lean	API	equation lemma for public mapOp
Program.lines_replaceGates	Circuit/Erase.lean	API	equation lemma for public replaceGates
Program.lines_eraseGates_of_special	Circuit/Erase.lean	API	equation lemma for public eraseGates
Program.lines_eraseGates_of_not_special	Circuit/Erase.lean	API	equation lemma for public eraseGates
Program.arity_lines_eraseGates	Circuit/Erase.lean	API	arity equation for public eraseGates
Program.card_wireSupport_le_pow	Circuit/FanIn.lean	API	bound on public wireSupport card
agreement_add_agreement_compl	Circuit/Frontier/AverageCase.lean	API	complement identity for public agreement
SmallSides.one_lt	Circuit/Frontier/BranchingProgram.lean	API	basic property of public SmallSides
exists_natLog_le_mul_add	Circuit/Frontier/Layouts/Basic.lean	GENERAL	general Nat.log linear bound
vertexCorrelation_lt_one	Circuit/Frontier/Layouts/BoundedDegree.lean	API	basic bound on public vertexCorrelation
ncard_eq_sum_indicator	Circuit/Frontier/Layouts/Gaussian/Basic.lean	GENERAL	general ncard/indicator sum identity
ncard_lt_of_not_le_abs	Circuit/Frontier/Layouts/Gaussian/Basic.lean	GENERAL	general ncard inequality from indicator sums
measureReal_pi_eq	Circuit/Frontier/Layouts/Gaussian/Basic.lean	GENERAL	Gaussian product measure identity
MaxDegreeLE.edgeRestrict	Circuit/Frontier/Layouts/General.lean	API	closure of MaxDegreeLE under edgeRestrict
ncard_inter_touching	Circuit/Frontier/Layouts/Local.lean	GENERAL	general multigraph ncard decomposition
exists_score_le	Circuit/Frontier/Layouts/Median.lean	API	basic property of public IsMedian
exists_le_score	Circuit/Frontier/Layouts/Median.lean	API	basic property of public IsMedian
ncard_endpoints_le	Circuit/Frontier/Layouts/Median.lean	API	bound on public Multigraph endpoints
logb_ncard_le_self	Circuit/Frontier/LowerBound.lean	GENERAL	general logb/ncard bound for sets of functions
touching_eq_of_edgeCut_eq_empty	Circuit/Frontier/Multigraph.lean	API	characterization of public touching for cut-free sets
connectedComponentMk_src	Circuit/Frontier/Multigraph.lean	API	basic fact for public Multigraph.toSimpleGraph
toSimpleGraph_induce	Circuit/Frontier/Multigraph.lean	API	induce commutes with public toSimpleGraph
ncard_edges_le	Circuit/Frontier/Network.lean	API	edge bound for public Network.branchingProgram
ncard_edges_last_le	Circuit/Frontier/Network.lean	API	edge bound for public Network.branchingProgram
cycleRank_le_of_nondeterministicDecides	Circuit/Frontier/Nondeterministic.lean	API	lower-bound result for nondeterministic circuits
logb_ncard_le_width_of_nondeterministicDecides	Circuit/Frontier/Nondeterministic.lean	API	lower-bound result for nondeterministic circuits
eventually_lt_innerSize_of_nondeterministicDecides	Circuit/Frontier/Nondeterministic.lean	API	lower-bound result for nondeterministic circuits
readAt_reindex	Circuit/Frontier/Projection.lean	API	reindex equation for public Network.readAt
read_reindex	Circuit/Frontier/Projection.lean	API	reindex equation for public Network.read
signedCount_eq_two_mul	Circuit/Frontier/Rectangle.lean	API	characterization of public signedCount
coverComplexity_le_program_cost	Circuit/Fusion/Basic.lean	API	cover complexity bound by public program cost
pairCoverComplexity_le_econondeterministicAndComplexity	Circuit/Fusion/Converse.lean	API	comparison of public complexity measures
econondeterministicAndComplexity_le_pairCoverComplexity	Circuit/Fusion/Converse.lean	API	comparison of public complexity measures
pairCoverComplexity_le_cyclic_cost	Circuit/Fusion/Cyclic.lean	API	cover complexity bound by cyclic circuit cost
PairCover.computesFrom_toCircuit	Circuit/Fusion/DeMorgan.lean	API	correctness of public PairCover.toCircuit
card_le_two_pow_length_inequality	Circuit/Fusion/Graph/Inequality.lean	API	size bound for pair covers of inequality
PairCover.ecomplexityFrom_le_sq	Circuit/Fusion/Quadratic.lean	API	complexity bound from public PairCover
stages_succ	Circuit/Iteration.lean	API	equation for public Synthesis.stages
Program.map_trace_polynomialInterpretation	Circuit/Linearize.lean	API	trace commutes with algebra map
affineInterpretation_taylorOp	Circuit/Linearize.lean	API	evaluation of public taylorOp
Program.arity_lines_linearize	Circuit/Linearize.lean	API	arity equation for public linearize
Program.innerGates_linearize	Circuit/Linearize.lean	API	innerGates of public linearize
Program.fanInAtMost_linearize	Circuit/Linearize.lean	API	fan-in characterization for public linearize
program_fanInAtMost_two	Circuit/Monotone/Clique/Essential.lean	API	fan-in bound for monotone programs
railBits_append	Circuit/Monotone/DualRail.lean	API	equation lemma for public railBits
dualCode_append	Circuit/Monotone/DualRail.lean	API	append lemma for public dualCode
exceedsAt_run_monotoneKWProtocol	Circuit/Monotone/KarchmerWigderson.lean	API	correctness of public monotoneKWProtocol (Karchmer-Wigderson)
Circuit.cost_program_withContext	Circuit/SimulationContext.lean	API	cost equation for public withContext

Follow-up: Foundations candidates. These general facts should move to Complexity/Foundations in a later change:
exists_natLog_le_mul_add, ncard_eq_sum_indicator, ncard_lt_of_not_le_abs, measureReal_pi_eq, ncard_inter_touching, logb_ncard_le_self.

Validation
At head 52401481 (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 52401481. The change only removes private from the 53 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 5240148.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at 5240148 (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 53 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 sample, for example SmallSides.one_lt, stages_succ, signedCount_eq_two_mul, circuit_correct and logb_ncard_le_self, is reasonable public API. The general measure and asymptotic facts Frontier/Layouts/Basic.exists_natLog_le_mul_add, Gaussian/Basic.ncard_eq_sum_indicator and measureReal_pi_eq would sit better in Foundations or Probability.