6.16. QuantumBlockEncoding/PrimitiveDepthBound.lean🔗

5 explicit public declarations, in source order.

Theorem6.16.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “next wire depth le”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/PrimitiveDepthBound.lean:12. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.16.1●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveDepthBound.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth_le {qubits : ℕ}
  (wireDepth : Fin qubits → ℕ) (bound : ℕ)
  (h : ∀ (wire : Fin qubits), wireDepth wire ≤ bound)
  (gate : QuantumBlockEncoding.PrimitiveGate qubits)
  (wire : Fin qubits) :
  QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth wireDepth gate
      wire ≤
    bound + 1

theorem QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth_le
  {qubits : ℕ}
  (wireDepth : Fin qubits → ℕ) (bound : ℕ)
  (h :
    ∀ (wire : Fin qubits),
      wireDepth wire ≤ bound)
  (gate :
    QuantumBlockEncoding.PrimitiveGate
      qubits)
  (wire : Fin qubits) :
  QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth
      wireDepth gate wire ≤
    bound + 1

Theorem6.16.2

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. Each scheduled instruction raises the global upper bound by at most one, from any supplied initial wire-depth profile.

Declaration kind. theorem.

Source: QuantumBlockEncoding/PrimitiveDepthBound.lean:23. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.16.2●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveDepthBound.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.foldl_nextWireDepth_le
  {qubits : ℕ} (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits)
  (wireDepth : Fin qubits → ℕ) (bound : ℕ)
  (h : ∀ (wire : Fin qubits), wireDepth wire ≤ bound)
  (wire : Fin qubits) :
  List.foldl QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth
      wireDepth circuit wire ≤
    bound + List.length circuit

theorem QuantumBlockEncoding.PrimitiveCircuit.foldl_nextWireDepth_le
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits)
  (wireDepth : Fin qubits → ℕ) (bound : ℕ)
  (h :
    ∀ (wire : Fin qubits),
      wireDepth wire ≤ bound)
  (wire : Fin qubits) :
  List.foldl
      QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth
      wireDepth circuit wire ≤
    bound + List.length circuit

Each scheduled instruction raises the global upper bound by at most one,
from any supplied initial wire-depth profile.

Theorem6.16.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “wire depths le gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/PrimitiveDepthBound.lean:35. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.16.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveDepthBound.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.wireDepths_le_gateCount
  {qubits : ℕ} (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits)
  (wire : Fin qubits) : circuit.wireDepths wire ≤ circuit.gateCount

theorem QuantumBlockEncoding.PrimitiveCircuit.wireDepths_le_gateCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits)
  (wire : Fin qubits) :
  circuit.wireDepths wire ≤
    circuit.gateCount

Theorem6.16.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “depth le gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/PrimitiveDepthBound.lean:40. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.16.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveDepthBound.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.depth_le_gateCount {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  circuit.depth ≤ circuit.gateCount

theorem QuantumBlockEncoding.PrimitiveCircuit.depth_le_gateCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  circuit.depth ≤ circuit.gateCount

Theorem6.16.5

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The actual reported resource depth, including scheduling parallelism.

Declaration kind. theorem.

Source: QuantumBlockEncoding/PrimitiveDepthBound.lean:45. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.16.5●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveDepthBound.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.resource_depth_le_gateCount
  {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  circuit.resource.depth ≤ circuit.gateCount

theorem QuantumBlockEncoding.PrimitiveCircuit.resource_depth_le_gateCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  circuit.resource.depth ≤
    circuit.gateCount

The actual reported resource depth, including scheduling parallelism.