6.26. QuantumBlockEncoding/SelectedRyPlane.lean🔗

25 explicit public declarations, in source order.

Definition6.26.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected ry angles”. One nonzero entry in a multiplexed angle table; all other branches are 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. 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. One nonzero entry in a multiplexed angle table; all other branches are identity.

Declaration kind. def.

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

Lean code for Definition6.26.1●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.selectedRyAngles {controls : ℕ}
  (chosen : QuantumBlockEncoding.PrimitiveBasis controls)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveBasis controls →
    QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.selectedRyAngles
  {controls : ℕ}
  (chosen :
    QuantumBlockEncoding.PrimitiveBasis
      controls)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveBasis
      controls →
    QuantumBlockEncoding.ExactAngle

One nonzero entry in a multiplexed angle table; all other branches are identity.

Definition6.26.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.26.2●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

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

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

Theorem6.26.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile selected ry eval block”; the hypotheses and conclusion in the code panel fix its exact scope. General block version, allowing unused passive wires.

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

Technical source note. General block version, allowing unused passive wires.

Declaration kind. theorem.

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

Lean code for Theorem6.26.3●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRy_eval_block {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (chosen : QuantumBlockEncoding.PrimitiveBasis controls)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy wires target distinct
        chosen angle) =
    QuantumBlockEncoding.controlledRyBlockMatrix wires target distinct
      (QuantumBlockEncoding.selectedRyAngles chosen angle)

theorem QuantumBlockEncoding.compileSelectedRy_eval_block
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (chosen :
    QuantumBlockEncoding.PrimitiveBasis
      controls)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy
        wires target distinct chosen
        angle) =
    QuantumBlockEncoding.controlledRyBlockMatrix
      wires target distinct
      (QuantumBlockEncoding.selectedRyAngles
        chosen angle)

General block version, allowing unused passive wires.

Definition6.26.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “real ry plane block”. The real matrix underlying the standard half-angle RY convention.

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 real matrix underlying the standard half-angle RY convention.

Declaration kind. def.

Source: QuantumBlockEncoding/SelectedRyPlane.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.26.4●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.realRyPlaneBlock (theta : ℝ) :
  Matrix (Fin 2) (Fin 2) ℝ

def QuantumBlockEncoding.realRyPlaneBlock
  (theta : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The real matrix underlying the standard half-angle RY convention.

Theorem6.26.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix eq real ry plane block”; 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/SelectedRyPlane.lean:47. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.26.5●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_eq_realRyPlaneBlock (theta : ℝ)
  (row column : Fin 2) :
  QuantumBlockEncoding.standardRyMatrix theta row column =
    ↑(QuantumBlockEncoding.realRyPlaneBlock theta row column)

theorem QuantumBlockEncoding.standardRyMatrix_eq_realRyPlaneBlock
  (theta : ℝ) (row column : Fin 2) :
  QuantumBlockEncoding.standardRyMatrix
      theta row column =
    ↑(QuantumBlockEncoding.realRyPlaneBlock
        theta row column)

Theorem6.26.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real ry plane block 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.

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

Lean code for Theorem6.26.6●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.realRyPlaneBlock_zero :
  QuantumBlockEncoding.realRyPlaneBlock 0 = 1

theorem QuantumBlockEncoding.realRyPlaneBlock_zero :
  QuantumBlockEncoding.realRyPlaneBlock
      0 =
    1

Definition6.26.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected ry plane matrix”. A real two-level plane: the chosen pair is ordered by target bit 0, then 1.

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 real two-level plane: the chosen pair is ordered by target bit 0, then 1. Every other computational-basis vector is fixed, including its sign.

Declaration kind. def.

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

Lean code for Definition6.26.7●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.selectedRyPlaneMatrix {qubits : ℕ}
  (target : Fin qubits)
  (chosen : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2)
  (theta : ℝ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
    (QuantumBlockEncoding.PrimitiveBasis qubits) ℝ

def QuantumBlockEncoding.selectedRyPlaneMatrix
  {qubits : ℕ} (target : Fin qubits)
  (chosen :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2)
  (theta : ℝ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    ℝ

A real two-level plane: the chosen pair is ordered by target bit 0, then 1.
Every other computational-basis vector is fixed, including its sign.

Theorem6.26.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive control assignment eq iff”; 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/SelectedRyPlane.lean:67. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.26.8●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.primitiveControlAssignment_eq_iff
  {qubits controls : ℕ} (target : Fin qubits)
  (wires :
    Fin controls ≃ QuantumBlockEncoding.OtherPrimitiveWires target)
  (rowContext chosen :
    QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2) :
  (QuantumBlockEncoding.primitiveControlAssignment
        (fun index => ↑(wires index)) target ⋯ rowContext =
      fun index => chosen (wires index)) ↔
    rowContext = chosen

theorem QuantumBlockEncoding.primitiveControlAssignment_eq_iff
  {qubits controls : ℕ}
  (target : Fin qubits)
  (wires :
    Fin controls ≃
      QuantumBlockEncoding.OtherPrimitiveWires
        target)
  (rowContext chosen :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2) :
  (QuantumBlockEncoding.primitiveControlAssignment
        (fun index => ↑(wires index))
        target ⋯ rowContext =
      fun index => chosen (wires index)) ↔
    rowContext = chosen

Theorem6.26.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile selected ry eval plane”; the hypotheses and conclusion in the code panel fix its exact scope. Full-control specialization: an actual finite RY/CX circuit equals the complex embedding of the explicitly real two-level plane.

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

Technical source note. Full-control specialization: an actual finite RY/CX circuit equals the complex embedding of the explicitly real two-level plane.

Declaration kind. theorem.

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

Lean code for Theorem6.26.9●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRy_eval_plane {qubits controls : ℕ}
  (target : Fin qubits)
  (wires :
    Fin controls ≃ QuantumBlockEncoding.OtherPrimitiveWires target)
  (chosen : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy
        (fun index => ↑(wires index)) target ⋯
        (fun index => chosen (wires index)) angle) =
    (QuantumBlockEncoding.selectedRyPlaneMatrix target chosen
          angle.eval).map
      Complex.ofReal

theorem QuantumBlockEncoding.compileSelectedRy_eval_plane
  {qubits controls : ℕ}
  (target : Fin qubits)
  (wires :
    Fin controls ≃
      QuantumBlockEncoding.OtherPrimitiveWires
        target)
  (chosen :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy
        (fun index => ↑(wires index))
        target ⋯
        (fun index =>
          chosen (wires index))
        angle) =
    (QuantumBlockEncoding.selectedRyPlaneMatrix
          target chosen angle.eval).map
      Complex.ofReal

Full-control specialization: an actual finite RY/CX circuit equals the
complex embedding of the explicitly real two-level plane.

Theorem6.26.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected ry plane matrix fixed column”; the hypotheses and conclusion in the code panel fix its exact scope. Entry-level complement statement: no amplitude or phase is changed outside the selected pair.

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

Technical source note. Entry-level complement statement: no amplitude or phase is changed outside the selected pair.

Declaration kind. theorem.

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

Lean code for Theorem6.26.10●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.selectedRyPlaneMatrix_fixed_column {qubits : ℕ}
  (target : Fin qubits)
  (chosen : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2)
  (theta : ℝ) (column : QuantumBlockEncoding.PrimitiveBasis qubits)
  (outside :
    ((QuantumBlockEncoding.splitPrimitiveWire target) column).2 ≠
      chosen)
  (row : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.selectedRyPlaneMatrix target chosen theta row
      column =
    1 row column

theorem QuantumBlockEncoding.selectedRyPlaneMatrix_fixed_column
  {qubits : ℕ} (target : Fin qubits)
  (chosen :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2)
  (theta : ℝ)
  (column :
    QuantumBlockEncoding.PrimitiveBasis
      qubits)
  (outside :
    ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          column).2 ≠
      chosen)
  (row :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.selectedRyPlaneMatrix
      target chosen theta row column =
    1 row column

Entry-level complement statement: no amplitude or phase is changed outside
the selected pair.

Theorem6.26.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.26.11●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.selectedRyPlaneMatrix_selected_entry {qubits : ℕ}
  (target : Fin qubits)
  (chosen : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2)
  (theta : ℝ) (rowBit columnBit : Fin 2) :
  QuantumBlockEncoding.selectedRyPlaneMatrix target chosen theta
      ((QuantumBlockEncoding.splitPrimitiveWire target).symm
        (rowBit, chosen))
      ((QuantumBlockEncoding.splitPrimitiveWire target).symm
        (columnBit, chosen)) =
    QuantumBlockEncoding.realRyPlaneBlock theta rowBit columnBit

theorem QuantumBlockEncoding.selectedRyPlaneMatrix_selected_entry
  {qubits : ℕ} (target : Fin qubits)
  (chosen :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2)
  (theta : ℝ) (rowBit columnBit : Fin 2) :
  QuantumBlockEncoding.selectedRyPlaneMatrix
      target chosen theta
      ((QuantumBlockEncoding.splitPrimitiveWire
            target).symm
        (rowBit, chosen))
      ((QuantumBlockEncoding.splitPrimitiveWire
            target).symm
        (columnBit, chosen)) =
    QuantumBlockEncoding.realRyPlaneBlock
      theta rowBit columnBit

Theorem6.26.12

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.26.12●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRy_ryCount {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits) (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (chosen : QuantumBlockEncoding.PrimitiveBasis controls)
  (angle : QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileSelectedRy wires target distinct chosen
        angle).ryCount =
    2 ^ controls

theorem QuantumBlockEncoding.compileSelectedRy_ryCount
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (chosen :
    QuantumBlockEncoding.PrimitiveBasis
      controls)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.compileSelectedRy
        wires target distinct chosen
        angle).ryCount =
    2 ^ controls

Theorem6.26.13

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.26.13●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

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

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

Definition6.26.14

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “selected ry step”. A proposition-valued field is a requirement until a constructor supplies it. A concrete selected-rotation instruction, not an assumed target operator.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Technical source note. A concrete selected-rotation instruction, not an assumed target operator.

Declaration kind. structure.

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

Lean code for Definition6.26.14●1 definition

structure(5 fields)defined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

structure QuantumBlockEncoding.SelectedRyStep (qubits controls : ℕ) : Type

structure QuantumBlockEncoding.SelectedRyStep
  (qubits controls : ℕ) : Type

A concrete selected-rotation instruction, not an assumed target operator.

Fields

wires : Fin controls → Fin qubits

target : Fin qubits

distinct : ∀ (control : Fin controls), self.wires control ≠ self.target

chosen : QuantumBlockEncoding.PrimitiveBasis controls

angle : QuantumBlockEncoding.ExactAngle

Definition6.26.15

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.26.15●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.SelectedRyStep.compile {qubits controls : ℕ}
  (step : QuantumBlockEncoding.SelectedRyStep qubits controls) :
  QuantumBlockEncoding.PrimitiveCircuit qubits

def QuantumBlockEncoding.SelectedRyStep.compile
  {qubits controls : ℕ}
  (step :
    QuantumBlockEncoding.SelectedRyStep
      qubits controls) :
  QuantumBlockEncoding.PrimitiveCircuit
    qubits

Definition6.26.16

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.26.16●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.SelectedRyStep.matrix {qubits controls : ℕ}
  (step : QuantumBlockEncoding.SelectedRyStep qubits controls) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
    (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.SelectedRyStep.matrix
  {qubits controls : ℕ}
  (step :
    QuantumBlockEncoding.SelectedRyStep
      qubits controls) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    ℂ

Definition6.26.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile selected ry steps”.

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

Lean code for Definition6.26.17●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.compileSelectedRySteps {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls)) :
  QuantumBlockEncoding.PrimitiveCircuit qubits

def QuantumBlockEncoding.compileSelectedRySteps
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls)) :
  QuantumBlockEncoding.PrimitiveCircuit
    qubits

Definition6.26.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected ry steps matrix”. Chronological product: the last listed stage multiplies on the left.

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. Chronological product: the last listed stage multiplies on the left.

Declaration kind. def.

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

Lean code for Definition6.26.18●1 definition

defdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

def QuantumBlockEncoding.selectedRyStepsMatrix {qubits controls : ℕ} :
  List (QuantumBlockEncoding.SelectedRyStep qubits controls) →
    Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
      (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.selectedRyStepsMatrix
  {qubits controls : ℕ} :
  List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls) →
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Chronological product: the last listed stage multiplies on the left.

Theorem6.26.19

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.26.19●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRySteps_eval {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls)) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRySteps steps) =
    QuantumBlockEncoding.selectedRyStepsMatrix steps

theorem QuantumBlockEncoding.compileSelectedRySteps_eval
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls)) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRySteps
        steps) =
    QuantumBlockEncoding.selectedRyStepsMatrix
      steps

Theorem6.26.20

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.26.20●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRySteps_ryCount
  {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps steps).ryCount =
    steps.length * 2 ^ controls

theorem QuantumBlockEncoding.compileSelectedRySteps_ryCount
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps
        steps).ryCount =
    steps.length * 2 ^ controls

Theorem6.26.21

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.26.21●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRySteps_cxCount
  {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps steps).cxCount =
    steps.length * (2 * (2 ^ controls - 1))

theorem QuantumBlockEncoding.compileSelectedRySteps_cxCount
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps
        steps).cxCount =
    steps.length *
      (2 * (2 ^ controls - 1))

Theorem6.26.22

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.26.22●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRySteps_noOracle
  {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps
          steps).resource.oracleCalls =
    0

theorem QuantumBlockEncoding.compileSelectedRySteps_noOracle
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps
          steps).resource.oracleCalls =
    0

Theorem6.26.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.26.23●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileUniformlyControlledRy_gateCount
  {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).gateCount =
    2 ^ controls + 2 * (2 ^ controls - 1)

theorem QuantumBlockEncoding.compileUniformlyControlledRy_gateCount
  {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).gateCount =
    2 ^ controls + 2 * (2 ^ controls - 1)

Theorem6.26.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.26.24●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRySteps_gateCount
  {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps steps).gateCount =
    steps.length * (2 ^ controls + 2 * (2 ^ controls - 1))

theorem QuantumBlockEncoding.compileSelectedRySteps_gateCount
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls)) :
  (QuantumBlockEncoding.compileSelectedRySteps
        steps).gateCount =
    steps.length *
      (2 ^ controls +
        2 * (2 ^ controls - 1))

Theorem6.26.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile selected ry steps cubic bound”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete cubic bound for a supplied finite list.

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

Technical source note. Concrete cubic bound for a supplied finite list. The length hypothesis is the decomposition obligation, not a claim that arbitrary stages already have such decompositions. With 'S = 2^controls', at most 'n (2S)(2S-1)/2' selected planes compile to at most '6 n S^3' primitive gates, with no oracle calls.

Declaration kind. theorem.

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

Lean code for Theorem6.26.25●1 theorem

theoremdefined in QuantumBlockEncoding/SelectedRyPlane.lean

complete

theorem QuantumBlockEncoding.compileSelectedRySteps_cubic_bound
  {qubits controls : ℕ}
  (steps : List (QuantumBlockEncoding.SelectedRyStep qubits controls))
  (stages : ℕ)
  (lengthBound :
    steps.length ≤
      stages * (2 * 2 ^ controls * (2 * 2 ^ controls - 1) / 2)) :
  (QuantumBlockEncoding.compileSelectedRySteps steps).gateCount ≤
      6 * stages * (2 ^ controls) ^ 3 ∧
    (QuantumBlockEncoding.compileSelectedRySteps
            steps).resource.oracleCalls =
      0

theorem QuantumBlockEncoding.compileSelectedRySteps_cubic_bound
  {qubits controls : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.SelectedRyStep
        qubits controls))
  (stages : ℕ)
  (lengthBound :
    steps.length ≤
      stages *
        (2 * 2 ^ controls *
            (2 * 2 ^ controls - 1) /
          2)) :
  (QuantumBlockEncoding.compileSelectedRySteps
          steps).gateCount ≤
      6 * stages * (2 ^ controls) ^ 3 ∧
    (QuantumBlockEncoding.compileSelectedRySteps
            steps).resource.oracleCalls =
      0

Concrete cubic bound for a supplied finite list. The length hypothesis is
the decomposition obligation, not a claim that arbitrary stages already have
such decompositions. With `S = 2^controls`, at most `n (2S)(2S-1)/2` selected
planes compile to at most `6 n S^3` primitive gates, with no oracle calls.