Implement and formally verify a compact Boolean substitution circuit

A hardware team has a fixed eight-input, sixteen-output substitution function specified by all 256 entries in truth_table.json. Implement that exact function as a combinational Boolean circuit suitable for a backend where nonlinear gates are expensive. The function must not change. No decomposition or existing implementation is supplied.

Deliver circuit.json, Solution.lean and instructions for checking the proof with Lean 4.19.0. The circuit has eight Boolean inputs and sixteen Boolean outputs, both ordered least-significant bit first. It may use only two-input XOR, two-input AND and one-input NOT gates. It must contain no more than 96 AND gates and no more than 490 gates in total. Fanout and wiring are free. Every gate must read only input wires or earlier gate outputs. No lookup tables, multiplexers, conditional expressions, arithmetic primitives, opaque external calls or additional input-dependent state may be counted as free operations.

The JSON schema is specified in circuit_format.txt. Its wire-level semantics, the full target table and the Lean proof interface are fixed in CircuitSpec.lean. Prove that your circuit is well formed, satisfies both gate budgets and computes the specified output for every x : Fin 256. The Lean circuit must be the same circuit as circuit.json, in the same order; the evaluator will compare their data. Deliver a complete kernel-checked proof. Missing proofs, sorry, admitted assumptions, new axioms, unsafe evaluation shortcuts and native_decide are not accepted. Standard logical axioms supplied by Lean are allowed; the final declarations must not depend on sorryAx or Lean.ofReduceBool.

The target has at least one implementation within the declared budgets. You are not asked to establish that 96 AND gates is the global minimum. Any circuit meeting the exact specification and both budgets is a correct answer. There is no preferred architecture or required synthesis algorithm. The difficulty is discovering a sufficiently compact implementation and delivering its formal equivalence proof; a correct table lookup or an oversized truth-table expansion is not a solution.

Place all deliverables in output/. Include any source needed to build the proof, but do not modify CircuitSpec.lean or replace the target function. If you use external synthesis tools, identify their versions in output/tool_versions.txt. The final circuit and proof must be self-contained.

The sixteen output bits represent two byte substitutions of the same input. Synthesize one shared circuit; both budgets apply to the entire circuit, not to each byte independently.
