ComplexLCUProjection.lean🔗

8 explicit public declarations, in source order.

Theorem10.5.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude lift 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/ComplexLCUProjection.lean:17. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.5.1●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift_apply.{u_1, u_2,
    u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift rotation row
      column =
    if row.2 = column.2 then rotation row.2.1 row.2.2 row.1 column.1
    else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
      rotation row column =
    if row.2 = column.2 then
      rotation row.2.1 row.2.2 row.1
        column.1
    else 0

Theorem10.5.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “select lift 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/ComplexLCUProjection.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.5.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectLift_apply.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [DecidableEq coefficient] [DecidableEq selector] [DecidableEq system]
  (permutation : selector → system ≃ system)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectLift permutation row
      column =
    if
        row =
          (column.1, column.2.1,
            (permutation column.2.1) column.2.2) then
      1
    else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectLift_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [DecidableEq coefficient]
  [DecidableEq selector]
  [DecidableEq system]
  (permutation :
    selector → system ≃ system)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectLift
      permutation row column =
    if
        row =
          (column.1, column.2.1,
            (permutation column.2.1)
              column.2.2) then
      1
    else 0

Theorem10.5.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selector lift clean column apply”; the hypotheses and conclusion in the code panel fix its exact scope. A selector lift has one coefficient/system delta on a clean input column.

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. A selector lift has one coefficient/system delta on a clean input column.

Declaration kind. theorem.

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

Lean code for Theorem10.5.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectorLift_cleanColumn_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemColumn : system)
  (row :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectorLift prepare row
      (cleanCoefficient, cleanSelector, systemColumn) =
    if row.1 = cleanCoefficient ∧ row.2.2 = systemColumn then
      prepare row.2.1 cleanSelector
    else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectorLift_cleanColumn_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemColumn : system)
  (row :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
      prepare row
      (cleanCoefficient, cleanSelector,
        systemColumn) =
    if
        row.1 = cleanCoefficient ∧
          row.2.2 = systemColumn then
      prepare row.2.1 cleanSelector
    else 0

A selector lift has one coefficient/system delta on a clean input column.

Theorem10.5.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star selector lift clean row apply”; the hypotheses and conclusion in the code panel fix its exact scope. The clean PREPARE bra has the conjugate selector entry and two deltas.

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 PREPARE bra has the conjugate selector entry and two deltas.

Declaration kind. theorem.

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

Lean code for Theorem10.5.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.star_selectorLift_cleanRow_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemRow : system)
  (column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  star (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift prepare)
      (cleanCoefficient, cleanSelector, systemRow) column =
    if column.1 = cleanCoefficient ∧ column.2.2 = systemRow then
      star (prepare column.2.1 cleanSelector)
    else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.star_selectorLift_cleanRow_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemRow : system)
  (column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  star
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        prepare)
      (cleanCoefficient, cleanSelector,
        systemRow)
      column =
    if
        column.1 = cleanCoefficient ∧
          column.2.2 = systemRow then
      star
        (prepare column.2.1 cleanSelector)
    else 0

The clean PREPARE bra has the conjugate selector entry and two deltas.

Theorem10.5.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude lift mul selector lift clean”; the hypotheses and conclusion in the code panel fix its exact scope. Amplitude followed by selector preparation, evaluated on a clean input.

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. Amplitude followed by selector preparation, evaluated on a clean input.

Declaration kind. theorem.

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

Lean code for Theorem10.5.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift_mul_selectorLift_clean.{u_1,
    u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemColumn : system)
  (row :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift rotation *
        QuantumBlockEncoding.Robin.ComplexLCU.selectorLift prepare)
      row (cleanCoefficient, cleanSelector, systemColumn) =
    if row.2.2 = systemColumn then
      rotation row.2.1 row.2.2 row.1 cleanCoefficient *
        prepare row.2.1 cleanSelector
    else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift_mul_selectorLift_clean.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemColumn : system)
  (row :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
          rotation *
        QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
          prepare)
      row
      (cleanCoefficient, cleanSelector,
        systemColumn) =
    if row.2.2 = systemColumn then
      rotation row.2.1 row.2.2 row.1
          cleanCoefficient *
        prepare row.2.1 cleanSelector
    else 0

Amplitude followed by selector preparation, evaluated on a clean input.

