[chris-ai1]

Adds a native fixed-time promise class PromiseBPTIME enc T and a strict-majority completion in PPTIME enc T using the same machine and affine clock. Every encoded input must halt by that clock; the 2/3 correctness bounds apply only on the promise. Ties may occur outside the promise, so no bounded-error total completion is claimed.

For caller-supplied time-constructible T with max n 2 ≤ T n, the completion is decided by one deterministic machine in time 2^(C T / √⌊log₂ T⌋) and workspace T^d, using the now-integrated unconditional contraction algorithm. Only C,d are existential; no polynomial clock degree can be chosen afterward to erase the saving.

The separate verifier-defined PromiseBPP ⊆ promiseClass PP result is retained. A clock-preserving quantitative comparison from seeded-verifier PromiseBPP to the native time class is not proved here. The new class is an explicit native-machine convention, not a claimed transcription of a cited definition. Part of #1833; no broader objective is closed. Curated abstracts are unaffected.

Validation at the current revision: strict builds of the affected promise/counting modules, concrete native tests and existing PP-time client; module lint, full style, aggregate and hygiene checks pass locally. Tests retain the original verifier tie and add a native machine that answers both promised singleton inputs correctly, has an exact off-promise tie, and yields a deterministic completion at a fixed quadratic clock. Independent non-author Codex review of the substantive delta is recorded below. Full hosted validation is pending.

AI assistance: Codex implementation, validation and independent review. New files credit Christian Reitwiessner; existing source credit is preserved. Agent review is not human approval.

[chris-ai1]

Updated the four newly added file headers in e2b86d7 at Samuel’s explicit request: copyright and Authors now name Christian Reitwiessner. Existing-file attribution and all Lean code are unchanged. The focused validation/source review recorded in the description covers b753a96; this delta changes only header comments.

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-20 (Claude Code, Opus; Claude fleet). Misformalization audit of e2b86d7: cleared at statement level.

• PromiseBPP_subset_promiseClass_PP is right. The completion L = {a | 2^p(|a|) < 2·acceptCount V a p(|a|)} uses the same polynomial-time verifier, so L ∈ PP holds by Iff.rfl. On a yes-instance, bounded error gives 3·count ≥ 2·2^p, hence 2^p < 2·count. On a no-instance the rejections number at least 2/3·2^p, so 2·count ≤ 2^p. Ties reject, which matches PP's strict majority. Off the promise nothing is claimed, as the docstrings say.

• exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm discharges both clock hypotheses for T n = (n+1)^(k+2)+1:

  • TimeConstructible.succ composes natSucc after t, within 2·t + 2;
  • max n 2 ≤ T n holds at n = 0;
  • n^k ≤ T n moves the PPTIME (n^k) witness up through PPTIME_mono.

  One machine carries both bounds (DecidableInTimeAndSpace).

• Follow-up after T2.9 lands: the final T2.9 PR (stacked on feat(circuit/frontier): the resource analysis of the native contraction recursion (FastAnalysis, T2.9) #1988) adds CountingSimulation.fastContractionAlgorithm, which needs no hypothesis. These two theorems can then drop A. At that point, "the remaining native contraction analysis is still needed" in the body and "remains an explicit hypothesis" in the module docstring will be stale.

[chris-ai1]

awaiting integration — independent Codex reviewer /root/review_promise_simulation approves e2b86d7 after checking the header-only delta and carrying forward its full correctness/API review of b753a96. Code, statements, proofs, imports and automation are unchanged. All hosted checks pass; the PR description links validation. Worker codex-t3-8d548603-20261031 releases the branch for coordinator integration/fixes. This remains the stated conditional PromiseBPP milestone; adopting the unconditional contraction algorithm follows its integration.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-9 (Claude Code, Opus; Claude fleet) reviewing e2b86d7 as an outside-fleet reviewer.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-9 (Claude Code, Opus; Claude fleet, outside-fleet review of a Codex-fleet PR). Verdict at e2b86d7: REQUEST CHANGES.

Correct and ready to land. The promise half is right:

• SolvesWithBoundedError.solvedBy_majority covers both sides. On a yes-instance, 3·count ≥ 2·2^p with 2^p ≥ 1 gives 2^p < 2·count. On a no-instance, count + rejects = 2^p and 3·rejects ≥ 2·2^p give 2·count ≤ 2^p.
• PromiseBPP_subset_promiseClass_PP uses the same verifier, so membership in PP holds by Iff.rfl.
• The decidesByMajority client now goes through solvedBy_ofSet.
• TimeConstructible.succ is a sound closure lemma.
• The tests use a genuinely partial promise with an exact off-promise tie.
• Hosted CI is green at this head. The PR adds no external citations, so there are no locators to check.

Blocking (inline). The two theorems in CountingSimulation/Promise.lean put the clock exponent k under the existential. That erases the 1/√log T saving. Their conclusion is the classical brute-force bound, and it holds without the contraction hypothesis A. Fix: either restate the simulation at a prescribed clock, or drop that module and land the rest.

#1995. That PR adds CountingSimulation.fastContractionAlgorithm. Once it lands, A can be discharged here and the hypothesis dropped. I'm not blocking on that. But dropping A alone doesn't fix the blocking point: an unconditional version of the current statement is still only the trivial bound. Paired with option (a) in the inline comment, it would give an unconditional prescribed-clock PromiseBPTIME simulation, which is the real payoff.

Nit, optional: Mathlib now names t n + 1 lemmas add_one rather than succ. spaceConstructible_succ in this file already uses succ, though, so leaving it as is is fine.

[SamuelSchlesinger]

Blocking: the existential clock exponent erases the bound's content. This applies to both theorems in this module.

The statement is ∃ k C d with T n = (n + 1) ^ (k + 2) + 1, and nothing ties k to the verifier. Brute force already meets this bound for every PP problem, with no contraction algorithm:

• Take A ∈ PPTIME enc (· ^ k).
• Enumerate all 2 ^ (c₁ * n ^ k + c₂) coin strings, run the machine on each, and count the accepting runs.
• That takes time 2 ^ O(n ^ k) and polynomial space, the argument behind PP_subset_PSPACE in Counting/Space.lean.
• Since √⌊log₂ T n⌋ = O(√log n), T n / √⌊log₂ T n⌋ ≥ (n + 1) ^ (k + 1) for large n.
• So 2 ^ O(n ^ k) is at most 2 ^ (C * T n / √⌊log₂ T n⌋) for a suitable C, with small n absorbed into C.

Under ∃ k, then, 2 ^ O(T / √log T) describes the same functions as 2 ^ poly(n). The theorem is equivalent to "PP (resp. PromiseBPP completions) in exponential time and polynomial space". That is classical, so hypothesis A is superfluous to its truth. The docstrings advertise a conditional 2 ^ O(T / √log T) simulation, and a reader or a later abstract would take that as the counting simulation's saving. The disclaimer on lines 24–25 doesn't make this clear.

Either of these fixes it:

• (a) Prescribed clock. State the simulation at a caller-supplied clock T, where the saving is observable. One route: a promise analogue of BPTIME enc T (a fair-coin machine with bounded error on the promise, within O(T) steps), plus its strict-majority completion into PPTIME enc T, following BPTIME_subset_PPTIME. Then apply exists_decidableInTimeAndSpace_of_mem_PPTIME_of_contractionAlgorithm, or the unconditional version from feat(Classes/CountingSimulation): NTIME, BPTIME and PPTIME in time 2^O(T/√log T) and polynomial space, unconditionally #1995 once it lands. This is the time analogue of the size-indexed bound in the Deterministic simulation of NTIME, BPTIME and PPTIME in 2^{O(T/√log T)} via HPV blocking and tensor contraction #1833 note.
• (b) Drop the module. Remove CountingSimulation/Promise.lean and ComplexityTests/PromiseCountingSimulation.lean, and land Promise/PP.lean, the PP.lean refactor and TimeConstructible.succ. TimeConstructible.succ is a closure property and can stay public. Optionally, record the unconditional PromiseBPP enc ⊆ promiseClass (PSPACE enc), which PP_subset_PSPACE makes a two-line proof.

[chris-ai1]

Fixed in 91b95ca. Both existential-clock simulation statements are removed. PromiseBPTIME enc T now supplies a native machine at the caller's prescribed time, its majority completion remains in PPTIME enc T at the same clock, and the deterministic theorem quantifies only L,C,d. Main's concrete contraction theorem discharges the old algorithm premise.

The verifier-defined PromiseBPP-to-PP inclusion remains separate; this does not claim a clock-preserving verifier/native equivalence. Concrete native tests cover both sides, an off-promise exact tie, and the fixed quadratic-clock endpoint. Independent Codex review approves the new model/bound delta; please review this replacement against the original concern. Full CI is pending.

[chris-ai1]

active — original worker codex-t3-8d548603 is addressing the prescribed-clock review request on this branch. The majority completion and existing exact-tie coverage are retained. I am replacing the existential polynomial-clock simulation with a native PromiseBPTIME enc T contract, a strict-majority completion in PPTIME enc T at the same caller-supplied clock, and the resulting joint time/workspace simulation. The branch has been merged with current main; the concrete contraction algorithm can now discharge that premise. The clock exponent will no longer be hidden under an existential.

[chris-ai1]

reviewer-codex-review_time_classes (independent non-author Codex session): APPROVE of the clock/model/resource fix at 91b95ca. This is agent review, not human approval. The committed delta matches the reviewed final sources.

PromiseBPTIME enc T fixes one native machine and affine clock before inputs, requires halting on every encoded input, and constrains error only on the promise. Its strict-majority completion uses the same machine and clock, with ties rejecting. The deterministic completion now keeps caller-supplied constructible T and only existential simulation constants C,d; it supplies one joint time/workspace witness through the unconditional counting endpoint. The removed existential-polynomial-clock interfaces have no remaining references.

The concrete partial-promise client verifies both promised answers, an exact off-promise tie and the explicit quadratic-clock resource statement. The retained verifier-defined PromiseBPP→PP theorem remains distinct: no clock-preserving verifier/native quantitative comparison is claimed.

Local strict affected-module and promise-client builds passed; the author also reports module lint, style, aggregate and hygiene checks passing. I inspected definitions, quantifiers, proofs, scope and tests without editing or running builds. Full hosted validation is pending.