PaperSevenPreparePrimitive.lean🔗

19 explicit public declarations, in source order.

Definition10.19.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven selector high matrix”.

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

Lean code for Definition10.19.1●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix :
  Matrix (Fin 8) (Fin 8) ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix :
  Matrix (Fin 8) (Fin 8) ℂ

Definition10.19.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven selector middle matrix”.

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

Lean code for Definition10.19.2●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix :
  Matrix (Fin 8) (Fin 8) ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix :
  Matrix (Fin 8) (Fin 8) ℂ

Definition10.19.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven selector low matrix”.

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

Lean code for Definition10.19.3●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix :
  Matrix (Fin 8) (Fin 8) ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix :
  Matrix (Fin 8) (Fin 8) ℂ

Theorem10.19.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven selector stages eq prepare”; 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/PaperSevenPreparePrimitive.lean:31. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorStages_eq_prepare :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix *
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix *
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix) =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorStages_eq_prepare :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix *
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix *
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix) =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare

Definition10.19.5

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.19.5●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires :
  Fin 1 → Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires :
  Fin 1 → Fin 8

Theorem10.19.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven middle physical 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/PaperSevenPreparePrimitive.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.19.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires_ne_target
  (wire : Fin 1) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires
      wire ≠
    4

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires_ne_target
  (wire : Fin 1) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires
      wire ≠
    4

Definition10.19.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven low physical 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/PaperSevenPreparePrimitive.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.19.7●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires :
  Fin 2 → Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires :
  Fin 2 → Fin 8

Theorem10.19.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires_ne_target
  (wire : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires wire ≠
    3

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires_ne_target
  (wire : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires
      wire ≠
    3

Theorem10.19.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits_decode
  (bits : QuantumBlockEncoding.PrimitiveBasis 8) (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits bits)
      wire =
    bits ⟨↑wire + 3, ⋯⟩

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits_decode
  (bits :
    QuantumBlockEncoding.PrimitiveBasis 8)
  (wire : Fin 3) :
  QuantumBlockEncoding.primitiveBits3LE
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
        bits)
      wire =
    bits ⟨↑wire + 3, ⋯⟩

Theorem10.19.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenHighContext_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 8) :
  ((QuantumBlockEncoding.splitPrimitiveWire 5) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 5) column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire 2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire 2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits row,
            row 7) =
          (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              column,
            column 7)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenHighContext_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            5)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            5)
          column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire
                2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                2)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              row,
            row 7) =
          (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              column,
            column 7)

Theorem10.19.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenHighPhysical_eval :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.ry 5
        QuantumBlockEncoding.Robin.warmRobinUniformSevenHighAngle) =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenHighPhysical_eval :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.ry
        5
        QuantumBlockEncoding.Robin.warmRobinUniformSevenHighAngle) =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorHighMatrix)

Theorem10.19.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddleContext_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 8) :
  ((QuantumBlockEncoding.splitPrimitiveWire 4) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 4) column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire 1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire 1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits row,
            row 7) =
          (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              column,
            column 7)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddleContext_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            4)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            4)
          column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire
                1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                1)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              row,
            row 7) =
          (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              column,
            column 7)

Theorem10.19.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires
      4
      QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires
      4
      QuantumBlockEncoding.Robin.warmRobinPaperSevenMiddlePhysicalWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorMiddleMatrix)

Theorem10.19.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLowContext_iff
  (row column : QuantumBlockEncoding.PrimitiveBasis 8) :
  ((QuantumBlockEncoding.splitPrimitiveWire 3) row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire 3) column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire 0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire 0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits row,
            row 7) =
          (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              column,
            column 7)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLowContext_iff
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      8) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            3)
          row).2 =
      ((QuantumBlockEncoding.splitPrimitiveWire
            3)
          column).2 ↔
    row 6 = column 6 ∧
      ((QuantumBlockEncoding.splitPrimitiveWire
                0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  row))).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                0)
              (QuantumBlockEncoding.primitiveBits3LE
                (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorBits
                  column))).2 ∧
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              row,
            row 7) =
          (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemBits
              column,
            column 7)

Theorem10.19.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.19.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires 3
      QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenLowAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysical_eval :
  QuantumBlockEncoding.controlledRyBlockMatrix
      QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires
      3
      QuantumBlockEncoding.Robin.warmRobinPaperSevenLowPhysicalWires_ne_target
      QuantumBlockEncoding.Robin.warmRobinUniformSevenLowAngles =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorLowMatrix)

Definition10.19.16

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.19.16●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 8

Theorem10.19.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven selector prepare circuit 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/PaperSevenPreparePrimitive.lean:243. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareCircuit_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareCircuit =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareCircuit_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareCircuit =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

Definition10.19.18

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.19.18●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorUnprepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorUnprepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 8

Theorem10.19.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven selector unprepare circuit 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/PaperSevenPreparePrimitive.lean:273. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorUnprepareCircuit_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorUnprepareCircuit =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (star
        (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare))

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorUnprepareCircuit_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorUnprepareCircuit =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (star
        (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare))