9.1. QuantumBlockEncoding/CubicAmplitudePrimitive.lean🔗

25 explicit public declarations, in source order.

Definition9.1.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 control wires”. The first two wires are system controls and wire two is the clean signal.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. The first two wires are system controls and wire two is the clean signal.

Declaration kind. def.

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

Lean code for Definition9.1.1●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires :
  Fin 2 → Fin 3

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires :
  Fin 2 → Fin 3

The first two wires are system controls and wire two is the clean signal.

Theorem9.1.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 control wires ne signal”; 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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.2●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
  (wire : Fin 2) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires wire ≠ 2

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
  (wire : Fin 2) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires
      wire ≠
    2

Definition9.1.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 control index”. Decode the two little-endian system controls.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Decode the two little-endian system controls.

Declaration kind. def.

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

Lean code for Definition9.1.3●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex
  (bits : QuantumBlockEncoding.PrimitiveBasis 2) : Fin 4

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      2) :
  Fin 4

Decode the two little-endian system controls.

Theorem9.1.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 amplitude abs le one”; 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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.4●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Amplitude_abs_le_one
  (bits : QuantumBlockEncoding.PrimitiveBasis 2) :
  |↑(QuantumBlockEncoding.CubicStatePreparation.cubicAmplitude 2
          (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex
            bits))| ≤
    1

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Amplitude_abs_le_one
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      2) :
  |↑(QuantumBlockEncoding.CubicStatePreparation.cubicAmplitude
          2
          (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex
            bits))| ≤
    1

Definition9.1.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 angle”. Exact standard-RY angle for the selected cubic amplitude.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Exact standard-RY angle for the selected cubic amplitude.

Declaration kind. def.

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

Lean code for Definition9.1.5●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle
  (bits : QuantumBlockEncoding.PrimitiveBasis 2) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      2) :
  QuantumBlockEncoding.ExactAngle

Exact standard-RY angle for the selected cubic amplitude.

Definition9.1.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive circuit”. Four-way uniformly controlled rotation, compiled to primitive gates.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Four-way uniformly controlled rotation, compiled to primitive gates.

Declaration kind. def.

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

Lean code for Definition9.1.6●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Four-way uniformly controlled rotation, compiled to primitive gates.

Definition9.1.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive program”.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Definition9.1.7●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 3

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 3

Theorem9.1.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive circuit eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact matrix semantics of the emitted gate list.

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

Why it is in this chapter. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Exact matrix semantics of the emitted gate list.

Declaration kind. theorem.

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

Lean code for Theorem9.1.8●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires 2
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires
      2
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle

Exact matrix semantics of the emitted gate list.

Theorem9.1.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive program 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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.9●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires 2
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram =
    QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires
      2
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle

Definition9.1.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 encode bits”. Encode a signal value and a two-qubit system index into three named wires.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Encode a signal value and a two-qubit system index into three named wires.

Declaration kind. def.

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

Lean code for Definition9.1.10●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
  (signal : Fin 2) (system : Fin 4) :
  QuantumBlockEncoding.PrimitiveBasis 3

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
  (signal : Fin 2) (system : Fin 4) :
  QuantumBlockEncoding.PrimitiveBasis 3

Encode a signal value and a two-qubit system index into three named wires.

Theorem9.1.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 encode bits signal”; 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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.11●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits_signal
  (signal : Fin 2) (system : Fin 4) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits signal
      system 2 =
    signal

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits_signal
  (signal : Fin 2) (system : Fin 4) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
      signal system 2 =
    signal

Theorem9.1.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 control index encode”; 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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.12●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex_encode
  (signal : Fin 2) (system : Fin 4) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex
      (QuantumBlockEncoding.primitiveControlAssignment
        QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires 2
        QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
        ((QuantumBlockEncoding.splitPrimitiveWire 2)
            (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
              signal system)).2) =
    system

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex_encode
  (signal : Fin 2) (system : Fin 4) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex
      (QuantumBlockEncoding.primitiveControlAssignment
        QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires
        2
        QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal
        ((QuantumBlockEncoding.splitPrimitiveWire
              2)
            (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
              signal system)).2) =
    system

Theorem9.1.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 encode bits context 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.

