[SamuelSchlesinger]

Generalizes the circuit fan-in input support bound in Complexity/Computability/Circuit/FanIn.lean to arbitrary per-operation weights $w$ satisfying $\forall op, \sigma.\text{Arity } op \le 1 + w(op)$, eliminating 90 lines of duplicate induction and helper theorems in Complexity/Computability/Circuit/Boolean/BinaryCost.lean.

Covers Item 7 (F4) of #884.

Summary of changes

• In Complexity/Computability/Circuit/FanIn.lean:
  • Made Wire.castSucc_injective, Program.reachableInputs, and Program.support_subset_reachableInputs public with docstrings.
  • Generalized Program.card_reachableInputs_le to Program.card_reachableInputs_le_cost for any weight function $w : \sigma.\text{Op} \to \mathbb{N}$ with $\forall op, \sigma.\text{Arity } op \le 1 + w(op)$.
  • Added public Program.card_biUnion_wireSupport_le_cost bounding wire support by frontier size plus program cost under $w$.
  • Deduced Program.card_reachableInputs_le in 5 lines via the cost bound for FanInAtMost r.
  • Added public import Cslib.Computability.Circuit.Simulation.
• In Complexity/Computability/Circuit/Boolean/BinaryCost.lean:
  • Added public import Complexity.Computability.Circuit.FanIn.
  • Removed duplicate private theorem wire_castSucc_injective'.
  • Simplified Program.card_biUnion_wireSupport_le_cost_binaryCost to a single line invoking Program.card_biUnion_wireSupport_le_cost with Boolean.binaryCost and Boolean.arity_le_one_add_binaryCost.
  • Preserved the statement of Program.card_biUnion_wireSupport_le_cost_binaryCost unchanged for downstream consumers (e.g. feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875).

Verification

All checks passed on commit 03f823f9 (rebased on origin/main at 36f94d8d):

• scripts/check.sh (all 6 gates: build, mk_all, test, lint, lint-style, checkInitImports)
• python3 scripts/check_hygiene.py
• python3 scripts/check_tidy_surface.py (1301 statements in 225 modules, matching baseline)
• python3 scripts/check_docs.py --config-only

AI disclosure

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

Refs #884 (Item 7, F4)

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at 03f823f.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — CHANGES REQUESTED at 03f823f (agent review)

The generalization is faithful. card_reachableInputs_le_cost replaces (r - 1) * g under FanInAtMost r with program.cost w under ∀ op, σ.Arity op ≤ 1 + w op, and the induction is the old one with r replaced by 1 + w line.op. The fan-in case is recovered exactly, not weakened. The weight max (r - 1) (Arity op - 1) satisfies the hypothesis for every operation, and on a program of fan-in at most r its cost is at most (r - 1) * g (cost_le_of_fanInAtMost). So the private card_reachableInputs_le keeps its statement, and Circuit.card_inputSupport_le_size, essential_le_size and the other public results are unchanged. Program.card_biUnion_wireSupport_le_cost_binaryCost keeps its statement, which ReadOnce.lean:751 uses, and becomes a one-line instance with arity_le_one_add_binaryCost, as #884 F4 proposed. Hosted ci-checks passed. The PR merges cleanly with current main (it predates #931–#934) and does not touch ComplexityTests.lean.

Blocking

1. Surface. Complexity/Computability/Circuit/FanIn.lean:47 (Program.reachableInputs, now a public, exposed def), :81 (Program.support_subset_reachableInputs) and :137 (Program.card_reachableInputs_le_cost) become public. reachableInputs is a backward over-approximation of the public Program.wireSupport, used only to prove the support bound: it duplicates a notion the library already has. The doc(contributing): privatize by intent, not by current usage #926 audit (refactor(Circuit): make 53 API and general declarations public again in Frontier, Fusion, Monotone and root modules (#926) #932, now on main) kept these three private as plumbing. The intended public result is Program.card_biUnion_wireSupport_le_cost, stated over wireSupport; its proof can use the private lemmas. Please keep the three private and drop the Main definitions entry and the card_reachableInputs_le_cost bullet at :21–30. Making Wire.castSucc_injective public is fine; F4 asked for it.
2. Third copy. Complexity/Computability/Circuit/Boolean/ReadOnce.lean:676 has another private wire_castSucc_injective'', with the same statement and proof. Now that Wire.castSucc_injective is public, replace its two uses (:773, :841) and delete the copy.

Nonblocking

• Boolean/BinaryCost.lean:10: public import Complexity.Computability.Circuit.FanIn is a proof-only dependency, because no public statement in BinaryCost mentions FanIn. A plain import keeps the fan-out down. ReadOnce.lean would then import FanIn directly for item 2.

[SamuelSchlesinger]

Thanks @reviewer-claude-c4b0c164-02 for the precise review and suggestions.

Updated in 5008448:

1. Kept Program.reachableInputs, Program.support_subset_reachableInputs, and Program.card_reachableInputs_le_cost private in Complexity/Computability/Circuit/FanIn.lean, preserving the surface of refactor(Circuit): make 53 API and general declarations public again in Frontier, Fusion, Monotone and root modules (#926) #932. Dropped the Main definitions and bullet from module header.
2. Deleted duplicate private wire_castSucc_injective'' in Complexity/Computability/Circuit/Boolean/ReadOnce.lean and used public Wire.castSucc_injective.
3. In Complexity/Computability/Circuit/Boolean/BinaryCost.lean, narrowed FanIn import to plain import; added plain import Complexity.Computability.Circuit.FanIn to ReadOnce.lean.

Rebased on latest main and validated build, lint-style, docs, and hygiene. Ready for re-review.

[SamuelSchlesinger]

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

Delta review of 5008448. The generalization commit is unchanged by git range-diff (03f823f = 79f08ba), so my earlier faithfulness check still holds: the weighted bound recovers (r - 1) * g exactly, and the public statements are unchanged.

1. Resolved. Program.reachableInputs, Program.support_subset_reachableInputs and Program.card_reachableInputs_le_cost are private again. The Main definitions section and the card_reachableInputs_le_cost bullet are gone. The public additions are now just Program.card_biUnion_wireSupport_le_cost (listed in Main results) and Wire.castSucc_injective.
2. Resolved. ReadOnce.lean's wire_castSucc_injective'' is deleted, and both uses now go through Wire.castSucc_injective with a direct import …Circuit.FanIn. No other wire_castSucc_injective copy remains.

• The nit is also taken: BinaryCost.lean now imports FanIn with a plain import.

Hosted ci-checks passed on this head.