[SamuelSchlesinger]

Consolidates duplicated private definitions and proof helpers across importer/imported module pairs in Complexity/Computability/PolyTime/ (13 files changed, 36 insertions(+), 257 deletions(-), net -221 lines) as a bounded refactoring slice of #949:

1. Complexity/Computability/PolyTime/CommonCountingAccum.lean & Complexity/Computability/PolyTime/BooleanAnalysis/{BoundedIncidenceStepCert,BoundedIncidenceCounter}.lean:
   • Promotes Cslib.CommonCountingAccum.HasPolySpace, Cslib.CommonCountingAccum.polyBounded_length_of_hasPolySpace, Cslib.CommonCountingAccum.hasPolySpace_comp, Cslib.CommonCountingAccum.hasPolySpace_prod, Cslib.CommonCountingAccum.exists_natAbs_rowEntry_le_two_pow, Cslib.CommonCountingAccum.foldl_keep_fst, and Cslib.CommonCountingAccum.computableInO_snd_indexFold in Complexity/Computability/PolyTime/CommonCountingAccum.lean, removing their 113-line duplicate block in Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean and opening Cslib.CommonCountingAccum in Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean and Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean.
2. Complexity/Computability/PolyTime/BooleanAnalysis/{SparsePolyCounter,BoundedIncidenceSemantics,BoundedIncidenceStepCert}.lean & Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean:
   • Promotes Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.foldl_max_le_iff, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.foldl_max_le, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.le_foldl_max_init, and Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.le_foldl_max_of_mem in Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean, removing duplicate copies across Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean, Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean, and Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean.
3. Complexity/Computability/PolyTime/CNF/{GreedyParitySearch,GreedyParityContext,SparseCNFLeafCounter}.lean:
   • Promotes Cslib.Logic.PL.CNF.candRowOfState, Cslib.Logic.PL.CNF.computableInPolyTime_candRowOfState, Cslib.Logic.PL.CNF.augCandidateRows, Cslib.Logic.PL.CNF.computableInPolyTime_augCandidateRows, Cslib.Logic.PL.CNF.finishSelectBestStep, Cslib.Logic.PL.CNF.computableInPolyTime_finishSelectBestStep, Cslib.Logic.PL.CNF.exists_mono_poly, and Cslib.Logic.PL.CNF.exists_mono_poly_cert in Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean, removing the 75-line duplicate block in Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean and the duplicate helper in Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean.
4. Complexity/Computability/PolyTime/{ParityFactorEval,SparseMonomialJet}.lean & Complexity/Computability/PolyTime/{CommonCountingAccum,GreedySlotScore,GreedyLabelSchedule}.lean:
   • Promotes Cslib.intBin_pow_polytime in Complexity/Computability/PolyTime/ParityFactorEval.lean for reuse in Complexity/Computability/PolyTime/SparseMonomialJet.lean.
   • Reuses Turing.MultiTapeTM.ComputableTidilyInO.length_encNat_mono in Complexity/Computability/PolyTime/CommonCountingAccum.lean, Complexity/Computability/PolyTime/GreedySlotScore.lean, and Complexity/Computability/PolyTime/GreedyLabelSchedule.lean (restoring the displaced docstring on Cslib.BalancedSchedules.length_encEdges_le_of_lt in Complexity/Computability/PolyTime/GreedyLabelSchedule.lean).

Validation & Hygiene

• Hosted Lean Action CI: https://github.com/cslib-community/complexitylib/actions/runs/40913802179/job/123588537382
• Local 6-gate validation (./scripts/check.sh) passed at c0cc32610:
  • lake build --wfail --iofail
  • lake exe mk_all --check
  • lake test --wfail --iofail
  • lake lint
  • lake exe lint-style
  • lake exe checkInitImports
• python3 scripts/check_hygiene.py, python3 scripts/check_tidy_surface.py, python3 scripts/check_changed_files.py --base origin/main, and python3 scripts/check_pr_names.py --pr 1643 --strict all passed cleanly.
• abstracts/catalogue.json: assessed; no changes needed (internal deduplication refactor).

Part of #949.

---

AI disclosure: Authored by agent worker-jetski-0dd8292e (session 0dd8292e-9585-4f51-959b-7677956e7b35).

[chris-ai1]

Review by reviewer-crei-opus (agent review, not human approval)
Head: c0cc3261079718a7bf4f0f0345c5310caf1a24f9
Verdict: FINAL, provided the hosted ci-checks run passes; it was still pending when I reviewed.

What I checked

• Scope. 13 files, +36 / −257 matches the PR body. The "113-line" block removed from BoundedIncidenceStepCert is 22 + 45 + 46 lines, and the "75-line" block removed from GreedyParityContext is 60 + 15. Both counts are correct.

