Figure4PreparePrimitive.lean🔗

23 explicit public declarations, in source order.

Definition10.9.1

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “warm robin figure 4 full system”.

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

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

Lean code for Definition10.9.1●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

abbrev QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem : Type

abbrev QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem :
  Type

Definition10.9.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 encode 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/Figure4PreparePrimitive.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.9.2●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4EncodeBits
  (coefficient : Fin 2) (selector : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem) :
  QuantumBlockEncoding.PrimitiveBasis 9

def QuantumBlockEncoding.Robin.warmRobinFigure4EncodeBits
  (coefficient : Fin 2) (selector : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem) :
  QuantumBlockEncoding.PrimitiveBasis 9

Definition10.9.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 bits 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. 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/Figure4PreparePrimitive.lean:30. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.9.3●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
    QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem

def QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
    (Fin 2) (Fin 8)
    QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem

Theorem10.9.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 bits index 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/Figure4PreparePrimitive.lean:35. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex

theorem QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex

Definition10.9.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 bits 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/Figure4PreparePrimitive.lean:39. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.9.5●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem

def QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv :
  QuantumBlockEncoding.PrimitiveBasis 9 ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8)
      QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem

Theorem10.9.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 bits equiv 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. 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/Figure4PreparePrimitive.lean:45. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv_apply
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv bits =
    QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex bits

theorem QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv_apply
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv
      bits =
    QuantumBlockEncoding.Robin.warmRobinFigure4BitsIndex
      bits

Theorem10.9.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 bits equiv 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. 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/Figure4PreparePrimitive.lean:48. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv_encode
  (coefficient : Fin 2) (selector : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4EncodeBits coefficient
        selector system) =
    (coefficient, selector, system)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv_encode
  (coefficient : Fin 2) (selector : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinFigure4FullSystem) :
  QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv
      (QuantumBlockEncoding.Robin.warmRobinFigure4EncodeBits
        coefficient selector system) =
    (coefficient, selector, system)

Definition10.9.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 prepare middle 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. 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/Figure4PreparePrimitive.lean:57. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.9.8●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires :
  Fin 1 → Fin 9

def QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires :
  Fin 1 → Fin 9

Theorem10.9.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare middle wires ne target”; 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/Figure4PreparePrimitive.lean:59. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires_ne_target
  (wire : Fin 1) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires wire ≠ 1

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires_ne_target
  (wire : Fin 1) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires
      wire ≠
    1

Definition10.9.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 prepare low 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. 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/Figure4PreparePrimitive.lean:64. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.9.10●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires :
  Fin 2 → Fin 9

def QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires :
  Fin 2 → Fin 9

Theorem10.9.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare low wires ne target”; 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/Figure4PreparePrimitive.lean:68. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires_ne_target
  (wire : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires wire ≠ 0

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires_ne_target
  (wire : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires
      wire ≠
    0

Theorem10.9.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 selector bits decode”; 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/Figure4PreparePrimitive.lean:72. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SelectorBits_decode
  (bits : QuantumBlockEncoding.PrimitiveBasis 9) (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits bits)
      wire =
    bits ⟨↑wire, ⋯⟩

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SelectorBits_decode
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 9)
  (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
        bits)
      wire =
    bits ⟨↑wire, ⋯⟩

Theorem10.9.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare high context 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. 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/Figure4PreparePrimitive.lean:78. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareHighContext_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 9) :
  ((QuantumBlockEncoding.splitPrimitiveWire 2) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 2) column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire 2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire 2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits row,
            row 7, row 8) =
          (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits column,
            column 7, column 8)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareHighContext_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            2)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            2)
          column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire
                2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              row,
            row 7, row 8) =
          (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              column,
            column 7, column 8)

Theorem10.9.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare high physical 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/Figure4PreparePrimitive.lean:91. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareHighPhysical_eval :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.ry 2
        QuantumBlockEncoding.Robin.warmRobinUniformSevenHighAngle) =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareHighPhysical_eval :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.ry
        2
        QuantumBlockEncoding.Robin.warmRobinUniformSevenHighAngle) =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix)

Theorem10.9.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare middle context 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. 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/Figure4PreparePrimitive.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleContext_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 9) :
  ((QuantumBlockEncoding.splitPrimitiveWire 1) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 1) column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire 1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire 1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits row,
            row 7, row 8) =
          (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits column,
            column 7, column 8)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleContext_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            1)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            1)
          column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire
                1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              row,
            row 7, row 8) =
          (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              column,
            column 7, column 8)

Theorem10.9.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare middle physical 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/Figure4PreparePrimitive.lean:138. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddlePhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires 1
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddlePhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires
      1
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareMiddleWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix)

Theorem10.9.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare low context 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. 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/Figure4PreparePrimitive.lean:184. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowContext_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 9) :
  ((QuantumBlockEncoding.splitPrimitiveWire 0) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 0) column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire 0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire 0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits row,
            row 7, row 8) =
          (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits column,
            column 7, column 8)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowContext_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      9) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            0)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            0)
          column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire
                0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinFigure4AddressBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              row,
            row 7, row 8) =
          (QuantumBlockEncoding.Robin.warmRobinFigure4SystemBits
              column,
            column 7, column 8)

Theorem10.9.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 prepare low physical 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/Figure4PreparePrimitive.lean:197. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.18●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowPhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires 0
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenLowAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowPhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires
      0
      QuantumBlockEncoding.Robin.warmRobinFigure4PrepareLowWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenLowAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix)

Definition10.9.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 selector prepare circuit”.

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

Lean code for Definition10.9.19●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4SelectorPrepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 9

def QuantumBlockEncoding.Robin.warmRobinFigure4SelectorPrepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 9

Definition10.9.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 selector prepare 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. 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/Figure4PreparePrimitive.lean:252. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.9.20●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4SelectorPrepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4SelectorPrepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

Theorem10.9.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 after prepare”; the hypotheses and conclusion in the code panel fix its exact scope. Required stage root: the physical first stage is the exact selector lift.

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. Required stage root: the physical first stage is the exact selector lift.

Declaration kind. theorem.

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

Lean code for Theorem10.9.21●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_after_prepare :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4SelectorPrepareProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_after_prepare :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4SelectorPrepareProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

Required stage root: the physical first stage is the exact selector lift.

Definition10.9.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 selector unprepare 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. 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/Figure4PreparePrimitive.lean:288. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.9.22●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4SelectorUnprepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

def QuantumBlockEncoding.Robin.warmRobinFigure4SelectorUnprepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 9

Theorem10.9.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 after unprepare”; 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/Figure4PreparePrimitive.lean:291. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.9.23●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_after_unprepare :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4SelectorUnprepareProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (star
        (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare))

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_after_unprepare :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinFigure4SelectorUnprepareProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinFigure4BitsEquiv.symm)
      (star
        (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare))