SymmetryFourSlotBlockEncoding.lean🔗

50 explicit public declarations, in source order.

Definition10.27.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair system to original”. Map a reversal-pair coordinate back to the original 'Fin 8' basis.

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. Map a reversal-pair coordinate back to the original 'Fin 8' basis.

Declaration kind. def.

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

Lean code for Definition10.27.1●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
  (index : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
  (index :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  Fin 8

Map a reversal-pair coordinate back to the original `Fin 8` basis.

Theorem10.27.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair system to original zero”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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/SymmetryFourSlotBlockEncoding.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.27.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_zero
  (pair : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal (0, pair) =
    QuantumBlockEncoding.Robin.warmRobinPairLow pair

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_zero
  (pair : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
      (0, pair) =
    QuantumBlockEncoding.Robin.warmRobinPairLow
      pair

Theorem10.27.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair system to original 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. 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/SymmetryFourSlotBlockEncoding.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.27.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_one
  (pair : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal (1, pair) =
    QuantumBlockEncoding.Robin.warmRobinPairHigh pair

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_one
  (pair : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
      (1, pair) =
    QuantumBlockEncoding.Robin.warmRobinPairHigh
      pair

Theorem10.27.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair system to original bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Pair coordinates enumerate the original eight basis states exactly once.

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. Pair coordinates enumerate the original eight basis states exactly once.

Declaration kind. theorem.

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

Lean code for Theorem10.27.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_bijective :
  Function.Bijective
    QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal

Pair coordinates enumerate the original eight basis states exactly once.

Definition10.27.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair system equiv”. Equivalence between pair coordinates and the original Robin basis.

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. Equivalence between pair coordinates and the original Robin basis.

Declaration kind. def.

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

Lean code for Definition10.27.5●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv :
  QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃ Fin 8

def QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv :
  QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    Fin 8

Equivalence between pair coordinates and the original Robin basis.

Theorem10.27.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.27.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv_apply
  (index : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv index =
    QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal index

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv_apply
  (index :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv
      index =
    QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
      index

Theorem10.27.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair system to original symm”; 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/SymmetryFourSlotBlockEncoding.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.27.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_symm
  (system : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
      (QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv.symm
        system) =
    system

theorem QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal_symm
  (system : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPairSystemToOriginal
      (QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv.symm
        system) =
    system

Definition10.27.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry basis change”. The symmetry-sector-to-pair basis change: one exact Hadamard-like rotation.

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 symmetry-sector-to-pair basis change: one exact Hadamard-like rotation.

Declaration kind. def.

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

Lean code for Definition10.27.8●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange :
  Matrix QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℂ

def QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange :
  Matrix
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    ℂ

The symmetry-sector-to-pair basis change: one exact Hadamard-like rotation.

Theorem10.27.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry basis change unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The symmetry basis change is unitary.

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 symmetry basis change is unitary.

Declaration kind. theorem.

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

Lean code for Theorem10.27.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_unitary :
  QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange ∈
    Matrix.unitaryGroup
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℂ

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_unitary :
  QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange ∈
    Matrix.unitaryGroup
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
      ℂ

The symmetry basis change is unitary.

Theorem10.27.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star warm robin uniform bit prepare apply”; the hypotheses and conclusion in the code panel fix its exact scope. Every entry of the real two-dimensional basis change is self-conjugate.

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. Every entry of the real two-dimensional basis change is self-conjugate.

Declaration kind. theorem.

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

Lean code for Theorem10.27.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.star_warmRobinUniformBitPrepare_apply
  (row column : Fin 2) :
  star
      (QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare row
        column) =
    QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare row column

theorem QuantumBlockEncoding.Robin.star_warmRobinUniformBitPrepare_apply
  (row column : Fin 2) :
  star
      (QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
        row column) =
    QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
      row column

Every entry of the real two-dimensional basis change is self-conjugate.

Theorem10.27.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform scalar square complex”; the hypotheses and conclusion in the code panel fix its exact scope. The common real selector amplitude has squared magnitude '1/2'.

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 common real selector amplitude has squared magnitude '1/2'.

Declaration kind. theorem.

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

Lean code for Theorem10.27.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformScalar_square_complex :
  ↑(√2 / 2) * ↑(√2 / 2) = 1 / 2

theorem QuantumBlockEncoding.Robin.warmRobinUniformScalar_square_complex :
  ↑(√2 / 2) * ↑(√2 / 2) = 1 / 2

The common real selector amplitude has squared magnitude `1/2`.

Theorem10.27.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry basis change apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula for the exact symmetry basis change.

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. Entry formula for the exact symmetry basis change.

Declaration kind. theorem.

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

Lean code for Theorem10.27.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_apply
  (row column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange row column =
    if row.2 = column.2 then
      QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare row.1
        column.1
    else 0

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_apply
  (row column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange
      row column =
    if row.2 = column.2 then
      QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
        row.1 column.1
    else 0

Entry formula for the exact symmetry basis change.

Theorem10.27.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star warm robin symmetry basis change apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula for the adjoint symmetry basis change.

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. Entry formula for the adjoint symmetry basis change.

Declaration kind. theorem.

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

Lean code for Theorem10.27.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.star_warmRobinSymmetryBasisChange_apply
  (row column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  star QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange row
      column =
    if row.2 = column.2 then
      star
        (QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare column.1
          row.1)
    else 0

theorem QuantumBlockEncoding.Robin.star_warmRobinSymmetryBasisChange_apply
  (row column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  star
      QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange
      row column =
    if row.2 = column.2 then
      star
        (QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
          column.1 row.1)
    else 0

Entry formula for the adjoint symmetry basis change.

Theorem10.27.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry basis change mul pair row”; the hypotheses and conclusion in the code panel fix its exact scope. Left multiplication preserves the pair index and sums only over sectors.

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. Left multiplication preserves the pair index and sums only over sectors.

Declaration kind. theorem.

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

Lean code for Theorem10.27.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_mul_pairRow.{u_1}
  {columnType : Type u_1} [Fintype columnType]
  (operator :
    Matrix QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem columnType
      ℂ)
  (rowSide : Fin 2) (rowPair : Fin 4) (column : columnType) :
  (QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange * operator)
      (rowSide, rowPair) column =
    ∑ side,
      QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare rowSide
          side *
        operator (side, rowPair) column

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_mul_pairRow.{u_1}
  {columnType : Type u_1}
  [Fintype columnType]
  (operator :
    Matrix
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
      columnType ℂ)
  (rowSide : Fin 2) (rowPair : Fin 4)
  (column : columnType) :
  (QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange *
        operator)
      (rowSide, rowPair) column =
    ∑ side,
      QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
          rowSide side *
        operator (side, rowPair) column

Left multiplication preserves the pair index and sums only over sectors.

Theorem10.27.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mul star warm robin symmetry basis change pair column”; the hypotheses and conclusion in the code panel fix its exact scope. Right multiplication by the adjoint also preserves the pair index.

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. Right multiplication by the adjoint also preserves the pair index.

Declaration kind. theorem.

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

Lean code for Theorem10.27.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.mul_star_warmRobinSymmetryBasisChange_pairColumn.{u_1}
  {rowType : Type u_1} [Fintype rowType]
  (operator :
    Matrix rowType QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℂ)
  (row : rowType) (columnSide : Fin 2) (columnPair : Fin 4) :
  (operator *
        star QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange)
      row (columnSide, columnPair) =
    ∑ side,
      operator row (side, columnPair) *
        star
          (QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
            columnSide side)

theorem QuantumBlockEncoding.Robin.mul_star_warmRobinSymmetryBasisChange_pairColumn.{u_1}
  {rowType : Type u_1} [Fintype rowType]
  (operator :
    Matrix rowType
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
      ℂ)
  (row : rowType) (columnSide : Fin 2)
  (columnPair : Fin 4) :
  (operator *
        star
          QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange)
      row (columnSide, columnPair) =
    ∑ side,
      operator row (side, columnPair) *
        star
          (QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
            columnSide side)

Right multiplication by the adjoint also preserves the pair index.

Theorem10.27.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin integer target pair high low”; the hypotheses and conclusion in the code panel fix its exact scope. Lower-left pair block equals the upper-right pair block by centrosymmetry.

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. Lower-left pair block equals the upper-right pair block by centrosymmetry.

Declaration kind. theorem.

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

Lean code for Theorem10.27.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_pair_high_low
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairHigh row)
      (QuantumBlockEncoding.Robin.warmRobinPairLow column) =
    QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairLow row)
      (QuantumBlockEncoding.Robin.warmRobinPairHigh column)

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_pair_high_low
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairHigh
        row)
      (QuantumBlockEncoding.Robin.warmRobinPairLow
        column) =
    QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairLow
        row)
      (QuantumBlockEncoding.Robin.warmRobinPairHigh
        column)

Lower-left pair block equals the upper-right pair block by centrosymmetry.

Theorem10.27.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin integer target pair high high”; the hypotheses and conclusion in the code panel fix its exact scope. The high-high pair block equals the low-low block.

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 high-high pair block equals the low-low block.

Declaration kind. theorem.

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

Lean code for Theorem10.27.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_pair_high_high
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairHigh row)
      (QuantumBlockEncoding.Robin.warmRobinPairHigh column) =
    QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairLow row)
      (QuantumBlockEncoding.Robin.warmRobinPairLow column)

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_pair_high_high
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairHigh
        row)
      (QuantumBlockEncoding.Robin.warmRobinPairHigh
        column) =
    QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinPairLow
        row)
      (QuantumBlockEncoding.Robin.warmRobinPairLow
        column)

The high-high pair block equals the low-low block.

Definition10.27.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair normalized target rat”. The fixed integer target, reordered by reversal pairs and divided by '224'.

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 fixed integer target, reordered by reversal pairs and divided by '224'.

Declaration kind. def.

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

Lean code for Definition10.27.18●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat :
  Matrix QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℚ

def QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat :
  Matrix
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    ℚ

The fixed integer target, reordered by reversal pairs and divided by `224`.

Theorem10.27.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair normalized target rat zero zero”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem10.27.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_zero_zero
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat (0, row)
      (0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow row)
          (QuantumBlockEncoding.Robin.warmRobinPairLow column)) /
      224

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_zero_zero
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat
      (0, row) (0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow
            row)
          (QuantumBlockEncoding.Robin.warmRobinPairLow
            column)) /
      224

Theorem10.27.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair normalized target rat zero 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. 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/SymmetryFourSlotBlockEncoding.lean:199. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.27.20●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_zero_one
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat (0, row)
      (1, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow row)
          (QuantumBlockEncoding.Robin.warmRobinPairHigh column)) /
      224

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_zero_one
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat
      (0, row) (1, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow
            row)
          (QuantumBlockEncoding.Robin.warmRobinPairHigh
            column)) /
      224

Theorem10.27.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair normalized target rat one zero”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem10.27.21●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_one_zero
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat (1, row)
      (0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow row)
          (QuantumBlockEncoding.Robin.warmRobinPairHigh column)) /
      224

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_one_zero
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat
      (1, row) (0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow
            row)
          (QuantumBlockEncoding.Robin.warmRobinPairHigh
            column)) /
      224

Theorem10.27.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair normalized target rat one 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. 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/SymmetryFourSlotBlockEncoding.lean:216. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.27.22●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_one_one
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat (1, row)
      (1, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow row)
          (QuantumBlockEncoding.Robin.warmRobinPairLow column)) /
      224

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat_one_one
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetRat
      (1, row) (1, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          (QuantumBlockEncoding.Robin.warmRobinPairLow
            row)
          (QuantumBlockEncoding.Robin.warmRobinPairLow
            column)) /
      224

Definition10.27.23

uses 0used by 0✓L∃∀N

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

Technical source note. Complex view of the pair-ordered normalized Robin target.

Declaration kind. def.

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

Lean code for Definition10.27.23●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex :
  Matrix QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℂ

def QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex :
  Matrix
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    ℂ

Complex view of the pair-ordered normalized Robin target.

Definition10.27.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot sector target complex”. Complex view of the direct-sum sector 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Complex view of the direct-sum sector target.

Declaration kind. def.

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

Lean code for Definition10.27.24●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTargetComplex :
  Matrix QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℂ

def QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTargetComplex :
  Matrix
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    ℂ

Complex view of the direct-sum sector target.

Theorem10.27.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry basis change conjugates target”; the hypotheses and conclusion in the code panel fix its exact scope. The exact symmetry transform reconstructs the pair-ordered Robin matrix.

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 exact symmetry transform reconstructs the pair-ordered Robin matrix.

