WeightedPermutation.lean🔗

15 explicit public declarations, in source order.

Definition10.34.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin five shift perm”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.1●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm (slot : Fin 5)
  (column : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm
  (slot : Fin 5) (column : Fin 8) : Fin 8

Definition10.34.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin five shift inverse”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.2●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFiveShiftInverse (slot : Fin 5)
  (row : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinFiveShiftInverse
  (slot : Fin 5) (row : Fin 8) : Fin 8

Definition10.34.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin five shift weight”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.3●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFiveShiftWeight (slot : Fin 5)
  (column : Fin 8) : ℤ

def QuantumBlockEncoding.Robin.warmRobinFiveShiftWeight
  (slot : Fin 5) (column : Fin 8) : ℤ

Theorem10.34.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin five shift left inverse”; 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/WeightedPermutation.lean:36. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.34.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_leftInverse (slot : Fin 5)
  (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFiveShiftInverse slot
      (QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm slot column) =
    column

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_leftInverse
  (slot : Fin 5) (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFiveShiftInverse
      slot
      (QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm
        slot column) =
    column

Theorem10.34.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin five shift right inverse”; 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/WeightedPermutation.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.34.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_rightInverse
  (slot : Fin 5) (row : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm slot
      (QuantumBlockEncoding.Robin.warmRobinFiveShiftInverse slot row) =
    row

theorem QuantumBlockEncoding.Robin.warmRobinFiveShift_rightInverse
  (slot : Fin 5) (row : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm
      slot
      (QuantumBlockEncoding.Robin.warmRobinFiveShiftInverse
        slot row) =
    row

Theorem10.34.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin five shift perm bijective”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.34.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm_bijective
  (slot : Fin 5) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm slot)

theorem QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm_bijective
  (slot : Fin 5) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm
      slot)

Theorem10.34.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin five shift decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. Exact 64-entry five-shift decomposition, with columns mapped to rows.

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 64-entry five-shift decomposition, with columns mapped to rows.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShiftDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm slot
              column =
            row then
        QuantumBlockEncoding.Robin.warmRobinFiveShiftWeight slot column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinFiveShiftDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinFiveShiftPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinFiveShiftWeight
          slot column
      else 0

Exact 64-entry five-shift decomposition, with columns mapped to rows.

Definition10.34.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin five shift amplitude”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.8●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFiveShiftAmplitude (slot : Fin 5)
  (column : Fin 8) : ℚ

def QuantumBlockEncoding.Robin.warmRobinFiveShiftAmplitude
  (slot : Fin 5) (column : Fin 8) : ℚ

Theorem10.34.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.34.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFiveShiftAmplitude_bounded
  (slot : Fin 5) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinFiveShiftAmplitude slot column| ≤
    5 / 7

theorem QuantumBlockEncoding.Robin.warmRobinFiveShiftAmplitude_bounded
  (slot : Fin 5) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinFiveShiftAmplitude
        slot column| ≤
    5 / 7

Definition10.34.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin eight slot perm”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.10●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinEightSlotPerm
  (slot column : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinEightSlotPerm
  (slot column : Fin 8) : Fin 8

Definition10.34.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin eight slot weight”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.11●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinEightSlotWeight
  (slot column : Fin 8) : ℤ

def QuantumBlockEncoding.Robin.warmRobinEightSlotWeight
  (slot column : Fin 8) : ℤ

Theorem10.34.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin eight slot decomposition”; 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/WeightedPermutation.lean:92. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.34.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinEightSlotDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinEightSlotPerm slot
              column =
            row then
        QuantumBlockEncoding.Robin.warmRobinEightSlotWeight slot column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinEightSlotDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinEightSlotPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinEightSlotWeight
          slot column
      else 0

Theorem10.34.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin eight slot perm bijective”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem10.34.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinEightSlotPerm_bijective
  (slot : Fin 8) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinEightSlotPerm slot)

theorem QuantumBlockEncoding.Robin.warmRobinEightSlotPerm_bijective
  (slot : Fin 8) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinEightSlotPerm
      slot)

Definition10.34.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin eight slot amplitude”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition10.34.14●1 definition

defdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

def QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude
  (slot column : Fin 8) : ℚ

def QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude
  (slot column : Fin 8) : ℚ

Theorem10.34.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin eight slot amplitude bounded”; 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/WeightedPermutation.lean:107. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.34.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/WeightedPermutation.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude_bounded
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude slot column| ≤
    4 / 7

theorem QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude_bounded
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude
        slot column| ≤
    4 / 7