Strengthen native time hierarchies with clock and padding arguments #1572

Activity

1. SamuelSchlesinger commented on Oct 29, 2026

   

   SamuelSchlesinger

   on Oct 29, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   Related work at Samuel’s current request: I am implementing #800 on feat/universal-simulation-20261029. The first native improvement separates transition-description, binary input-head, and live-configuration costs, targeting universal_bounds_le with (B + 1)^4 * J^2 in place of (B + 1)^5 * J^3 (B still bounds description, input encoding, and clock digits). A streaming input lookup is also under development. I will preserve your ownership of Hierarchy/Time.lean and avoid changing its public hierarchy statements; necessary compatibility fixes will only weaken the stronger simulator estimate to the existing bound. Once checked, the stronger certificate should let your hierarchy work reduce its simulation exponents. The O(t log t) backend remains the broader #800 objective.
2. SamuelSchlesinger commented on Oct 29, 2026

   

   SamuelSchlesinger

   on Oct 29, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   The simulator improvement is now in PR #1586, with passed focused Lean checks and independent source review; full CI is running. Its grouped time envelope is (B+1)^4 J^2 instead of (B+1)^5 J^3, with B still bounding encoded description, input, and binary-clock lengths. Existing public hierarchy statements were preserved; the changes in Hierarchy/Time.lean only weaken the new estimate to the old envelope. This gives your hierarchy work a concrete stronger native certificate to adopt after integration, while #800’s buffered logarithmic-overhead objective remains open.
3. SamuelSchlesinger commented on Oct 29, 2026

   

   SamuelSchlesinger

   on Oct 29, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   Awaiting coordinator review: #1587 proves the native strict hierarchy for every pair of positive integer polynomial degrees (1 ≤ a < b), including linear versus quadratic time. The PR contains the implementation, exact-source independent agent review, targeted validation, and the remaining scope. Full validation is running in Lean Action CI. This issue stays open for the general logarithmic-gap and noninteger-degree results and the sharp nondeterministic/alternating hierarchies; simulator work in #800 remains separate.
4. orbitingflea

   added a commit that references this issue on Oct 29, 2026

   feat(hierarchy): prove integer polynomial hierarchies by native paddi…

   ...

   5fd9719
5. SamuelSchlesinger commented on Oct 30, 2026

   

   SamuelSchlesinger

   on Oct 30, 2026

   CollaboratorAuthor

   More actions

   triage-claude-e6cf7b0d-2 (Claude Code, Opus): status. #1587 landed the first milestone: the strict hierarchy for integer polynomial degrees 1 ≤ a < b (DTIME_pow_ssubset_DTIME_pow), with the logarithmic-clock separation DTIME_ssubset_DTIME_of_log_clock and native padding. The issue stays open for the remaining targets listed above and in ROADMAP: the general f log f hierarchy (simulator in #800), noninteger degrees and finer logarithmic gaps, and sharp nondeterministic and alternating hierarchies.
6. SamuelSchlesinger commented on Oct 31, 2026

   

   SamuelSchlesinger

   on Oct 31, 2026

   CollaboratorAuthor

   More actions

   worker-claude-e6cf7b0d-ntime-hier (Claude Code, Opus): claiming the nondeterministic time hierarchy milestone, on branch claude/ntime-hierarchy.

   Target: NTIME (n ^ a) ⊂ NTIME (n ^ b) on bit strings for integers 1 ≤ a < b, for the native finite binary NTMs. This mirrors DTIME_pow_ssubset_DTIME_pow. The plan has three steps:

   1. An explicit-time verifier characterization of NTIME (new infrastructure, PR 1).
      • A problem in NTIME t has a verifier that runs in linear time on (instance, certificate) pairs, through the choice table and the linear-time saved-coin replay. Every certificate length of at least c * t n + c works.
      • Conversely, a verifier that runs in time T on pairs, with a certificate length computable in unary, puts the problem in NTIME within O(T + ℓ + n). The machine is a closed fair-coin composition: deterministic preparation, then a small fixed sampler that copies the framed instance and samples the certificate, then the deterministic verifier, all through toNTM. The existing GuessVerify uses the PPT clock compiler, which loses the degree.
   2. A coarse hierarchy by lazy diagonalization (Žák 1983; Arora–Barak §3.2).
      • As in timeDiagonal, each input carries a framed description of a deterministic verifier V, so every description gets its own interval of lengths [l, u].
      • For l ≤ n < u, the diagonal machine guesses a certificate and runs V on (x ++ [false], w) with the universal machine.
      • At n = u, it decides deterministically, by brute force over certificates, whether V accepts the length-l input, and negates the answer.
      • The target is NTIME (n ^ d) ⊂ NTIME (n ^ (K * (d + 1))) for an explicit K.
   3. Native polynomial padding for NTIME, with amplification. Both padding directions follow from step 1. The overlapping-exponent amplification of Hierarchy/Polynomial then reaches every pair of integer degrees.

   Public statements stay in plain computability. The f log f and sharp real-exponent forms stay open under this issue.
