Follow-ups from the review of the 2026-11-06 merges #2841

An independent review of the 68 commits merged to main on 2026-11-06 (through 242879e) found no unsound definitions, vacuous headline results, misattributed sources, or sorry/axiom/native_decide. The medium findings were stale documentation, status errors and duplicated proofs; they were fixed in #2831, #2832, #2833, #2834, #2835, #2836 and #2840.

This issue tracks the follow-ups that were too broad for those PRs, plus small deduplications noticed along the way. Items marked (in progress) are being picked up now; the rest are open for anyone.

Duplicate proofs and certificates (in progress)

• Cslib.intBin_pow_polytime (PolyTime/ParityFactorEval.lean) restates the public Turing.MultiTapeTM.ComputableInPolyTime.intBin_pow'. Private copies of the integer add/natCast/pow certificates also remain in ExchangeReplacement.lean, BoundedIncidenceStepCert.lean and IntervalCount/PolyTime.lean.
• computableInPolyTime_{insertSorted,sortDedup,equationVars} in PolyTime/CNF/SparsePolyCompile.lean are duplicated as private bi_* lemmas in BooleanAnalysis/BoundedIncidenceCounter.lean.
• length_frame_append is duplicated in KernelTakeDropUnary.lean and KernelZipTransducer.lean. producerBank_injective is duplicated in RecordProduct/Entry.lean and RecordBoxProduct/Entry.lean.
• PRG/NextBit.lean has a private copy of PMF.bind_uniformOfFintype_update. CollisionResistantToOneWay.lean keeps a private tsum_uniformList_mul_le that belongs beside Cslib.BitString.uniformList_apply_le.

API completion (in progress)

• State the zipFold certificates on (l.zipWithLeft (f p) r).reduceOption and remove Turing.MultiTapeTM.zipFold (refactor(Computability): finish recent frame, option-map and TM2 migrations #2840 added zipFold_eq_zipWithLeft).
• Move FixedPrime.window_mono to Schonhage/Callable/Bounds.lean as a CallableProduct.windowSize monotonicity lemma, and retire FixedPrime/Window.lean.
• Move Paillier.totient_sq and the general ZMod (N ^ 2) lemmas out of the crypto namespace into small Foundations modules.

Placement and design (open)

• The liftNet/liftAdversary simp API lives in UC/DummyAdversary.lean. It would sit better beside UC/Execution.lean, and Machine.closeProgram belongs in the probabilistic-oracle layer.
• factoringGame/FactoringHard (RabinFactoring.lean) accept only Blum-modulus generators. A generic factoring assumption would also serve RSADesc/ModulusDesc.
• Extract the set-partition block-count API and the Finite (Setoid α) instance from SetPartition/JoinMatrix.lean into SetPartition/Basic.lean.
• Add a public IsAddFundamentalDomain ↔ AddSubgroup.op conversion for lattices. It is currently private in Lattice/QuotientMeasure.lean and copied in a test.
• The private degree-calculus encList/encDPi lemmas in TM2/Degree.lean deserve public homes beside their polynomial-time counterparts. natAbs_workTapePos_runFrom_le_of_runsInSpace (WordRAM OfTuring/Space.lean) is a general multi-tape lemma, restricted to Bool without need.
• Arithmetic and Boolean circuit evaluation repeat the same step/evaluation poly-time plumbing (Circuit/Arithmetic/EvaluationTime.lean vs Circuit/Boolean/EvaluationTime.lean).
• FiatShamirNIZK still hides its failure output behind Classical.arbitrary X and [Nonempty X], which refactor(crypto): make Fiat-Shamir reduction failure output explicit #2791 removed from the signature reduction.
• The OT-commitment ideal receipt in CompleteSender.lean is computed by the same expression in both laws. An independent functionality-side receipt would make the coupling meaningful (see doc(crypto): correct Module-LWE, UC and sampling status notes #2831).
• About 270 simp only [... length_encPair ...]; omega sites could use enc_len (refactor(Encodings): close encoded length bounds with enc_len #2224 migrated only some). This overlaps plan(automation): apply the #2184 proof simplifications across the library #2209.

Full per-commit review reports are not public. Each item above names the declarations and files involved.

AI assistance: Jetski coordinator session 83ab9013 (review by independent agents; fixes by Gemini 4 Carbon workers, reviewed by separate agents).