Circuit-level oracle inlining

This module exposes the exact semantics and gate accounting for extending an adaptive history by one answer from a fixed-width oracle circuit.

@[simp]

theorem Complexity.Circuit.eval_appendOracleAnswer {inputWidth historyWidth queryWidth historyGates queryGates oracleGates : ℕ} [NeZero inputWidth] [NeZero historyWidth] [NeZero queryWidth] (history : Circuit Basis.andOr2 inputWidth historyWidth historyGates) (query : Circuit Basis.andOr2 historyWidth queryWidth queryGates) (oracle : Circuit Basis.andOr2 queryWidth 1 oracleGates) (input : BitString inputWidth) : (history.appendOracleAnswer query oracle).eval input = Fin.append (history.eval input) (oracle.eval (query.eval (history.eval input)))

One inlining step retains the existing history and appends the oracle circuit's answer to the query computed from that history.

@[simp]

theorem Complexity.Circuit.size_appendOracleAnswer {inputWidth historyWidth queryWidth historyGates queryGates oracleGates : ℕ} [NeZero inputWidth] [NeZero historyWidth] [NeZero queryWidth] (history : Circuit Basis.andOr2 inputWidth historyWidth historyGates) (query : Circuit Basis.andOr2 historyWidth queryWidth queryGates) (oracle : Circuit Basis.andOr2 queryWidth 1 oracleGates) : (history.appendOracleAnswer query oracle).size = history.size + historyWidth + query.size + oracle.size

One inlining step has the source history size, the query and oracle sizes, and one additional historyWidth-gate copy of the retained history.