6.27. QuantumBlockEncoding/SelectedRyTrace.lean🔗

10 explicit public declarations, in source order.

Definition6.27.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “gate”; its constructors are the cases that downstream code must handle.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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. inductive.

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

Lean code for Definition6.27.1●1 definition

inductive(2 constructors, 1 parameter)defined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

inductive QuantumBlockEncoding.SelectedRyTrace.Gate (qubits : ℕ) : Type

inductive QuantumBlockEncoding.SelectedRyTrace.Gate
  (qubits : ℕ) : Type

Constructors

ry {qubits : ℕ} (target : Fin qubits) (coefficient : ℚ) :
  QuantumBlockEncoding.SelectedRyTrace.Gate qubits

cx {qubits : ℕ} (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.SelectedRyTrace.Gate qubits

Definition6.27.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “instantiate”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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. def.

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

Lean code for Definition6.27.2●1 definition

defdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

def QuantumBlockEncoding.SelectedRyTrace.Gate.instantiate {qubits : ℕ}
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.SelectedRyTrace.Gate qubits →
    QuantumBlockEncoding.PrimitiveGate qubits

def QuantumBlockEncoding.SelectedRyTrace.Gate.instantiate
  {qubits : ℕ}
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.SelectedRyTrace.Gate
      qubits →
    QuantumBlockEncoding.PrimitiveGate
      qubits

Definition6.27.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “instantiate”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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. def.

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

Lean code for Definition6.27.3●1 definition

defdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

def QuantumBlockEncoding.SelectedRyTrace.instantiate {qubits : ℕ}
  (angle : QuantumBlockEncoding.ExactAngle)
  (trace : List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits)) :
  QuantumBlockEncoding.PrimitiveCircuit qubits

def QuantumBlockEncoding.SelectedRyTrace.instantiate
  {qubits : ℕ}
  (angle :
    QuantumBlockEncoding.ExactAngle)
  (trace :
    List
      (QuantumBlockEncoding.SelectedRyTrace.Gate
        qubits)) :
  QuantumBlockEncoding.PrimitiveCircuit
    qubits

Definition6.27.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile”. The supplied tuple order is the recursive control order.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. The supplied tuple order is the recursive control order. No dense data-state amplitude table is needed: these coefficients concern only the local controls.

Declaration kind. def.

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

Lean code for Definition6.27.4●1 definition

defdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

def QuantumBlockEncoding.SelectedRyTrace.compile {qubits : ℕ} (controls : ℕ)
  (wires : Fin controls → Fin qubits) (target : Fin qubits) :
  (∀ (control : Fin controls), wires control ≠ target) →
    (QuantumBlockEncoding.PrimitiveBasis controls → ℚ) →
      List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits)

def QuantumBlockEncoding.SelectedRyTrace.compile
  {qubits : ℕ} (controls : ℕ)
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits) :
  (∀ (control : Fin controls),
      wires control ≠ target) →
    (QuantumBlockEncoding.PrimitiveBasis
          controls →
        ℚ) →
      List
        (QuantumBlockEncoding.SelectedRyTrace.Gate
          qubits)

The supplied tuple order is the recursive control order. No dense data-state
amplitude table is needed: these coefficients concern only the local controls.

Theorem6.27.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval congr”; 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/SelectedRyTrace.lean:43. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.27.5●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

theorem QuantumBlockEncoding.SelectedRyTrace.eval_congr {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (c : Fin controls), wires c ≠ target)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle)
  (h :
    ∀ (bits : QuantumBlockEncoding.PrimitiveBasis controls),
      (a bits).eval = (b bits).eval) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct a) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct b)

theorem QuantumBlockEncoding.SelectedRyTrace.eval_congr
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (c : Fin controls),
      wires c ≠ target)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle)
  (h :
    ∀
      (bits :
        QuantumBlockEncoding.PrimitiveBasis
          controls),
      (a bits).eval = (b bits).eval) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        a) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct b)

Theorem6.27.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile refines”; 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/SelectedRyTrace.lean:53. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.27.6●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

theorem QuantumBlockEncoding.SelectedRyTrace.compile_refines
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (c : Fin controls), wires c ≠ target)
  (coefficients : QuantumBlockEncoding.PrimitiveBasis controls → ℚ)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate angle
        (QuantumBlockEncoding.SelectedRyTrace.compile controls wires
          target distinct coefficients)) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct fun bits =>
        QuantumBlockEncoding.ExactAngle.scale (coefficients bits) angle)

theorem QuantumBlockEncoding.SelectedRyTrace.compile_refines
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (c : Fin controls),
      wires c ≠ target)
  (coefficients :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      ℚ)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate
        angle
        (QuantumBlockEncoding.SelectedRyTrace.compile
          controls wires target distinct
          coefficients)) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        fun bits =>
        QuantumBlockEncoding.ExactAngle.scale
          (coefficients bits) angle)

Definition6.27.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected”. A selected plane has one coefficient equal to one; all other controls select zero.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. A selected plane has one coefficient equal to one; all other controls select zero.

Declaration kind. def.

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

Lean code for Definition6.27.7●1 definition

defdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

def QuantumBlockEncoding.SelectedRyTrace.selected {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (c : Fin controls), wires c ≠ target)
  (chosen : QuantumBlockEncoding.PrimitiveBasis controls) :
  List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits)

def QuantumBlockEncoding.SelectedRyTrace.selected
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (c : Fin controls),
      wires c ≠ target)
  (chosen :
    QuantumBlockEncoding.PrimitiveBasis
      controls) :
  List
    (QuantumBlockEncoding.SelectedRyTrace.Gate
      qubits)

A selected plane has one coefficient equal to one; all other controls select zero.

Theorem6.27.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected refines”; 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/SelectedRyTrace.lean:95. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.27.8●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

theorem QuantumBlockEncoding.SelectedRyTrace.selected_refines
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (c : Fin controls), wires c ≠ target)
  (chosen : QuantumBlockEncoding.PrimitiveBasis controls)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate angle
        (QuantumBlockEncoding.SelectedRyTrace.selected wires target
          distinct chosen)) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy wires target distinct
        chosen angle)

theorem QuantumBlockEncoding.SelectedRyTrace.selected_refines
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (c : Fin controls),
      wires c ≠ target)
  (chosen :
    QuantumBlockEncoding.PrimitiveBasis
      controls)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate
        angle
        (QuantumBlockEncoding.SelectedRyTrace.selected
          wires target distinct chosen)) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy
        wires target distinct chosen
        angle)

Theorem6.27.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile length”; 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/SelectedRyTrace.lean:105. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.27.9●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

theorem QuantumBlockEncoding.SelectedRyTrace.compile_length
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (c : Fin controls), wires c ≠ target)
  (coefficients : QuantumBlockEncoding.PrimitiveBasis controls → ℚ) :
  (QuantumBlockEncoding.SelectedRyTrace.compile controls wires target
        distinct coefficients).length =
    2 ^ controls + 2 * (2 ^ controls - 1)

theorem QuantumBlockEncoding.SelectedRyTrace.compile_length
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (c : Fin controls),
      wires c ≠ target)
  (coefficients :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      ℚ) :
  (QuantumBlockEncoding.SelectedRyTrace.compile
        controls wires target distinct
        coefficients).length =
    2 ^ controls + 2 * (2 ^ controls - 1)

Theorem6.27.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected 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/SelectedRyTrace.lean:117. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.27.10●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyTrace.lean

complete

theorem QuantumBlockEncoding.SelectedRyTrace.selected_gateCount
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (c : Fin controls), wires c ≠ target)
  (chosen : QuantumBlockEncoding.PrimitiveBasis controls)
  (angle : QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.SelectedRyTrace.instantiate angle
        (QuantumBlockEncoding.SelectedRyTrace.selected wires target
          distinct chosen)).gateCount =
    2 ^ controls + 2 * (2 ^ controls - 1)

theorem QuantumBlockEncoding.SelectedRyTrace.selected_gateCount
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (c : Fin controls),
      wires c ≠ target)
  (chosen :
    QuantumBlockEncoding.PrimitiveBasis
      controls)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.SelectedRyTrace.instantiate
        angle
        (QuantumBlockEncoding.SelectedRyTrace.selected
          wires target distinct
          chosen)).gateCount =
    2 ^ controls + 2 * (2 ^ controls - 1)