Declaration kind. theorem.

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

Lean code for Theorem10.27.25●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_conjugates_target :
  QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange *
      (QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTargetComplex *
        star QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange) =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange_conjugates_target :
  QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange *
      (QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTargetComplex *
        star
          QuantumBlockEncoding.Robin.warmRobinSymmetryBasisChange) =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex

The exact symmetry transform reconstructs the pair-ordered Robin matrix.

Definition10.27.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot pair logical unitary”. Conjugate the sector logical unitary back to reversal-pair coordinates.

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. Conjugate the sector logical unitary back to reversal-pair coordinates.

Declaration kind. def.

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

Lean code for Definition10.27.26●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    ℂ

def QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    ℂ

Conjugate the sector logical unitary back to reversal-pair coordinates.

Theorem10.27.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot pair logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The pair-basis logical unitary remains exactly unitary.

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 pair-basis logical unitary remains exactly unitary.

Declaration kind. theorem.

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

Lean code for Theorem10.27.27●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
        QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
      ℂ

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        (Fin 2) (Fin 4)
        QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
      ℂ

The pair-basis logical unitary remains exactly unitary.

Theorem10.27.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot pair logical unitary clean system block”; the hypotheses and conclusion in the code panel fix its exact scope. Its clean system block is the pair-ordered normalized Robin target.

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. Its clean system block is the pair-ordered normalized Robin target.

Declaration kind. theorem.

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

Lean code for Theorem10.27.28●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary_cleanSystemBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary 0
      0 =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary_cleanSystemBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary
      0 0 =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex

Its clean system block is the pair-ordered normalized Robin target.

Theorem10.27.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot pair logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entry form of the pair-basis clean-block certificate.

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. Entry form of the pair-basis clean-block certificate.

Declaration kind. theorem.

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

Lean code for Theorem10.27.29●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary_cleanEntry
  (row column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary
      (0, 0, row) (0, 0, column) =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex row
      column

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary_cleanEntry
  (row column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary
      (0, 0, row) (0, 0, column) =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex
      row column

Entry form of the pair-basis clean-block certificate.

Definition10.27.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot product system equiv”. Reindex only the system component from pair order to original 'Fin 8'.

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. Reindex only the system component from pair order to original 'Fin 8'.

Declaration kind. def.

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

Lean code for Definition10.27.30●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotProductSystemEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      (Fin 8)

def QuantumBlockEncoding.Robin.warmRobinFourSlotProductSystemEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4) (Fin 8)

Reindex only the system component from pair order to original `Fin 8`.

Definition10.27.31

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot original index equiv”. Flatten coefficient × selector × original system into six qubits.

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. Flatten coefficient × selector × original system into six qubits.

Declaration kind. def.

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

Lean code for Definition10.27.31●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotOriginalIndexEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      (Fin 8) ≃
    Fin (QuantumBlockEncoding.gridSize 6)

def QuantumBlockEncoding.Robin.warmRobinFourSlotOriginalIndexEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4) (Fin 8) ≃
    Fin (QuantumBlockEncoding.gridSize 6)

Flatten coefficient × selector × original system into six qubits.

Definition10.27.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot product bits equiv”. The six primitive wires interpreted as coefficient, selector, and system registers through the already-certified T2 flattening.

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 six primitive wires interpreted as coefficient, selector, and system registers through the already-certified T2 flattening. Consequently q0--q2 are system, q3--q4 are selector, and q5 is coefficient.

Declaration kind. def.

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

Lean code for Definition10.27.32●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv :
  QuantumBlockEncoding.PrimitiveBasis 6 ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      (Fin 8)

def QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv :
  QuantumBlockEncoding.PrimitiveBasis 6 ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4) (Fin 8)

The six primitive wires interpreted as coefficient, selector, and system
registers through the already-certified T2 flattening.  Consequently q0--q2
are system, q3--q4 are selector, and q5 is coefficient.

Theorem10.27.33

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot product bits equiv index”; the hypotheses and conclusion in the code panel fix its exact scope. Primitive little-endian indexing is exactly the original T2 index map.

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. Primitive little-endian indexing is exactly the original T2 index map.

Declaration kind. theorem.

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

Lean code for Theorem10.27.33●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv_index
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotOriginalIndexEquiv
      (QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv
        bits) =
    (QuantumBlockEncoding.primitiveBasisLEEquiv 6) bits

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv_index
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotOriginalIndexEquiv
      (QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv
        bits) =
    (QuantumBlockEncoding.primitiveBasisLEEquiv
        6)
      bits

Primitive little-endian indexing is exactly the original T2 index map.

Theorem10.27.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot product bits equiv all basis”; the hypotheses and conclusion in the code panel fix its exact scope. Regression over all 64 basis states, stated as the concrete register formula consumed by executable backends.

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. Regression over all 64 basis states, stated as the concrete register formula consumed by executable backends.

Declaration kind. theorem.

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

