SymmetryFourSlotPrimitive.lean🔗

10 explicit public declarations, in source order.

Definition10.29.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair coordinate circuit”. System-wire order is '(p0, p1, sector)'.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. System-wire order is '(p0, p1, sector)'.

Declaration kind. def.

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

Lean code for Definition10.29.1●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

System-wire order is `(p0, p1, sector)`.

Definition10.29.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair coordinate basis equiv”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.29.2●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 3 ≃
    QuantumBlockEncoding.PrimitiveBasis 3

def QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 3 ≃
    QuantumBlockEncoding.PrimitiveBasis 3

Theorem10.29.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair coordinate circuit eval eq”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.29.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit_eval_eq :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit_eval_eq :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv

Definition10.29.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.29.4●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairBits
  (index : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.PrimitiveBasis 3

def QuantumBlockEncoding.Robin.warmRobinPairBits
  (index :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.PrimitiveBasis 3

Definition10.29.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin original bits value”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.29.5●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinOriginalBitsValue
  (state : QuantumBlockEncoding.PrimitiveBasis 3) : ℕ

def QuantumBlockEncoding.Robin.warmRobinOriginalBitsValue
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      3) :
  ℕ

Theorem10.29.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair coordinate circuit image”; the hypotheses and conclusion in the code panel fix its exact scope. The two CX gates implement the non-free pair-coordinate reindex exactly.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. The two CX gates implement the non-free pair-coordinate reindex exactly.

Declaration kind. theorem.

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

Lean code for Theorem10.29.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit_image
  (index : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinOriginalBitsValue
      (QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv
        (QuantumBlockEncoding.Robin.warmRobinPairBits index)) =
    ↑(QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv index)

theorem QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit_image
  (index :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinOriginalBitsValue
      (QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv
        (QuantumBlockEncoding.Robin.warmRobinPairBits
          index)) =
    ↑(QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv
        index)

The two CX gates implement the non-free pair-coordinate reindex exactly.

Theorem10.29.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair coordinate circuit bijective”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.29.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit_bijective :
  Function.Bijective
    ⇑QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv

theorem QuantumBlockEncoding.Robin.warmRobinPairCoordinateCircuit_bijective :
  Function.Bijective
    ⇑QuantumBlockEncoding.Robin.warmRobinPairCoordinateBasisEquiv

Definition10.29.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot exact angle”. Lean-owned exact standard-RY angle for one loader branch.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Lean-owned exact standard-RY angle for one loader branch.

Declaration kind. def.

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

Lean code for Definition10.29.8●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.ExactAngle

Lean-owned exact standard-RY angle for one loader branch.

Theorem10.29.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot exact angle 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.29.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle_eval
  (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  (QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle slot
        column).eval =
    2 *
      Real.arccos
        (QuantumBlockEncoding.Robin.warmRobinFourSlotCoefficient slot
          column)

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle_eval
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  (QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle
        slot column).eval =
    2 *
      Real.arccos
        (QuantumBlockEncoding.Robin.warmRobinFourSlotCoefficient
          slot column)

Theorem10.29.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot exact ry eq rotation”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.29.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotExactRy_eq_rotation
  (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle slot
          column).eval =
    QuantumBlockEncoding.Robin.warmRobinFourSlotRotation slot column

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotExactRy_eq_rotation
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.standardRyMatrix
      (QuantumBlockEncoding.Robin.warmRobinFourSlotExactAngle
          slot column).eval =
    QuantumBlockEncoding.Robin.warmRobinFourSlotRotation
      slot column