Lean checks the proposition indexed as “next wire depth le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem nextWireDepth_le {qubits : Nat} (wireDepth : Fin qubits → Nat)
(bound : Nat) (h : ∀ wire, wireDepth wire ≤ bound)
(gate : PrimitiveGate qubits) (wire : Fin qubits) :
nextWireDepth wireDepth gate wire ≤ bound + 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “foldl next wire depth le”; the hypotheses and conclusion in the code panel fix its exact scope. Each scheduled instruction raises the global upper bound by at most one, from any supplied initial wire-depth profile.
theorem foldl_nextWireDepth_le {qubits : Nat} (circuit : PrimitiveCircuit qubits)
(wireDepth : Fin qubits → Nat) (bound : Nat)
(h : ∀ wire, wireDepth wire ≤ bound) :
∀ wire, circuit.foldl nextWireDepth wireDepth wire ≤ bound + circuit.length := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “wire depths le gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem wireDepths_le_gateCount {qubits : Nat} (circuit : PrimitiveCircuit qubits)
(wire : Fin qubits) : circuit.wireDepths wire ≤ circuit.gateCount := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “depth le gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem depth_le_gateCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) :
circuit.depth ≤ circuit.gateCount :=
Finset.sup_le (fun wire _ => wireDepths_le_gateCount circuit wire)
/-- The actual reported resource depth, including scheduling parallelism. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “resource depth le gate count”; the hypotheses and conclusion in the code panel fix its exact scope. The actual reported resource depth, including scheduling parallelism.
theorem resource_depth_le_gateCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) :
circuit.resource.depth ≤ circuit.gateCount :=
depth_le_gateCount circuit
commit-pinned source · Verso Blueprint panel