6.13. QuantumBlockEncoding/UniformlyControlledRy.lean🔗

11 explicit public declarations, in source order.

Definition6.13.1

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/UniformlyControlledRy.lean:34. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.13.1●1 definition

defdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

def QuantumBlockEncoding.primitiveControlAssignment {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (context : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis controls

def QuantumBlockEncoding.primitiveControlAssignment
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (context :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2) :
  QuantumBlockEncoding.PrimitiveBasis
    controls

Definition6.13.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “controlled ry block matrix”. Backend-independent specification: each fixed assignment of the non-target wires owns one exact two-dimensional RY block selected by the control bits.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Backend-independent specification: each fixed assignment of the non-target wires owns one exact two-dimensional RY block selected by the control bits.

Declaration kind. def.

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

Lean code for Definition6.13.2●1 definition

defdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

def QuantumBlockEncoding.controlledRyBlockMatrix {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
    (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.controlledRyBlockMatrix
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    ℂ

Backend-independent specification: each fixed assignment of the non-target
wires owns one exact two-dimensional RY block selected by the control bits.

Theorem6.13.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “controlled ry block matrix apply”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/UniformlyControlledRy.lean:51. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.3●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.controlledRyBlockMatrix_apply {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle)
  (row column : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.controlledRyBlockMatrix wires target distinct
      angles row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire target) row).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire target)
              column).2 then
      QuantumBlockEncoding.standardRyMatrix
        (angles
            (QuantumBlockEncoding.primitiveControlAssignment wires
              target distinct
              ((QuantumBlockEncoding.splitPrimitiveWire target)
                  row).2)).eval
        (row target) (column target)
    else 0

theorem QuantumBlockEncoding.controlledRyBlockMatrix_apply
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle)
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.controlledRyBlockMatrix
      wires target distinct angles row
      column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              row).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              column).2 then
      QuantumBlockEncoding.standardRyMatrix
        (angles
            (QuantumBlockEncoding.primitiveControlAssignment
              wires target distinct
              ((QuantumBlockEncoding.splitPrimitiveWire
                    target)
                  row).2)).eval
        (row target) (column target)
    else 0

Definition6.13.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile uniformly controlled ry”. Reference recursive compiler.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Reference recursive compiler. Controls are consumed from low to high in the supplied control tuple; circuit execution remains chronological.

Declaration kind. def.

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

Lean code for Definition6.13.4●1 definition

defdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

def QuantumBlockEncoding.compileUniformlyControlledRy {qubits : ℕ}
  (controls : ℕ) (wires : Fin controls → Fin qubits)
  (target : Fin qubits) :
  (∀ (control : Fin controls), wires control ≠ target) →
    (QuantumBlockEncoding.PrimitiveBasis controls →
        QuantumBlockEncoding.ExactAngle) →
      QuantumBlockEncoding.PrimitiveCircuit qubits

def QuantumBlockEncoding.compileUniformlyControlledRy
  {qubits : ℕ} (controls : ℕ)
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits) :
  (∀ (control : Fin controls),
      wires control ≠ target) →
    (QuantumBlockEncoding.PrimitiveBasis
          controls →
        QuantumBlockEncoding.ExactAngle) →
      QuantumBlockEncoding.PrimitiveCircuit
        qubits

Reference recursive compiler.  Controls are consumed from low to high in
the supplied control tuple; circuit execution remains chronological.

Definition6.13.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “uniformly controlled ry matrix”. Recursive matrix specification corresponding to the standard multiplexor identity.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Recursive matrix specification corresponding to the standard multiplexor identity. This definition is backend-independent and mentions only exact primitive matrix semantics.

Declaration kind. def.

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

Lean code for Definition6.13.5●1 definition

defdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

def QuantumBlockEncoding.uniformlyControlledRyMatrix {qubits : ℕ}
  (controls : ℕ) (wires : Fin controls → Fin qubits)
  (target : Fin qubits) :
  (∀ (control : Fin controls), wires control ≠ target) →
    (QuantumBlockEncoding.PrimitiveBasis controls →
        QuantumBlockEncoding.ExactAngle) →
      Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
        (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.uniformlyControlledRyMatrix
  {qubits : ℕ} (controls : ℕ)
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits) :
  (∀ (control : Fin controls),
      wires control ≠ target) →
    (QuantumBlockEncoding.PrimitiveBasis
          controls →
        QuantumBlockEncoding.ExactAngle) →
      Matrix
        (QuantumBlockEncoding.PrimitiveBasis
          qubits)
        (QuantumBlockEncoding.PrimitiveBasis
          qubits)
        ℂ

Recursive matrix specification corresponding to the standard multiplexor
identity.  This definition is backend-independent and mentions only exact
primitive matrix semantics.

Theorem6.13.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile uniformly controlled ry eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/UniformlyControlledRy.lean:240. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.6●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_eval
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct angles) =
    QuantumBlockEncoding.uniformlyControlledRyMatrix controls wires
      target distinct angles

theorem QuantumBlockEncoding.compileUniformlyControlledRy_eval
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        angles) =
    QuantumBlockEncoding.uniformlyControlledRyMatrix
      controls wires target distinct
      angles

Theorem6.13.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile uniformly controlled ry eval controlled ry block matrix”; the hypotheses and conclusion in the code panel fix its exact scope. The recursive compiler satisfies the independent block-diagonal specification selected by the computational-basis controls.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The recursive compiler satisfies the independent block-diagonal specification selected by the computational-basis controls.

Declaration kind. theorem.

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

Lean code for Theorem6.13.7●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_eval_controlledRyBlockMatrix
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct angles) =
    QuantumBlockEncoding.controlledRyBlockMatrix wires target distinct
      angles

theorem QuantumBlockEncoding.compileUniformlyControlledRy_eval_controlledRyBlockMatrix
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        angles) =
    QuantumBlockEncoding.controlledRyBlockMatrix
      wires target distinct angles

The recursive compiler satisfies the independent block-diagonal
specification selected by the computational-basis controls.

Theorem6.13.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile uniformly controlled ry ry 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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/UniformlyControlledRy.lean:370. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.8●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_ryCount
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct angles).ryCount =
    2 ^ controls

theorem QuantumBlockEncoding.compileUniformlyControlledRy_ryCount
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        angles).ryCount =
    2 ^ controls

Theorem6.13.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile uniformly controlled ry cx 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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/UniformlyControlledRy.lean:386. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.9●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_cxCount
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct angles).cxCount =
    2 * (2 ^ controls - 1)

theorem QuantumBlockEncoding.compileUniformlyControlledRy_cxCount
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        angles).cxCount =
    2 * (2 ^ controls - 1)

Theorem6.13.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile uniformly controlled ry oracle calls eq zero”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/UniformlyControlledRy.lean:403. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.13.10●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_oracleCalls_eq_zero
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
          target distinct angles).resource.oracleCalls =
    0

theorem QuantumBlockEncoding.compileUniformlyControlledRy_oracleCalls_eq_zero
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy
          controls wires target distinct
          angles).resource.oracleCalls =
    0

Theorem6.13.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile uniformly controlled ry five control counts”; the hypotheses and conclusion in the code panel fix its exact scope. Frozen Robin reference count: five controls require 32 RY and 62 CX.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Frozen Robin reference count: five controls require 32 RY and 62 CX.

Declaration kind. theorem.

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

Lean code for Theorem6.13.11●1 theorem

theoremdefined in QuantumBlockEncoding/UniformlyControlledRy.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_five_control_counts
  {qubits : ℕ} (wires : Fin 5 → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (control : Fin 5), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis 5 →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy 5 wires target
          distinct angles).ryCount =
      32 ∧
    (QuantumBlockEncoding.compileUniformlyControlledRy 5 wires target
          distinct angles).cxCount =
      62

theorem QuantumBlockEncoding.compileUniformlyControlledRy_five_control_counts
  {qubits : ℕ}
  (wires : Fin 5 → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin 5),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        5 →
      QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileUniformlyControlledRy
          5 wires target distinct
          angles).ryCount =
      32 ∧
    (QuantumBlockEncoding.compileUniformlyControlledRy
          5 wires target distinct
          angles).cxCount =
      62

Frozen Robin reference count: five controls require 32 RY and 62 CX.