[SamuelSchlesinger]

Infrastructure only, no new mathematics. This PR does the M6.6 cleanup follow-ups from the #4497/#4501/#4509 reviews.

1. Cslib.Circuits.directProductInput removed in favour of Cslib.BitString.block. The two were the same function, fun j => x (finProdFinEquiv (i, j)), with the same argument order. Replication.lean and all 25 clients (18 library modules, 7 test files) now use BitString.block. Following the no-alias rule, the old name is gone and no deprecation is left behind. The client lemmas named after it are renamed to match:

• directProductInput_flatten → block_flatten, flatten_directProductInput → flatten_block (Sorting.lean)
• directProductInput_pack → block_pack (Iteration/Record.lean)
• directProductInput_eval_batchOrCircuit → block_eval_batchOrCircuit (MassProduction/Pipeline/Circuit.lean)

Apart from those names, every statement is unchanged: the only edit is the swap of two equal-by-definition terms. One proof side effect: BitString.block_apply is @[simp], but directProductInput had no simp lemma. So simp now unfolds fully applied blocks. That required changing three private proofs: BatchOr.layout_apply is restated in simp normal form, KeyedSort.output_key ends in a simp only, and an rfl in block_blockMap is gone.

2. Design.restrict_binaryPolynomial is derived from Design.mem_block_binaryPolynomial_iff. Membership in block i already does the parity arithmetic, so restricting to the cell (j, v) reduces to restrict_bitPolynomial (proof: 6 lines → 4). The statement is unchanged. The lemma now comes after the membership lemma, and its docstring points to it.

3. max 1 (clog 2 n) stays unshared with CSP.bitWidth. binaryFieldDegree n (the degree of the binary field in the NW design) and CSP.bitWidth n (an encoding width in Logics/Propositional/CSP/ToBoolean.lean) have the same body but different meanings, and each has public clients that state their own bounds. Sharing the definition would mean either importing CSP into NisanWigderson or changing public statements. A shared lemma isn't worth it either: the only common proof is two lines (n ≤ 2 ^ max 1 (clog 2 n)). The lowest suitable home, Foundations/Data/Nat/PowClog.lean, would gain a new public lemma and an import edge for those two lines.

Overlap. No file of #4522 (HardnessAmplification), #4524 (DirectProduct) or the upcoming CIKK 4b (UniformLearning/CIKK) is touched. #4529 also edits MCSP/PartialHardness/Completeness.lean, at other hunks (L12, L243; this PR changes L265–268). No open PR adds a use of directProductInput.

Duplicates. After a full build, python3 scripts/parallel_defs.py --theorems reports no duplicate statement among the 77 theorems examined, including the renamed block_* lemmas. python3 scripts/parallel_defs.py reports no parallel definition among the 8 declarations examined.

Manuals. No edit to either manual. Neither the Operator's Manual (manual/) nor the Agent Operator's Manual (AGENT_OPERATORS.md) mentions directProductInput, the renamed lemmas or restrict_binaryPolynomial. The same goes for results/, ROADMAP.md and the guides. Replication.lean's module docstring now lists blockMap/directProduct against BitString.block.

Validation. scripts/check.sh --quick passes (119 affected targets, source hygiene, ratchets, lint of the affected modules, mk_all --check), and so does lake build --wfail --iofail CslibFrontier. CI supplies the full run.

Written by a Jetski agent (meta-os18-thm5, session 63503c38) for Samuel Schlesinger. Not reviewed by a human.

[SamuelSchlesinger]

Agent review (reviewer review-4538, Jetski session d898e715) of d38fcff: approve.

• Migration is faithful. BitString.block and the removed directProductInput have the same body, fun j => x (finProdFinEquiv (i, j)), and the same argument order (block index, then position). I took the base sources of all 27 files, rewrote directProductInput to BitString.block and applied the four lemma renames, then diffed the result against the PR head. The only differences left are the ones the body lists:
  • the layout_apply/output_key proof edits;
  • the dropped rfl;
  • the docstring;
  • the restrict_binaryPolynomial move;
  • two tests whose named arguments (k := 4) (n := 2) become (m := 4) (k := 2), which is the same 4 × 2 layout.
• No remaining references, and no collisions. directProductInput appears nowhere on the PR ref, including manual/, results/, ROADMAP.md and AGENT_OPERATORS.md. None of the 70 other open PRs adds it. The new names live in bitonicSortTraceCircuit, Iteration and MassProduction.Pipeline and collide with nothing.
• Migration policy. Removing the name with no alias follows the pre-release no-alias rule in AGENTS.md Proof hygiene.
• Proofs. The KeyedSort.output_key change replaces a terminal simp with simp only, which is fine. The new restrict_binaryPolynomial proof uses simp only in its one non-terminal step.
• Point 3. Leaving max 1 (clog 2 n) unshared is reasonable. binaryFieldDegree and CSP.bitWidth mean different things, and the only shared fact is a two-line bound.
• Manuals. No edit is needed. Neither manual names these declarations, and no workflow changes.

Optional nits for a follow-up, not this PR:

• bitonicSortTraceCircuit.flatten and Iteration.pack are definitionally BitString.blocksEquiv.symm, possibly composed with encode. So block_flatten and flatten_block restate block_blocksEquiv_symm and blocksEquiv.apply_symm_apply. This predates this PR.
• CSP.le_two_pow_bitWidth could use the one-line proof of le_two_pow_binaryFieldDegree.

ci-checks was still pending when I reviewed, so I rely on CI for warnings (#4523), and queue_pr.py waits for it. Agent review, not human review.