Paid Dense Physical Query Compiler
Abstract
A fixed finite compiler executes dense naming and pays for every transfer into physical query construction.
Theorem 1.1 (Actual complete word execution and independent count).
Proof. Machine-checked in Lean as D5/S0/Computability/DenseQueryCompiler.dense_query_run (✓ std3). ∎
Source. Repository-derived.
Commentary.
The compiler has twenty-three Boolean stacks and fixed finite labels and control. It translates every instruction of the actual dense converter and unary preprocessor. When the dense program finishes, two ordinary transfer loops move the output into the preprocessor input, charging twice the output length plus two transitions. All intermediate source, dictionary, saved, and query stacks are empty at the exact clean halt.
For raw source length L and B equal to L squared plus eight L plus seven, the direct clock is eighty times (L plus one) squared plus four B squared plus twenty-two B plus fifteen. The returned whole word decodes as a physical query for precisely the densely prepared raw clause family. Its ordinary explicit-universe count equals the conventional appearing-name count, which is defined independently of the Hamiltonian and oracle.
Every malformed word reaches the valid zero-variable one-empty-clause query. The same query can follow a valid empty-clause source, so validation follows the decoder rather than equality with the dummy word. The theorem proves query construction and paid ordinary execution; the physical response and distinguished Ask are supplied by the separate physical protocol.
References
- Truth anchor:
D5/S0/Computability/DenseQueryCompiler.dense_query_run - Dependency: D5/S0/Computability/ClausePreprocessorRefinement
- Dependency: D5/S0/Computability/DenseClauseConversion