[SamuelSchlesinger]

Makes 42 declarations in Logics, Algorithms and Computability/WordRAM public again (37 API, 5 general mathematics), across 24 files. Earlier passes made them private because nothing outside their module used them (#868 (25), #601 (8), #606 (5), #634 (3), 036aad3 (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). 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 42 declarations

Declaration	File	Class	Reason
listPredecessor_append	Algorithms/Lean/FusionTree/Tree.lean	API	equation lemma for public listPredecessor
listPredecessor_ne_none_iff	Algorithms/Lean/FusionTree/Tree.lean	API	spec of listPredecessor
listPredecessor_some_spec	Algorithms/Lean/FusionTree/Tree.lean	API	spec of listPredecessor
IsBitonic.min_le_max_halves	Algorithms/Lean/Sort/Bitonic/Correctness.lean	API	half-cleaner property of public IsBitonic
isBitonic_append	Algorithms/Lean/Sort/Bitonic/Correctness.lean	API	bitonic-sequence closure property
sort_sorted	Algorithms/Lean/Sort/Bitonic/Correctness.lean	API	headline sortedness of bitonic sort
start_mem_search	Algorithms/Reachability/BreadthFirst.lean	API	start belongs to search result
reachable_lt	Algorithms/Reachability/InductiveCounting/Semantics.lean	API	characterization of reachability/roundSet semantics
roundSet_zero	Algorithms/Reachability/InductiveCounting/Semantics.lean	API	characterization of reachability/roundSet semantics
mem_roundSet_succ	Algorithms/Reachability/InductiveCounting/Semantics.lean	API	characterization of reachability/roundSet semantics
mem_roundSet_final	Algorithms/Reachability/InductiveCounting/Semantics.lean	API	characterization of reachability/roundSet semantics
minimum_mem	Algorithms/WordRAM/FusionTree/Preprocessing.lean	API	basic property of public fusion-tree minimum
successor_eq_least	Algorithms/WordRAM/VanEmdeBoas/Call.lean	API	spec of van Emde Boas successor
member_eq_false_of_max_lt	Algorithms/WordRAM/VanEmdeBoas/Member.lean	API	membership property of VEB tree
member_maximum	Algorithms/WordRAM/VanEmdeBoas/Member.lean	API	membership property of VEB tree
clear_succ	WordRAM/Allocation.lean	API	equation lemma for clear
copyPrefix_succ	WordRAM/Copy.lean	API	equation lemma for copyPrefix
step_halt_mono_width	WordRAM/Defs.lean	API	halting monotone in word width for step
next_mapOp	WordRAM/MapOp.lean	API	mapOp invariance of Next/Runs
runs_mapOp	WordRAM/MapOp.lean	API	mapOp invariance of Next/Runs
eval_congr	WordRAM/Multiword/CircuitRun.lean	API	congruence property of circuit Operation
admissible_congr	WordRAM/Multiword/CircuitRun.lean	API	congruence property of circuit Operation
Data.comap_extend	WordRAM/Structured.lean	API	simp equation for public Data.extend/Data.comap
Data.extend_extend	WordRAM/Structured.lean	API	simp equation for public Data.extend
Op.eval_modifies	WordRAM/Trace.lean	API	public Op.eval writes only its probed cells
isCarrySuccessor_of_lexRank_succ	Logics/FirstOrder/Ordered/TupleSuccessor.lean	API	successor direction for public lexRank and IsCarrySuccessor
satisfiable_copies_iff	Logics/FirstOrder/Problems/CNF.lean	API	satisfiability is invariant under public Copies
isThreeCNF_copies_iff	Logics/FirstOrder/Problems/CNF.lean	API	3-CNF shape is invariant under public Copies
simpleGraph_copies_iff	Logics/FirstOrder/Problems/Coloring.lean	API	graph axioms are invariant under public Copies
independentSet_copies_iff	Logics/FirstOrder/Problems/IndependentSetReduction.lean	API	independent-set membership is invariant under public Copies
Clause.length_split3	Logics/Propositional/CNF/ThreeCNF.lean	API	length of public Clause.split3
CNF.IsExactThreeDistinct.expect_countUnsat	Logics/Propositional/CNF/UnsatVal.lean	API	expected-unsat / relabel property of IsExactThreeDistinct
Clause.IsExactThreeDistinct.relabel_of_injOn	Logics/Propositional/CNF/UnsatVal.lean	API	expected-unsat / relabel property of IsExactThreeDistinct
exists_mul_pow_le_pow	Logics/Propositional/ClauseSet/Sparsification.lean	GENERAL	general real/natural exponential inequality
toClauseSet_append	Logics/Propositional/ClauseSet/Sparsification/List.lean	API	basic property of CNF-to-clause-set conversion
toClauseSet_mono	Logics/Propositional/ClauseSet/Sparsification/List.lean	API	basic property of CNF-to-clause-set conversion
subclause_eq_true_iff	Logics/Propositional/ClauseSet/Sparsification/List.lean	API	basic property of CNF-to-clause-set conversion
toFinset_filter_not_mem	Logics/Propositional/ClauseSet/Sparsification/List.lean	GENERAL	list filter to Finset difference fact
Derives.exists_isProof	Logics/Propositional/Resolution/Proof.lean	API	derivation yields a proof list, basic property of Derives
exists_forall_parityOn_incidence_eq_xor	Logics/Propositional/Tseitin.lean	GENERAL	edge assignment with prescribed vertex parities on a connected multigraph
parityOn_univ_eq_false_of_forall	Logics/Propositional/Tseitin.lean	GENERAL	handshake parity identity for multigraph incidences
exists_forall_parityOn_incidence_eq	Logics/Propositional/Tseitin.lean	GENERAL	edge assignment realizing any vertex charge up to one vertex

Follow-up: Foundations candidates. These general facts should move to Complexity/Foundations in a later change:
exists_mul_pow_le_pow, toFinset_filter_not_mem, exists_forall_parityOn_incidence_eq_xor, parityOn_univ_eq_false_of_forall, exists_forall_parityOn_incidence_eq.

Validation
At head 5ed9cfe7 (base 9a1dc195), 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 5ed9cfe7. The change only removes private from the 42 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 5ed9cfe.

[SamuelSchlesinger]

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

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

Nonblocking (#926 spot-check):

• The sample is reasonable API: the WordRAM step and copy equations (clear_succ, copyPrefix_succ), step_halt_mono_width, eval_congr/admissible_congr, minimum_mem, the listPredecessor specs and the Tseitin parity lemmas.
• ClauseSet/Sparsification.exists_mul_pow_le_pow (∃ α ≥ 1, C·αᵈ ≤ r^α) and Sparsification/List.toFinset_filter_not_mem are general facts that would be more discoverable in Foundations.