Lean code for Theorem10.27.34●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv_all_basis
  (bits : QuantumBlockEncoding.PrimitiveBasis 6) :
  ↑(QuantumBlockEncoding.Robin.warmRobinFourSlotOriginalIndexEquiv
        (QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv
          bits)) =
    ↑(bits 0) + 2 * ↑(bits 1) + 4 * ↑(bits 2) + 8 * ↑(bits 3) +
        16 * ↑(bits 4) +
      32 * ↑(bits 5)

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv_all_basis
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      6) :
  ↑(QuantumBlockEncoding.Robin.warmRobinFourSlotOriginalIndexEquiv
        (QuantumBlockEncoding.Robin.warmRobinFourSlotProductBitsEquiv
          bits)) =
    ↑(bits 0) + 2 * ↑(bits 1) +
            4 * ↑(bits 2) +
          8 * ↑(bits 3) +
        16 * ↑(bits 4) +
      32 * ↑(bits 5)

Regression over all 64 basis states, stated as the concrete register
formula consumed by executable backends.

Definition10.27.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot index equiv”. Combined system reindexing and six-qubit flattening.

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. Combined system reindexing and six-qubit flattening.

Declaration kind. def.

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

Lean code for Definition10.27.35●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotIndexEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    Fin (QuantumBlockEncoding.gridSize 6)

def QuantumBlockEncoding.Robin.warmRobinFourSlotIndexEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    Fin (QuantumBlockEncoding.gridSize 6)

Combined system reindexing and six-qubit flattening.

Definition10.27.36

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot clean index”. Flat clean index for an original Robin system basis state.

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. Flat clean index for an original Robin system basis state.

Declaration kind. def.

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

Lean code for Definition10.27.36●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex
  (system : Fin 8) : Fin (QuantumBlockEncoding.gridSize 6)

def QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex
  (system : Fin 8) :
  Fin (QuantumBlockEncoding.gridSize 6)

Flat clean index for an original Robin system basis state.

Definition10.27.37

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot flat unitary”. Six-qubit matrix in the original system order.

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. Six-qubit matrix in the original system order.

Declaration kind. def.

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

Lean code for Definition10.27.37●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary :
  Matrix (Fin (QuantumBlockEncoding.gridSize 6))
    (Fin (QuantumBlockEncoding.gridSize 6)) ℂ

def QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize 6))
    (Fin
      (QuantumBlockEncoding.gridSize 6))
    ℂ

Six-qubit matrix in the original system order.

Theorem10.27.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot flat unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing preserves exact unitarity.

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. Reindexing preserves exact unitarity.

Declaration kind. theorem.

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

Lean code for Theorem10.27.38●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 6)) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 6))
      ℂ

Reindexing preserves exact unitarity.

Theorem10.27.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot flat unitary reindex”; the hypotheses and conclusion in the code panel fix its exact scope. Applying the flat matrix at flattened indices recovers the product entry.

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. Applying the flat matrix at flattened indices recovers the product entry.

Declaration kind. theorem.

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

Lean code for Theorem10.27.39●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary_reindex
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFourSlotIndexEquiv row)
      (QuantumBlockEncoding.Robin.warmRobinFourSlotIndexEquiv column) =
    QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary row
      column

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary_reindex
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFourSlotIndexEquiv
        row)
      (QuantumBlockEncoding.Robin.warmRobinFourSlotIndexEquiv
        column) =
    QuantumBlockEncoding.Robin.warmRobinFourSlotPairLogicalUnitary
      row column

Applying the flat matrix at flattened indices recovers the product entry.

Theorem10.27.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin pair normalized target complex symm”; the hypotheses and conclusion in the code panel fix its exact scope. Pair-ordered target at inverse-reindexed indices is the original target.

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. Pair-ordered target at inverse-reindexed indices is the original target.

Declaration kind. theorem.

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

Lean code for Theorem10.27.40●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex_symm
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex
      (QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv.symm row)
      (QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv.symm
        column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat row column /
        224)

theorem QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex_symm
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex
      (QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv.symm
        row)
      (QuantumBlockEncoding.Robin.warmRobinPairSystemEquiv.symm
        column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat
          row column /
        224)

Pair-ordered target at inverse-reindexed indices is the original target.

Theorem10.27.41

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The flat clean block is exactly the original fixed Robin target.

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 flat clean block is exactly the original fixed Robin target.

Declaration kind. theorem.

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

Lean code for Theorem10.27.41●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex row)
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFourSlotFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

The flat clean block is exactly the original fixed Robin target.

