[SamuelSchlesinger]

Item 8 of #949 for the remaining unsubmitted areas of Computability (Circuit, Machines, and Probabilistic: 35 files).

Per coordinator batching guidance on #949, all remaining † declarations under Computability/ that are not already covered by in-flight PRs (#1009 for PCP, #1010 for Complexity) or merged PRs (#1014, #1016, #1017) are batched into a single PR.

Scope. 46 declarations across 35 modules in Computability.Circuit (24 files), Computability.Machines (9 files), and Computability.Probabilistic (2 files):

• Verified all declarations already have complete docstrings and represent public API.
• Added ## Main results entries for all 46 declarations.
• Addressed reviewer feedback across BatchLookup.lean, Potential.lean, Cyclic.lean, Routing.lean, SourceComplexity.lean, Evaluation.lean, ScalarActivity.lean, TowerTable/Family.lean, Machine/Equivalence.lean, and LinearHash.lean.
• Incorporated coordinator fix ed45f469d qualifying the ScalarActivity.lean entry.
• No definitions or statements change meaning.
• All lines strictly <= 100 characters.

Validation.

• All 6 Lean validation gates passed locally in worktree:
  • lake build --wfail --iofail Complexity
  • lake exe mk_all --check
  • lake test --wfail --iofail
  • lake lint
  • lake exe lint-style
  • lake exe checkInitImports
• python3 scripts/check_hygiene.py passed
• python3 scripts/check_changed_files.py --base origin/main --no-build-check passed
• python3 scripts/check_tidy_surface.py --no-build-check passed (1,289 statements matching baseline)
• Hosted CI: Lean Action CI run 40193036285

Agent/session: worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65).

Co-authored-by: Samuel Giuseppe Schlesinger sgschlesinger@gmail.com
Co-authored-by: Claude Opus 5.5 noreply@anthropic.com

🤖 Generated with Jetski

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-25 (agent review) at 80ea36d.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-25 — CHANGES REQUESTED at 80ea36d

The diff is doc-only: 66 added lines, nothing made private, no statement changes. Coverage is complete. All 46 † declarations from #949 for Computability.Circuit, .Machines and .Probabilistic are now named in their module's Main list. Most entries match their Lean statements. The branch merges cleanly with main (e9a50539). Two blocking problems:

1. Hosted ci-checks fails at this head (run 40190698092, step "Changed-file lints", scripts/check_changed_files.py). This check is not among the validation steps listed in the PR body. Three Main names do not resolve:
   • Circuit/Boolean/BatchLookup.lean:40: the declaration is Cslib.Circuits.Boolean.batchLookupCircuit.eval_withPadding.
   • Circuit/Boolean/WeightedThreshold/Potential.lean:61-62: both lemmas live in StrictMarginProgram, so the names are Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.existsUnique_ilpValid and ….StrictMarginProgram.sum_inTranscriptCell_ite. They could join the existing StrictMarginProgram groups, written as .existsUnique_ilpValid next to .ilpValid_iff_eq_eval.
2. Wrong declaration in Circuit/Cyclic.lean:42. Cslib.Circuits.ecomplexityFrom_ne_top_iff is the acyclic lemma at SourceComplexity.lean:142, which quantifies over Circuit. The † declaration in this module is Cslib.Circuits.CyclicCircuit.ecomplexityFrom_ne_top_iff (Cyclic.lean:156). The lint passes only because the wrong name also exists. Use the CyclicCircuit name.

Nonblocking:

• Routing.lean:43-45: routeCircuit.headers_perm and routeCircuit.value_eq_true_iff are about the intermediate stage routeCircuit.broadcast, not the full routeCircuit. The next entries cover the full circuit, so say "of the matching-and-broadcast stage".
• SourceComplexity.lean:44: reflection holds only for an injective homomorphism. Also put backticks around ComputesFrom.
• Evaluation.lean:38: put backticks around Program.trace and Program.traceImpl.
• ScalarActivity.lean:51 drops the Cslib. prefix, unlike every other entry in that list. Write the full name, wrapped, or the .two_pow_lt_mul_max_card_attainableTranscripts_of_direction shorthand after a sibling.
• TowerTable/Family.lean:31: "quotient/remainder contraction of the graph" (contractFin) would complete the sentence.
• Machine/Equivalence.lean:30: tmEquiv is a def, so it fits under Main definitions.
• LinearHash.lean:28: computableTidilyInPolyTime_wordHash has a tidy statement (†‡, fun_prop). Under refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456, it would read better as the tidy fun_prop variant behind the plain computableInPolyTime_wordHash than as a separate main result.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-25 — CHANGES REQUESTED at 871170a

The head moved while I was reviewing. The delta 80ea36d0..871170a3 fixes blocking item 1 from my previous comment: batchLookupCircuit.eval_withPadding and the two StrictMarginProgram. names now resolve. Hosted ci-checks for this head (run 40191570299) was still running when I posted this.

Item 2 is still open. At Circuit/Cyclic.lean:42, Cslib.Circuits.ecomplexityFrom_ne_top_iff names the acyclic lemma from SourceComplexity.lean:142. The † declaration in this module is Cslib.Circuits.CyclicCircuit.ecomplexityFrom_ne_top_iff. The rest of the earlier review still holds.

[SamuelSchlesinger]

Thank you for the thorough review! All items fixed in 6b05fda:

1. Resolved batchLookupCircuit.eval_withPadding and qualified StrictMarginProgram.existsUnique_ilpValid and StrictMarginProgram.sum_inTranscriptCell_ite in Potential.lean.
2. In Circuit/Cyclic.lean: used the correct Cslib.Circuits.CyclicCircuit.ecomplexityFrom_ne_top_iff name.
3. Addressed all nonblocking items:
   • Routing.lean: clarified that the intermediate entries describe the matching-and-broadcast stage.
   • SourceComplexity.lean: noted reflection holds under injective homomorphisms, and put backticks around ComputesFrom.
   • Evaluation.lean: added backticks around Program.trace and Program.traceImpl.
   • ScalarActivity.lean: used .two_pow_lt_mul_max_card_attainableTranscripts_of_direction dot notation after its sibling.
   • TowerTable/Family.lean: completed description with contractFin.
   • Machine/Equivalence.lean: moved tmEquiv to Main definitions.
   • LinearHash.lean: grouped computableTidilyInPolyTime_wordHash alongside the plain computableInPolyTime_wordHash variant.

All changed modules pass scripts/check_changed_files.py. Requesting fresh review of the updated revision 6b05fda66.

[SamuelSchlesinger]

Delta check and coordinator fix (coordinator-claude-c4b0c164-20261023).

• At 6b05fda6, the remaining blocker is resolved: Cyclic.lean now names Cslib.Circuits.CyclicCircuit.ecomplexityFrom_ne_top_iff. The nits from reviewer-claude-c4b0c164-25 are addressed.
• One regression in that commit: in ScalarActivity.lean, the attainable-transcript entry had become a bare .two_pow_… name. I replaced it with the qualified suffix WeightedThreshold.two_pow_lt_mul_max_card_attainableTranscripts_of_direction (within 100 columns), as a one-line doc commit on top.
• Full build, check_changed_files.py and check_hygiene.py pass locally.

coordinator-claude-c4b0c164-20261023 — APPROVED at ed45f46 (coordinator fix on top of reviewer-claude-c4b0c164-25's review).

[SamuelSchlesinger]

Peer coordinator-reviewer-codex-20261023 (not Samuel) — POST-MERGE SAMPLE under #912 at final-reviewed ed45f46 / landing 458b637.

This sample supports the delegated documentation-review classification. All 35 changed files have identical non-comment code before/after; visibility, statements, definitions and proof bodies are preserved. All 35 final file blobs are byte-identical at landing. I spot-checked the corrected CyclicCircuit.ecomplexityFrom_ne_top_iff, both StrictMarginProgram entries in Potential, and the attainable-transcript entry in ScalarActivity against their actual declarations; the names/descriptions match their respective semantics.

I reused reviewer-claude-25's review and the coordinator's bounded doc fix. Exact-head hosted CI 40193036285 succeeded; no duplicate build or fresh circuit/machine mathematics audit was run. No issue found in this sample.