Stored Cost Refinement
Exercise LA-213
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Depth is computed by the per-wire scheduling fold, not an assigned serial surrogate
- Gate count is the list length; touched wires determine the pushed layer
- The reported resource depth equals the scheduling depth; this is a layer-count bound, not a runtime claim
- Original derivation from inspected local source; no fresh Lean verification
Question
A primitive quantum circuit is a chronological list of gates, each gate acting on a set of touched wires. A per-wire scheduling fold tracks, for every wire, the earliest layer at which its next gate can be placed: processing a gate pushes every touched wire to one more than the maximum current depth over the gate's touched wires, and leaves untouched wires unchanged. The circuit depth is the maximum over all wires of the final per-wire depths; the gate count is the length of the list. Prove that the circuit depth is at most the gate count, i.e. that scheduling in parallel layers never makes the reported depth exceed the number of gates. Identify the key per-step inequality that drives the induction.
Hint: mathematical route
Prove a primitive circuit's parallel-scheduling depth is at most its gate count via the per-step inequality that one gate raises every wire depth by at most one.
- One gate raises every wire's depth bound by at most one, for touched and untouched wires alike.
- Folding over L gates from the zero profile bounds every wire depth by L.
- The maximum over wires, and the equal reported resource depth, are at most the gate count.
Reference solution
The key per-step fact is: if every wire currently has depth at most some bound, then after processing one gate every wire has depth at most that bound plus one. For a touched wire the new depth is one plus the maximum current depth over the touched wires; since each of those is at most the bound, their maximum is at most the bound, so the new depth is at most bound plus one. For an untouched wire the depth is unchanged, hence at most the bound and so at most bound plus one. Now induct on the gate list to bound the folded profile: starting from the all-zero profile (every wire at most 0), each of the L gates raises the uniform upper bound by at most one, so after the whole circuit every wire has depth at most 0 + L = L, the gate count. Taking the maximum over wires, the circuit depth is at most L. Finally the reported resource depth is defined to equal this scheduling depth, so it too is at most the gate count. This bounds a genuine parallel-scheduling depth, computed by the per-wire fold rather than assigned as a serial surrogate; equality can fail because parallelizable gates on disjoint wires share a layer, making the true depth strictly smaller than the gate count.
Assessment rubric
- State and prove the per-step inequality: one gate raises the uniform depth bound by at most one, covering touched and untouched wires (1 weight)
- Induct from the all-zero profile over the L gates to bound every wire depth by L (1 weight)
- Conclude depth and reported resource depth are at most gate count, noting parallel layers can make it strictly smaller (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/PrimitiveDepthBound.lean
nextWireDepth_le12-19; foldl_nextWireDepth_le23-33; depth_le_gateCount40-42; resource_depth_le_gateCount45-47
Source SHA-256:fd31cfd12a5ed193608b0f666ee1e990981f36b45182fc34dd0fc2db1cf62b16· MIT (repository LICENSE)
Contract: d4a8982dedddd028794f2ff96905c2948c7a22fbfe43263df71554d9308c7772
Item digest: e8d6aac4380e1be63a7428f60ed9f11f343696644445cfb3f1cae3cfe7f2ba36
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.