One Query Operational Protocol
Abstract
Actual preprocessing, one physical ask, paid response writes and postprocessing.
Theorem 1.1 (All-input execution with exactly one ask and a direct quadratic clock).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PhysicalProtocol/ClauseOracleProtocol.one_query_run (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every raw Boolean source word, the actual pre-machine emits the decoded physical query or the valid zero-variable one-empty-clause fallback. The ask relates its whole decoded query to a positive reduced rational whose complex cast equals the full physical trace. That relation contains no satisfying-count premise.
The ask exposes a read-only external stream while ordinary writable response stacks are empty. Each symbol is read into finite control in one transition, then written by the fixed materialization machine in a separate actual transition. A real reversal puts the response on the post input stack. The handoff preserves all those stack contents and changes only the fixed control and label.
The response length is at most twice (L plus one) squared plus L plus five. The complete run uses at most sixteen L squared plus fifty L plus seventy-one transitions. Its final configuration is the exact clean post halt for the canonical binary count. Every complete run has exactly one ask, including malformed sources. The count is over the decoded explicit variable universe; conventional appearing-name word conversion is separate.