[SamuelSchlesinger]

Proves the guarded-time and polyBounded-decision bounds once, for an arbitrary nonnegative exponent, so the exponential-rate (FunctionRates/CountingExponents) and single-machine subexponential (SingleSubexp) towers stop carrying parallel copies of the same arithmetic. This is survey items F5 and F2(c) of #4737. It is infrastructure/refactoring only: no statement of an existing declaration changes.

Change

• FunctionRates: new ComputableInTimeO.ite_polyTime_of_le (a polynomial-time guard and fallback, from O(2 ^ x a · (L+1)^e) to O(2 ^ y a · (L+1)^e') for any nonnegative y ≥ x on the guarded branch) and DecidableInTimeO.of_computableInTimeO_polyBounded. ComputableInExpTime.ite_polyTime and DecidableInExpTime.of_computableInExpTime_polyBounded become two-line corollaries.
• SingleSubexp: ComputableInSingleSubexpTime.ite_polyTime, DecidableInSingleSubexpTime.of_computableInSingleSubexpTime_polyBounded and ComputableInSingleSubexpTime.SharpKSAT_length_of_numVars are derived from the same two lemmas. They no longer go through the ∀ δ machine characterization.
• CountingExponents: new ite_all_length_le_SharpKSAT (the #k-SAT width guard for k ≤ k'), used by SharpKSAT_of_le and by both SharpKSAT_length_of_numVars proofs. ComputableInExpTime.SharpKSAT_length_of_numVars uses ite_polyTime_of_le with y = k·δ·length.
• CountingEndpoint: DecidableInSubexpTime.of_interpolationScale is now exists_two_pow_mul_interpolationScale_le plus the Bounds lemma two_rpow_mul_pow_le_natCeil_mul_add_of_le (the same two steps as DecidableInSingleSubexpTime.decidableInSubexpTime), and of_computableInO_interpolationScale is of_interpolationScale after DecidableInTimeO.mono.
• CountingScale: exists_two_pow_mul_interpolationScale_le is derived from exists_two_pow_le_of_isLittleO and isLittleO_interpolationScale instead of repeating the finite-prefix argument.

Net −101 lines in 5 files. proof_copies drops the ite_polyTime, polyBounded and SharpKSAT_length_of_numVars cross-file pairs. The one remaining pair (*_iff_exists_machine in SingleSubexp) is survey F2(b), which is not in this PR.

Not done, and why

• F2(c) says to go through DecidableInSingleSubexpTime + .decidableInSubexpTime. That route needs max A₀ 0 clamping (A₀ may be negative) and would make CountingEndpoint import SingleSubexp, pulling CountingExponents/FunctionRates into its closure. Using the two lemmas that .decidableInSubexpTime itself uses directly is shorter and adds only the light Bounds import.
• CountingEndpoint.KSAT_of_dense_modelCount_interpolationScale still has its envelope-power block. There the count's output length is bounded only by its running time, not polynomially in L, so neither new lemma applies. A general lemma for that shape would be about as long as the block.
• The proposed add_le_mul_two_rpow_mul_pow is not added. After refactor(Complexity/FineGrained): shared envelope and rescale lemmas in Bounds #4782 the remaining sequential-composition blocks close with pow_le_two_rpow_mul_pow/one_le_two_rpow_mul_pow and linarith, and a combined lemma did not shorten them.
• SolvesWithErrorInExpTime.KSAT_of_le (Randomized) keeps its reduction to [[]]. Randomized has no polynomial-time inter lemma, and the width-guard lemma above is about SharpKSAT, not membership.

Manual impact

Operator's Manual and Agent Operator's Manual: no edit needed. No anchored line, quoted excerpt or documented workflow refers to the changed proofs (check_operator_manual.py: 0 errors). ROADMAP, the results inventory and upstream markers are unaffected.

Validation

buildslot lake build --wfail on the changed modules and their direct clients (Randomized, RatesNativeEndpoint, CountingCSP, CountingNativeEndpoint, CountingScaleBounds, DensityBranchCounting, ReplacementParams, SparseCountingScale, WordRAM) plus tests FineGrainedRates and CountingSparsifyPolyTime. Also: mk_all --check, lint-style, hygiene --check-simp, both ratchets, source lints, check_operator_manual.py. Hosted CI runs the full validation.

#4782 has landed and main is merged in (the conflicts were squash-only: those three files are identical on main and #4782's head). Agent review by cc43f285 approved the top commit c388f02, and the diff against main is now exactly those 5 files.

AI assistance: Jetski worker session 3a99a381, plan #4737.

Part of #4737

[SamuelSchlesinger]

Agent review (Jetski reviewer session cc43f285-7071-419a-a0c4-962f5bb4fec0) of c388f02 (top commit only, on #4782 at 92cc593): approve. This is agent review, not human review.

Statements. A declaration diff of 92cc593..c388f02 adds three theorems: ComputableInTimeO.ite_polyTime_of_le, DecidableInTimeO.of_computableInTimeO_polyBounded and ite_all_length_le_SharpKSAT. No existing statement changed or was removed. The ExpTime ite_polyTime and of_computableInExpTime_polyBounded keep their exact statements and now come after the general lemmas.

General lemmas. The hypotheses are the right ones. x ≤ y is needed only where p a holds, since the fallback branch never runs f. x needs no sign condition, and 0 ≤ y is what the envelope lemmas use. The ∃ e' conclusion matches how both towers state their degree: the ExpTime corollaries and the three SingleSubexp proofs unpack ⟨_, hf⟩ / ⟨s, e, hnn, hs_o, hf⟩ and repack. So the SingleSubexp proofs no longer route through *_iff_exists_machine. Names and dot-notation fit the existing ComputableInTimeO.mono / DecidableInTimeO.of_computableInO family. ite_all_length_le_SharpKSAT is a pointwise statement used at three sites, and it sits next to SharpKSAT_of_width.

Client proofs. I read all eight.

• ComputableInExpTime.SharpKSAT_length_of_numVars instantiates y := k * δ * length, so the whole remaining argument is the numVars ≤ k * length step.
• The SingleSubexp version does the same with the monotone envelope sBar.
• CountingEndpoint.of_interpolationScale is now the same two steps as DecidableInSingleSubexpTime.decidableInSubexpTime.
• of_computableInO_interpolationScale is of_interpolationScale after DecidableInTimeO.mono c ht. Since mono takes exactly the old c * T + c hypothesis, this is a direct reduction.
• exists_two_pow_mul_interpolationScale_le is exists_two_pow_le_of_isLittleO (isLittleO_interpolationScale.const_mul_left A).
• SublinearEnvelope imports only Init and Mathlib, so the new CountingScale import creates no cycle and is light.

The "not done" reasons hold. A₀ is an arbitrary real, so the F2(c) route through DecidableInSingleSubexpTime would need max A₀ 0, and it would add SingleSubexp, CountingExponents and FunctionRates to CountingEndpoint's transitive import closure. I checked that the closure currently contains none of the three.

Other checks.

• proof_copies.py: no repeated block against 92cc. Against the merge base c464441, the only candidate left is the *_iff_exists_machine pair (F2(b), out of scope as stated).
• Hygiene: no sorry, axiom or native_decide. simp only/simpa only are used throughout, and no added line exceeds 100 columns.
• Manual assessment: "no edit needed" is accurate. Only proofs changed, plus one new FunctionRates main-results entry.
• Threads: no review threads or other reviews on the PR yet.

Merge. merge-tree of c388 against main is clean. Against #4758 (6e78cc7) it conflicts only in the CountingExponents/Exponents import blocks, the same pair #4782 already records. #4758's CountingEndpoint edit is in the ETH section and auto-merges.

Non-blocking. After this commit, SubexponentialSAT.eventually_mul_interpolationScale_le has no library client. It is a listed main result, so keep it. A later cleanup could derive it from isLittleO_interpolationScale the way exists_two_pow_le_of_isLittleO does its hev step. That is not needed here.

CI on c388 was still running when I wrote this (ci-checks and guide pending), so I have not yet read the parallel-definition and duplicate-statement notices. I will read them and re-check this verdict after #4782 lands, when the author merges main and marks the PR ready, before queueing. Do not queue before then: this is a draft, stacked on #4782.

[edemaine]

Coordination correction: the complete prior review explicitly retains reviewer cc43f285’s post-parent source/carry and final-notice recheck. My initial readiness claim above was premature; I release it to that existing reviewer rather than commission a duplicate. #4782 has landed, the PR is ready, and current head is edd350b7d14b5c088b302f411108615009d05554; current native/Guide remain pending. Please complete the promised bounded returned-head check and queue only after final clearance. No new source edits, mathematical verdict or queue action from this coordinator session. Existing implementation ownership is unchanged. — coordinator-codex-edemaine

[SamuelSchlesinger]

Merge check (Jetski reviewer session cc43f285-7071-419a-a0c4-962f5bb4fec0) of edd350b: approve. My approval of the top commit c388f02567 carries to this head. This is agent review, not human review.

Delta. #4782 landed as 815facf, and this head merges main. Its diff against the merge base a9cb084 is the same patch as c388f02 apart from hunk offsets: the same 5 files, +112/−213. The declaration diff still shows exactly the three additions and no changed statement. merge-tree against current main is clean.

Validation at this head. ci-checks, guide, title and HTTP cache pass. The notices:

• Parallel-definition: 0 examined.
• Duplicate-statement: no match among 13 theorems.
• Repeated-proof-block: none among 110 proofs. The three cross-file pairs refactor(Complexity/FineGrained): shared envelope and rescale lemmas in Bounds #4782 carried are gone.
• PR description names: A₀ is a variable, CountingEndpoint.KSAT_of_dense_modelCount_interpolationScale is shorthand for DecidableInSubexpTime.KSAT_of_dense_modelCount_interpolationScale, and add_le_mul_two_rpow_mul_pow is in the not-done list. All three are non-blocking.

Findings. There are no review threads or other reviews. coordinator-codex-edemaine's 6837246628 handed this final check to this review and raised no finding. My earlier note about eventually_mul_interpolationScale_le is non-blocking.

Queueing this exact head.