Why it is in this chapter. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.13●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits_context_eq_iff
  (leftSignal rightSignal : Fin 2) (left right : Fin 4) :
  ((QuantumBlockEncoding.splitPrimitiveWire 2)
          (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
            leftSignal left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 2)
          (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
            rightSignal right)).2 ↔
    left = right

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits_context_eq_iff
  (leftSignal rightSignal : Fin 2)
  (left right : Fin 4) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            2)
          (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
            leftSignal left)).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            2)
          (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
            rightSignal right)).2 ↔
    left = right

Theorem9.1.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive program clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The primitive program's clean signal block is exactly the cubic diagonal.

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

Why it is in this chapter. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. The primitive program's clean signal block is exactly the cubic diagonal.

Declaration kind. theorem.

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

Lean code for Theorem9.1.14●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_cleanEntry
  (row column : Fin 4) :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits 0 row)
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits 0
        column) =
    ↑(QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator 2
        row column)

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_cleanEntry
  (row column : Fin 4) :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
        0 row)
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits
        0 column) =
    ↑(QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator
        2 row column)

The primitive program's clean signal block is exactly the cubic diagonal.

Definition9.1.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive flat unitary”. Flat little-endian unitary used by the operator-certificate interface.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Flat little-endian unitary used by the operator-certificate interface.

Declaration kind. def.

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

Lean code for Definition9.1.15●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary :
  Matrix (Fin (QuantumBlockEncoding.gridSize 3))
    (Fin (QuantumBlockEncoding.gridSize 3)) ℂ

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize 3))
    (Fin
      (QuantumBlockEncoding.gridSize 3))
    ℂ

Flat little-endian unitary used by the operator-certificate interface.

Theorem9.1.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive flat unitary unitary”; 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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.16●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_unitary :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 3)) ℂ

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_unitary :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 3))
      ℂ

Definition9.1.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive clean index”.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Definition9.1.17●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex
  (system : Fin 4) : Fin (QuantumBlockEncoding.gridSize 3)

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex
  (system : Fin 4) :
  Fin (QuantumBlockEncoding.gridSize 3)

Theorem9.1.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive flat unitary clean 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.

Why it is in this chapter. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Theorem9.1.18●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_cleanBlock
  (row column : Fin 4) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator 2
        row column)

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_cleanBlock
  (row column : Fin 4) :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator
        2 row column)

Definition9.1.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 complex target”.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Definition9.1.19●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ComplexTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℂ
    (QuantumBlockEncoding.gridSize 2) (QuantumBlockEncoding.gridSize 2)

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ComplexTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℂ (QuantumBlockEncoding.gridSize 2)
    (QuantumBlockEncoding.gridSize 2)

Definition9.1.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive presentation”.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Definition9.1.20●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitivePresentation :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitivePresentation :
  QuantumBlockEncoding.Circuit

Definition9.1.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive resource”.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Definition9.1.21●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource :
  QuantumBlockEncoding.Resource

Definition9.1.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive operator candidate”.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

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

Lean code for Definition9.1.22●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℂ 2

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℂ 2

Definition9.1.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cubic n 2 primitive verified block encoding”. Exact unitarity and clean-block promotion for the finite cubic route.

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. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Exact unitarity and clean-block promotion for the finite cubic route.

Declaration kind. def.

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

Lean code for Definition9.1.23●1 definition

defdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℂ 2

def QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℂ 2

Exact unitarity and clean-block promotion for the finite cubic route.

Theorem9.1.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. No opaque oracle survives in the accepted primitive resource row.

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

Why it is in this chapter. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. No opaque oracle survives in the accepted primitive resource row.

Declaration kind. theorem.

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

Lean code for Theorem9.1.24●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_oracleCalls_eq_zero :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource.oracleCalls =
    0

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_oracleCalls_eq_zero :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource.oracleCalls =
    0

No opaque oracle survives in the accepted primitive resource row.

Theorem9.1.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic n 2 primitive resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. Resource ownership is definitional rather than a handwritten tuple.

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

Why it is in this chapter. State-preparation and exact rational Householder developments for the cubic benchmark family.

Technical source note. Resource ownership is definitional rather than a handwritten tuple.

Declaration kind. theorem.

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

Lean code for Theorem9.1.25●1 theorem

theoremdefined in QuantumBlockEncoding/CubicAmplitudePrimitive.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_resource_faithful :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource =
    QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit.resource

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_resource_faithful :
  QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource =
    QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit.resource

Resource ownership is definitional rather than a handwritten tuple.