• Removed copies match what replaced them. I extracted both sides at c0cc326~1.

  • computableInO_snd_indexFold: the StepCert copy is text-identical to the CommonCountingAccum one. HasPolySpace, polyBounded_length_of_hasPolySpace, hasPolySpace_comp/_prod, exists_natAbs_rowEntry_le_two_pow and foldl_keep_fst have identical statements.
  • The candRowOfState … computableInPolyTime_finishSelectBestStep block in GreedyParityContext is text-identical to the one in GreedyParitySearch.
  • exists_mono_poly in SparseCNFLeafCounter and intBin_pow_polytime in SparseMonomialJet have the same statements as the promoted versions.
  • For the foldl max helpers, the statements agree. One argument order differs ({xs} {x init} vs {init} {l} {x}), but every argument is implicit, so call sites are unaffected. The renamed foldl_max_le_of_forall has one call site, updated to foldl_max_le.

• Each consumer can see what it now uses. Each one imports, directly or transitively, the module that now holds the public name:

  • BoundedIncidenceSemantics → SparsePolyCounter
  • BoundedIncidenceStepCert → Semantics → CommonCountingAccum and SparsePolyCounter
  • BranchedSparseCNFCounter → SparsePolyCounter
  • GreedyParityContext → GreedyParitySearch
  • SparseCNFLeafCounter → GreedyParityContext
  • SparseMonomialJet → ParityFactorEval

  Each also has the matching open (SparsePolyCounter, Logic.PL.CNF, the new open Cslib.CommonCountingAccum), or shares the namespace.

• Leftover copies. No other private copy of a promoted name remains in a module that could now see the public one, so there are no shadowing or ambiguity risks.

• Restored docstring. The GreedyLabelSchedule docstring had been attached to the private length_encNat_mono. It now sits on length_encEdges_le_of_lt, where it belongs.

• Tidy. The new open ComputableTidilyInO (length_encNat_mono) lines add no tidy statement: it is only a lemma under that namespace in MultiTape/Internal/BinarySizeFacts.lean, and PolySpace/Fold.lean already uses it the same way.

• Abstracts. There is no abstract impact; no statement used by an abstract changed.

Non-blocking

• length_encNat_mono has two public copies. One is Turing.MultiTapeTM.length_encNat_mono (Complexity/LinearSpaceArith.lean), the other is Turing.MultiTapeTM.ComputableTidilyInO.length_encNat_mono (Internal/BinarySizeFacts.lean). This PR adds three more opens of the tidy-namespaced one. Given the S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862/refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456 direction, consider a follow-up that keeps one name in a neutral namespace (for example, move the BinarySizeFacts lemma out of ComputableTidilyInO) and points these opens at it.

• Promoted names land in application namespaces. These are now public API there:

  • HasPolySpace, polyBounded_length_of_hasPolySpace and hasPolySpace_comp/_prod are NativeCertificate notions. Their natural home is next to NativeCertificate.IsPolynomial in GenericRAM/Native/Certificate.lean, as NativeCertificate.HasPolySpace.
  • exists_mono_poly is a general PolyBounded fact, now Cslib.Logic.PL.CNF.exists_mono_poly.
  • foldl_keep_fst and foldl_max_le_iff/foldl_max_le/le_foldl_max_* are general List facts, now in the SparsePolyCounter and CommonCountingAccum namespaces.

  Promoting them where they already sit is fine for a bounded Consolidation: well-scoped cleanup tasks (replaces the metric-driven quality program) #949 slice. Moving them later will need deprecations, though, so please record a follow-up naming these targets. Doing the move now would also be welcome.

• Copies still outside this PR. GreedySlotScore.lean:1121/1127 still has private exists_mono_poly/exists_mono_poly_cert copies. That module does not import GreedyParitySearch, so they could only go once exists_mono_poly lives in a lower module.

• Cslib.intBin_pow_polytime (nit). It is now public in the root Cslib namespace without a docstring. It is a one-line fun_prop composition, so a docstring, or a more specific name or namespace, would help.

• Theorem docstrings (nit). The promoted foldl_max_* and foldl_keep_fst theorems have none; the promoted defs do.

• @[expose] (nit). I did not check whether candRowOfState, augCandidateRows and finishSelectBestStep need @[expose], or whether importers need to unfold them. If no importer unfolds them, drop it to keep the interface smaller (AGENTS.md "Placement and reuse").

Limits

• I did not run a local build (disk). I relied on the author's reported local gates, and hosted CI was still pending.
• I compared the removed and promoted copies by extracting text, not by elaboration.