Definition10.27.42

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot t 2 schedule”. Fair T2 logical-stage schedule for the four-slot construction.

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. Fair T2 logical-stage schedule for the four-slot construction.

Declaration kind. def.

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

Lean code for Definition10.27.42●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotT2Schedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.Robin.warmRobinFourSlotT2Schedule :
  QuantumBlockEncoding.LayeredCircuit

Fair T2 logical-stage schedule for the four-slot construction.

Definition10.27.43

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot t 2 circuit”. The corresponding logical gate list.

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 corresponding logical gate list.

Declaration kind. def.

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

Lean code for Definition10.27.43●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotT2Circuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.Robin.warmRobinFourSlotT2Circuit :
  QuantumBlockEncoding.Circuit

The corresponding logical gate list.

Definition10.27.44

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot t 2 resource”. Exact resource row under the declared T2 logical-stage convention.

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. Exact resource row under the declared T2 logical-stage convention.

Declaration kind. def.

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

Lean code for Definition10.27.44●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotT2Resource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Robin.warmRobinFourSlotT2Resource :
  QuantumBlockEncoding.Resource

Exact resource row under the declared T2 logical-stage convention.

Definition10.27.45

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot block contains target”. The operator-first clean-block predicate for the four-slot 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. The operator-first clean-block predicate for the four-slot route.

Declaration kind. def.

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

Lean code for Definition10.27.45●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotBlockContainsTarget : Prop

def QuantumBlockEncoding.Robin.warmRobinFourSlotBlockContainsTarget :
  Prop

The operator-first clean-block predicate for the four-slot route.

Theorem10.27.46

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot block contains target proof”; the hypotheses and conclusion in the code panel fix its exact scope. The clean-block predicate is discharged by the original-basis theorem.

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 clean-block predicate is discharged by the original-basis theorem.

Declaration kind. theorem.

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

Lean code for Theorem10.27.46●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinFourSlotBlockContainsTarget

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinFourSlotBlockContainsTarget

The clean-block predicate is discharged by the original-basis theorem.

Definition10.27.47

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot operator candidate”. Four-slot T2 candidate for the fixed 'N=8' Robin 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Four-slot T2 candidate for the fixed 'N=8' Robin target.

Declaration kind. def.

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

Lean code for Definition10.27.47●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℂ 3

def QuantumBlockEncoding.Robin.warmRobinFourSlotOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℂ 3

Four-slot T2 candidate for the fixed `N=8` Robin target.

Definition10.27.48

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot verified block encoding”. Fully verified T2 block encoding for the four-slot symmetry 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Fully verified T2 block encoding for the four-slot symmetry route.

Declaration kind. def.

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

Lean code for Definition10.27.48●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℂ 3

def QuantumBlockEncoding.Robin.warmRobinFourSlotVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℂ 3

Fully verified T2 block encoding for the four-slot symmetry route.

Theorem10.27.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot t 2 cost better than hadamard 8”; the hypotheses and conclusion in the code panel fix its exact scope. Under one T2 logical-stage convention, four slots strictly improve the Hadamard-8 route: gate count and depth tie, while the clean layout uses one fewer auxiliary qubit.

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. Under one T2 logical-stage convention, four slots strictly improve the Hadamard-8 route: gate count and depth tie, while the clean layout uses one fewer auxiliary qubit.

Declaration kind. theorem.

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

Lean code for Theorem10.27.49●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT2Cost_betterThan_hadamard8 :
  QuantumBlockEncoding.Robin.warmRobinFourSlotOperatorCandidate.cost.betterThan
    QuantumBlockEncoding.Robin.warmRobinHadamard8OperatorCandidate.cost

theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT2Cost_betterThan_hadamard8 :
  QuantumBlockEncoding.Robin.warmRobinFourSlotOperatorCandidate.cost.betterThan
    QuantumBlockEncoding.Robin.warmRobinHadamard8OperatorCandidate.cost

Under one T2 logical-stage convention, four slots strictly improve the
Hadamard-8 route: gate count and depth tie, while the clean layout uses one
fewer auxiliary qubit.

Definition10.27.50

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin four slot t 3 blocked leaf”. Honest boundary: primitive synthesis and refinement remain a T3 obligation.

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. Honest boundary: primitive synthesis and refinement remain a T3 obligation.

Declaration kind. def.

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

Lean code for Definition10.27.50●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFourSlotT3BlockedLeaf : String

def QuantumBlockEncoding.Robin.warmRobinFourSlotT3BlockedLeaf :
  String

Honest boundary: primitive synthesis and refinement remain a T3 obligation.