Theorem10.5.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “select lift mul amplitude lift mul selector lift clean”; the hypotheses and conclusion in the code panel fix its exact scope. SELECT applied after amplitude and PREPARE, on one clean input column.

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. SELECT applied after amplitude and PREPARE, on one clean input column.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/ComplexLCUProjection.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.5.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectLift_mul_amplitudeLift_mul_selectorLift_clean.{u_1,
    u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (permutation : selector → system ≃ system)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemColumn : system)
  (row :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  (QuantumBlockEncoding.Robin.ComplexLCU.selectLift permutation *
        (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift rotation *
          QuantumBlockEncoding.Robin.ComplexLCU.selectorLift prepare))
      row (cleanCoefficient, cleanSelector, systemColumn) =
    if (permutation row.2.1).symm row.2.2 = systemColumn then
      rotation row.2.1 systemColumn row.1 cleanCoefficient *
        prepare row.2.1 cleanSelector
    else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectLift_mul_amplitudeLift_mul_selectorLift_clean.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (permutation :
    selector → system ≃ system)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemColumn : system)
  (row :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  (QuantumBlockEncoding.Robin.ComplexLCU.selectLift
          permutation *
        (QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
            rotation *
          QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
            prepare))
      row
      (cleanCoefficient, cleanSelector,
        systemColumn) =
    if
        (permutation row.2.1).symm
            row.2.2 =
          systemColumn then
      rotation row.2.1 systemColumn row.1
          cleanCoefficient *
        prepare row.2.1 cleanSelector
    else 0

SELECT applied after amplitude and PREPARE, on one clean input column.

Theorem10.5.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star selector lift mul clean”; the hypotheses and conclusion in the code panel fix its exact scope. Project an arbitrary right factor through the clean PREPARE bra.

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. Project an arbitrary right factor through the clean PREPARE bra.

Declaration kind. theorem.

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

Lean code for Theorem10.5.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.star_selectorLift_mul_clean.{u_1,
    u_2, u_3, u_4}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  {κ : Type u_4} [Fintype coefficient] [DecidableEq coefficient]
  [Fintype selector] [DecidableEq selector] [Fintype system]
  [DecidableEq system] [Fintype κ]
  (prepare : Matrix selector selector ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      κ ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemRow : system) (column : κ) :
  (star (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift prepare) *
        operator)
      (cleanCoefficient, cleanSelector, systemRow) column =
    ∑ selectorIndex,
      star (prepare selectorIndex cleanSelector) *
        operator (cleanCoefficient, selectorIndex, systemRow) column

theorem QuantumBlockEncoding.Robin.ComplexLCU.star_selectorLift_mul_clean.{u_1,
    u_2, u_3, u_4}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3} {κ : Type u_4}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system] [Fintype κ]
  (prepare : Matrix selector selector ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      κ ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemRow : system) (column : κ) :
  (star
          (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
            prepare) *
        operator)
      (cleanCoefficient, cleanSelector,
        systemRow)
      column =
    ∑ selectorIndex,
      star
          (prepare selectorIndex
            cleanSelector) *
        operator
          (cleanCoefficient,
            selectorIndex, systemRow)
          column

Project an arbitrary right factor through the clean PREPARE bra.

Theorem10.5.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare amplitude select unprepare clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Exact projected clean entry of PREPARE/amplitude/SELECT/unprepare.

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. Exact projected clean entry of PREPARE/amplitude/SELECT/unprepare.

Declaration kind. theorem.

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

Lean code for Theorem10.5.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCUProjection.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_cleanEntry.{u_1,
    u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (permutation : selector → system ≃ system)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemRow systemColumn : system) :
  QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare
      prepare rotation permutation
      (cleanCoefficient, cleanSelector, systemRow)
      (cleanCoefficient, cleanSelector, systemColumn) =
    ∑ selectorIndex,
      if (permutation selectorIndex) systemColumn = systemRow then
        star (prepare selectorIndex cleanSelector) *
            rotation selectorIndex systemColumn cleanCoefficient
              cleanCoefficient *
          prepare selectorIndex cleanSelector
      else 0

theorem QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_cleanEntry.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (prepare : Matrix selector selector ℂ)
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (permutation :
    selector → system ≃ system)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemRow systemColumn : system) :
  QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare
      prepare rotation permutation
      (cleanCoefficient, cleanSelector,
        systemRow)
      (cleanCoefficient, cleanSelector,
        systemColumn) =
    ∑ selectorIndex,
      if
          (permutation selectorIndex)
              systemColumn =
            systemRow then
        star
              (prepare selectorIndex
                cleanSelector) *
            rotation selectorIndex
              systemColumn
              cleanCoefficient
              cleanCoefficient *
          prepare selectorIndex
            cleanSelector
      else 0

Exact projected clean entry of PREPARE/amplitude/SELECT/unprepare.