7. SamuelSchlesinger commented on Oct 31, 2026

   

   SamuelSchlesinger

   on Oct 31, 2026

   CollaboratorAuthor

   More actions

   worker-claude-e6cf7b0d-ntime-hier (Claude Code, Opus): handoff for the nondeterministic time hierarchy. Step 1 of the plan is in #2025 (head d0d8822e5) and awaits review. The hierarchy itself is not proved yet. I am stopping here, and steps 2–3 are available to the next worker.

   Landed in the PR (infrastructure).

   • setOf_exists_mem_NTIME (guess and verify within explicit time). The certificate length is ℓ : α → ℕ, computed in unary, and it may depend on the instance.
   • exists_verifier_of_mem_NTIME: a linear-time verifier on pairs, accepting every certificate length L ≥ c * t n + c.
   • The fixed sampler MultiTapePTM.pairSampler.

   Step 2: the coarse hierarchy NTIME ((n+1)^d) ⊂ NTIME ((n+1)^(K*d+K)), by lazy diagonalization. Design checked against the source:

   • Inputs are x = frame e ++ pad, as in timeDiagonal, where e describes a deterministic verifier machine on encPair encBits encBits. Each description therefore has its own interval of lengths [l_e, u_e], so no disjoint global intervals are needed.
   • Let Sim(y) := ∃ w, |w| = J(|y|) ∧ universal (decodeDesc e, (encPair encBits encBits (y, w)).map eBit, J'(|y|)) halts with [true]. Then D(x_n) := Sim(x_{n+1}) for l_e ≤ n < u_e, and D(x_{u_e}) := ¬Sim(x_{l_e}).
   • The endpoint is a deterministic brute force over enumList (J l_e), for example with ComputableInO.findWith (BigO/Lists). Choose u_e large enough to pay 2^O(J(l_e)), by a formula testable in O(n).
   • D is setOf_exists_mem_NTIME applied to the verifier F_D(x, w). The certificate length is J(|x|+1), written in unary with TimeConstructible and ComputableInO.natToUnary; its quadratic cost fits inside the coarse gap.
   • For the contradiction, take N deciding L(D) within c (n+1)^d + c. Its verifier from exists_verifier_of_mem_NTIME is a concrete machine, so take its padded description e. The chain is N(x_l) = D(x_l) = N(x_{l+1}) = … = N(x_u) = D(x_u) = ¬N(x_l). This is Arora–Barak's argument: Theorem 3.3 in §3.3 of the January 2007 web draft. The library cites Theorem 3.2 for the 2009 book, and I have not verified that number.
   • Reuse Diagonal.shortDesc, decodeDesc_unframe_frame_append, universal_desc and computableTidilyInO_universal from Hierarchy/Hierarchy.Time. feat(universal): simulate t steps in O(t log t) time (#800) #1852's O(t log t) universal function would shrink K, but the argument does not need it.

   Step 3: padding and amplification to every pair of integer degrees 1 ≤ a < b. Exact degree preservation is not available, because the plain calculus has no linear-time writer for unary polynomial lengths: natToUnary is quadratic, and doubling costs a log factor. The following weaker transfer suffices.

   • NTIME ((n+1)^b) ⊆ NTIME ((n+1)^a) implies NTIME ((n+1)^(b*k)) ⊆ NTIME ((n+1)^(a*(k+1)+1)). Pad to length about 2^((k+1) * size(m+1)).
   • Forward direction: guard (m+1)^(k+1) ≤ |x|, which is quadratic and needs b ≥ 2. The certificate length is if guard then c * 2^(b*k*size(m+1)) + c else 0, via ComputableInO.ite and unary_two_pow.
   • Backward direction: guess and verify with the linear verifier of the padded language, after the rounded writer computableInO_roundedPolynomialPadding.
   • Amplification: for k ≥ 3a, a*(k+3) ≤ b*k, so NTIME (n^(a(k+3))) ⊆ NTIME (n^(a(k+1)+1)) ⊆ NTIME (n^(a(k+2))). Every level therefore collapses to degree a*(3a+2), contradicting step 2 at that degree. This covers a = 1 too.
   • A linear-time unary writer, or binary-to-unary conversion, would recover the exact-degree transfer of Padding/Polynomial. It is optional.

   The real-exponent f(n+1) = o(g(n)) form stays open, as does the alternating hierarchy.
8. SamuelSchlesinger commented on Oct 31, 2026

   

   SamuelSchlesinger

   on Oct 31, 2026

   CollaboratorAuthor

   More actions

   worker-claude-e6cf7b0d-ntime-hier-2 (Claude Code, Opus): claiming step 2 of the handoff above, the coarse nondeterministic hierarchy by lazy diagonalization, on branch claude/ntime-lazy-diagonal (stacked on #2025 by merge). Step 3 (padding and amplification) only if step 2 lands in time.
9. SamuelSchlesinger commented on Oct 31, 2026

   

   SamuelSchlesinger

   on Oct 31, 2026

   CollaboratorAuthor

   More actions

   worker-claude-e6cf7b0d-ntime-hier-2 (Claude Code, Opus): handoff. Step 2 (the coarse hierarchy) is in #2031 (head ba518a6f8, stacked on #2025), awaiting review. I am stopping here; step 3 is available.

   Landed in #2031.

   • NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le: NTIME ((n + 1) ^ d) ⊂ NTIME ((n + 1) ^ e) whenever 6 * d + 14 ≤ e, separated by the explicit lazyDiagonal d (lazyDiagonal_mem_NTIME, lazyDiagonal_notMem_NTIME).
   • exists_computableInO_any_enumList (new Classes/Time/BoundedExists): a polynomial-time test tried on every word of length ℓ x within time 2 ^ O(|x| + ℓ x), by Savitch at depth 1. setOf_exists_mem_PSPACE now shares its edges.
   • Design difference from the source: each padded description w = frame code ++ junk gets its own interval [|frame w|, 2 ^ ((|frame w| + 1) ^ (d + 3)) - 1], and the diagonal runs the linear-time verifiers of feat(Classes/Time): explicit-time verifier characterization of NTIME #2025 rather than NTMs. Arora–Barak's Theorem 3.3 (§3.3, web draft dated 2007-01-08) is checked at the source and is now in references.bib as AroraBarak07, with Zak1983 for the method.

   Step 3: every pair of integer degrees 1 ≤ a < b. The handoff plan above works, with these details.

   • Transfer: for 1 ≤ a, 2 ≤ b and 1 ≤ k, a collapse NTIME ((n + 1) ^ b) ⊆ NTIME ((n + 1) ^ a) gives NTIME ((n + 1) ^ (b * k)) ⊆ NTIME ((n + 1) ^ (a * (k + 1) + 1)).
   • Forward direction: B = {x | ((unframe x).length + 1) ^ (k + 1) ≤ x.length ∧ unframe x ∈ A}, by guess and verify with A's linear verifier. Take the certificate length if guard then c * 2 ^ (b * k * Nat.size (m + 1)) + c else 0, with m = (unframe x).length. The guard exponent must be k + 1, not k: ComputableInO.unary_two_pow costs (N + 1) * 2 ^ N, and the extra log factor must fit under (n + 1) ^ b. Reuse computableInO_polynomialPaddingGuard (k + 1). The unary k * Nat.size (m + 1) writer in BigO/PolynomialPadding is private, so it must be exposed or rederived.
   • Backward direction: pad y to frame y ++ replicate (2 ^ ((k + 1) * Nat.size (|y| + 1))) true with computableInO_roundedPolynomialPadding, which costs O((m + 1) ^ (k + 2)). Then guess and verify with B's linear verifier, with certificate length c * 2 ^ (a * ((k + 1) * Nat.size (m + 1) + 1)) + c. That length is at least c * (|pad y| + 1) ^ a + c, and unary_two_pow writes it within O((m + 1) ^ (a * (k + 1) + 1)). This is where the + 1 in the transfer comes from.
   • Amplification: for k ≥ 3 * a, a * (k + 3) ≤ b * k and a * (k + 1) + 1 ≤ a * (k + 2). So every level a * (k + 3) collapses to a * (k + 2), and by induction everything above collapses to D = a * (3 * a + 2). This contradicts NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le (d := D) (e := a * (3 * a + 2 + j)) for j large. Then n ^ a versus n ^ b follows as in Hierarchy/Polynomial.

   The sharp f (n + 1) = o (g n) form and the alternating hierarchy stay open.
10. SamuelSchlesinger commented on Oct 31, 2026

    

    SamuelSchlesinger

    on Oct 31, 2026

    CollaboratorAuthor

    More actions

    worker-claude-e6cf7b0d-ntime-hier-3 (Claude Code, Opus): claiming step 3 of the handoff above (padding transfer and amplification to NTIME ((n + 1) ^ a) ⊂ NTIME ((n + 1) ^ b) for integers 1 ≤ a < b), on branch claude/ntime-pow-hierarchy, stacked on #2031 by merge.
11. SamuelSchlesinger commented on Oct 31, 2026

    

    SamuelSchlesinger

    on Oct 31, 2026

    CollaboratorAuthor

    More actions

    worker-claude-e6cf7b0d-ntime-hier-3 (Claude Code, Opus): step 3 is in #2036 (head 99d172460), stacked on #2031 by merge and awaiting review. NTIME_pow_ssubset_NTIME_pow proves NTIME (n ^ a) ⊂ NTIME (n ^ b) on bit strings for all integers 1 ≤ a < b, including a = 1. NTIME_succ_pow_ssubset_NTIME_succ_pow is the (n + 1) form. I am stopping here.

    What #2036 adds.

    • The padding directions are public, non-vacuous lemmas: setOf_padded_mem_NTIME and mem_NTIME_of_setOf_padded_mem. The padded language is {x | (|unframe x| + 1) ^ (k + 1) ≤ |x| ∧ unframe x ∈ A}.
    • NTIME_pow_mul_subset_of_subset composes them into the transfer b * k ↦ a * (k + 1) + 1.
    • The amplification is the one in the handoff above: everything collapses to degree a * (3 * a + 2), which contradicts feat(Classes/Hierarchy): coarse nondeterministic time hierarchy by lazy diagonalization #2031 at degree a * (18 * a + 26).
    • Infrastructure: a public unary rounded-power writer, computableInO_unary_roundedPower, which computableInO_roundedPolynomialPadding now reuses, and NTIME_succ_pow_eq.

    Landing order. #2025, then #2031, then #2036. After each parent lands, #2036 needs main merged in before it is queued, because the queue squash-merges.

    Still open under this issue: the sharp f (n + 1) = o (g n) form with real exponents, finer logarithmic gaps, the deterministic f log f hierarchy (#800), and the alternating hierarchy. A degree-exact nondeterministic transfer would need a linear-time unary writer for polynomial lengths; the hierarchy does not need it.
12. orbitingflea

    added 4 commits that reference this issue on Oct 31, 2026

    feat(Classes/Time): explicit-time verifier characterization of NTIME (c…

    ...

    bb6b1c5

    feat(Classes/Hierarchy): coarse nondeterministic time hierarchy by la…

    ...

    f5834e4

    feat(Classes/Hierarchy): nondeterministic time hierarchy at every int…

    ...

    b372d90

    feat(Classes/Hierarchy): nondeterministic exponential time hierarchy …

    ...

    91c5943