Psi-Turing 机器：复杂性壁垒和 oracle 分离的有限 introspection
An Exact Rounds-versus-Queries Trade-off for Pointer Chasing, Machine-Checked in Lean 4
AI总结：
本文提出 Psi-Turing 机器，通过引入有限 introspection 接口和信息预算，证明 P^Ψ ≠ NP^Ψ 并建立严格深度层次，同时提供两种独立平台和转换桥梁，以标准化 introspection 接口。
摘要：
我们引入 Psi-Turing 机器（Psi-TM）：配备常深 introspection 接口 ι 和每步显式信息预算 B(d,n)=c d log₂ n 的经典图灵机。通过冻结接口，我们开发了信息论下界工具包：预算计数、Ψ-欺骗和Ψ-法诺，包含 worked examples L_k 和 L_k^phase。我们证明了 oracle 相对分离 P^Ψ ≠ NP^Ψ 和严格深度层次，通过 Anti-Simulation Hook 规则出多项式模拟 ι_k 的多项式调用 ι_{k-1} 的可能性。我们还提出了两个独立平台（Psi 决策树和接口受限电路 IC-AC^0/IC-NC^1）和转换桥梁，将机器、树和电路的界限转换，具有显式的 poly/log 损耗。该模型在 ι 之外保持经典计算能力，但允许关于壁垒（相对化；自然证明和证明复杂性部分/条件进展）的精确 oracle 意识陈述。目标是标准化最小 introspection 接口，具有明确计数的信息预算。
英文摘要：
A deterministic query algorithm with $d$ rounds submits $d$ batches of queries, each chosen from the answers to earlier batches. Canonne and Gur asked for general bounds on the cost of removing rounds. For $k$-step pointer chasing over $k$ tables of $m \geq 2$ entries we determine this cost exactly: for $1 \leq d \leq k$, the least worst-case number of queries with at most $d$ rounds is exactly $(k-d)m+d$, so every round removed costs exactly $m-1$ queries, which is what the naive merging of two consecutive rounds pays. The lower bound uses an adversary that answers every query with the queried index, except at the first unread cell of the chain. The model, the problem and the theorem are formalised in Lean 4 without Mathlib, with no sorry and only the axioms propext and Quot.sound; an exhaustive search confirms the formula for small parameters.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
