SymmetryFourSlot.lean🔗

21 explicit public declarations, in source order.

Definition10.26.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin reverse 8”. Reverse an eight-dimensional basis index.

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

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

Technical source note. Reverse an eight-dimensional basis index.

Declaration kind. def.

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

Lean code for Definition10.26.1●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinReverse8 (index : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinReverse8
  (index : Fin 8) : Fin 8

Reverse an eight-dimensional basis index.

Theorem10.26.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.26.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinReverse8_value (index : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinReverse8 index) = 7 - ↑index

theorem QuantumBlockEncoding.Robin.warmRobinReverse8_value
  (index : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinReverse8
        index) =
    7 - ↑index

Theorem10.26.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.26.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinReverse8_involution
  (index : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinReverse8
      (QuantumBlockEncoding.Robin.warmRobinReverse8 index) =
    index

theorem QuantumBlockEncoding.Robin.warmRobinReverse8_involution
  (index : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinReverse8
      (QuantumBlockEncoding.Robin.warmRobinReverse8
        index) =
    index

Theorem10.26.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin integer target centrosymmetric”; the hypotheses and conclusion in the code panel fix its exact scope. The fixed integer Robin matrix is invariant under simultaneous reversal.

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 fixed integer Robin matrix is invariant under simultaneous reversal.

Declaration kind. theorem.

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

Lean code for Theorem10.26.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_centrosymmetric
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinReverse8 row)
      (QuantumBlockEncoding.Robin.warmRobinReverse8 column)

theorem QuantumBlockEncoding.Robin.warmRobinIntegerTarget_centrosymmetric
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      (QuantumBlockEncoding.Robin.warmRobinReverse8
        row)
      (QuantumBlockEncoding.Robin.warmRobinReverse8
        column)

The fixed integer Robin matrix is invariant under simultaneous reversal.

Definition10.26.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair low”. Embed the low representative of a reversal pair.

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. Embed the low representative of a reversal pair.

Declaration kind. def.

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

Lean code for Definition10.26.5●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairLow (index : Fin 4) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPairLow
  (index : Fin 4) : Fin 8

Embed the low representative of a reversal pair.

Definition10.26.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin pair high”. Embed the high representative paired with 'index'.

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

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

Technical source note. Embed the high representative paired with 'index'.

Declaration kind. def.

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

Lean code for Definition10.26.6●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPairHigh (index : Fin 4) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPairHigh
  (index : Fin 4) : Fin 8

Embed the high representative paired with `index`.

Definition10.26.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry plus block”. Integer matrix in the symmetric reversal sector.

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. Integer matrix in the symmetric reversal sector.

Declaration kind. def.

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

Lean code for Definition10.26.7●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock :
  QuantumBlockEncoding.Matrix 4 4 ℤ

def QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock :
  QuantumBlockEncoding.Matrix 4 4 ℤ

Integer matrix in the symmetric reversal sector.

Definition10.26.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry minus block”. Integer matrix in the antisymmetric reversal sector.

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. Integer matrix in the antisymmetric reversal sector.

Declaration kind. def.

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

Lean code for Definition10.26.8●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock :
  QuantumBlockEncoding.Matrix 4 4 ℤ

def QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock :
  QuantumBlockEncoding.Matrix 4 4 ℤ

Integer matrix in the antisymmetric reversal sector.

Definition10.26.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry four shift perm”. The four cyclic permutations used in both symmetry sectors.

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 four cyclic permutations used in both symmetry sectors.

Declaration kind. def.

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

Lean code for Definition10.26.9●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm
  (slot column : Fin 4) : Fin 4

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm
  (slot column : Fin 4) : Fin 4

The four cyclic permutations used in both symmetry sectors.

Theorem10.26.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.26.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm_bijective
  (slot : Fin 4) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm slot)

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm_bijective
  (slot : Fin 4) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm
      slot)

Definition10.26.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry plus weight”. Integer weights for the symmetric sector.

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. Integer weights for the symmetric sector.

Declaration kind. def.

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

Lean code for Definition10.26.11●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryPlusWeight
  (slot column : Fin 4) : ℤ

def QuantumBlockEncoding.Robin.warmRobinSymmetryPlusWeight
  (slot column : Fin 4) : ℤ

Integer weights for the symmetric sector.

Definition10.26.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry minus weight”. Integer weights for the antisymmetric sector.

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. Integer weights for the antisymmetric sector.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlot.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.26.12●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryMinusWeight
  (slot column : Fin 4) : ℤ

def QuantumBlockEncoding.Robin.warmRobinSymmetryMinusWeight
  (slot column : Fin 4) : ℤ

Integer weights for the antisymmetric sector.

Theorem10.26.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry plus four shift decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. Exact four-shift decomposition of the symmetric sector.

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 four-shift decomposition of the symmetric sector.

Declaration kind. theorem.

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

Lean code for Theorem10.26.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryPlusFourShiftDecomposition
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm slot
              column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSymmetryPlusWeight slot
          column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryPlusFourShiftDecomposition
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock
      row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSymmetryPlusWeight
          slot column
      else 0

Exact four-shift decomposition of the symmetric sector.

Theorem10.26.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry minus four shift decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. Exact four-shift decomposition of the antisymmetric sector.

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 four-shift decomposition of the antisymmetric sector.

Declaration kind. theorem.

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

Lean code for Theorem10.26.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryMinusFourShiftDecomposition
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm slot
              column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSymmetryMinusWeight slot
          column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryMinusFourShiftDecomposition
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock
      row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSymmetryMinusWeight
          slot column
      else 0

Exact four-shift decomposition of the antisymmetric sector.

Definition10.26.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry four shift weight”. Select the weight table by symmetry sector ('0' symmetric, '1' antisymmetric).

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. Select the weight table by symmetry sector ('0' symmetric, '1' antisymmetric).

Declaration kind. def.

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

Lean code for Definition10.26.15●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftWeight
  (sector : Fin 2) (slot column : Fin 4) : ℤ

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftWeight
  (sector : Fin 2) (slot column : Fin 4) :
  ℤ

Select the weight table by symmetry sector (`0` symmetric, `1` antisymmetric).

Definition10.26.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry four shift amplitude”. Clean coefficient used by the four-slot amplitude loader.

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. Clean coefficient used by the four-slot amplitude loader.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlot.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.26.16●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftAmplitude
  (sector : Fin 2) (slot column : Fin 4) : ℚ

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftAmplitude
  (sector : Fin 2) (slot column : Fin 4) :
  ℚ

Clean coefficient used by the four-slot amplitude loader.

Theorem10.26.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry four shift amplitude bounded”; the hypotheses and conclusion in the code panel fix its exact scope. Every four-slot amplitude lies in the unit interval.

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 four-slot amplitude lies in the unit interval.

Declaration kind. theorem.

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

Lean code for Theorem10.26.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftAmplitude_bounded
  (sector : Fin 2) (slot column : Fin 4) :
  |QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftAmplitude sector
        slot column| ≤
    23 / 28

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftAmplitude_bounded
  (sector : Fin 2) (slot column : Fin 4) :
  |QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftAmplitude
        sector slot column| ≤
    23 / 28

Every four-slot amplitude lies in the unit interval.

Definition10.26.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry four shift clean formula”. Structural clean formula in one symmetry sector.

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. Structural clean formula in one symmetry sector.

Declaration kind. def.

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

Lean code for Definition10.26.18●1 definition

defdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftCleanFormula
  (sector : Fin 2) : QuantumBlockEncoding.Matrix 4 4 ℚ

def QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftCleanFormula
  (sector : Fin 2) :
  QuantumBlockEncoding.Matrix 4 4 ℚ

Structural clean formula in one symmetry sector.

Theorem10.26.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry plus four shift clean formula eq”; the hypotheses and conclusion in the code panel fix its exact scope. The symmetric-sector clean formula is exactly 'M₊ / 224'.

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 symmetric-sector clean formula is exactly 'M₊ / 224'.

Declaration kind. theorem.

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

Lean code for Theorem10.26.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryPlusFourShiftCleanFormula_eq
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftCleanFormula 0
      row column =
    ↑(QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock row
          column) /
      224

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryPlusFourShiftCleanFormula_eq
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftCleanFormula
      0 row column =
    ↑(QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock
          row column) /
      224

The symmetric-sector clean formula is exactly `M₊ / 224`.

Theorem10.26.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry minus four shift clean formula eq”; the hypotheses and conclusion in the code panel fix its exact scope. The antisymmetric-sector clean formula is exactly 'M₋ / 224'.

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 antisymmetric-sector clean formula is exactly 'M₋ / 224'.

Declaration kind. theorem.

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

Lean code for Theorem10.26.20●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryMinusFourShiftCleanFormula_eq
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftCleanFormula 1
      row column =
    ↑(QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock row
          column) /
      224

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryMinusFourShiftCleanFormula_eq
  (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetryFourShiftCleanFormula
      1 row column =
    ↑(QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock
          row column) /
      224

The antisymmetric-sector clean formula is exactly `M₋ / 224`.

Theorem10.26.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry blocks column one full support”; the hypotheses and conclusion in the code panel fix its exact scope. Both symmetry blocks have four nonzero entries in column one.

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. Both symmetry blocks have four nonzero entries in column one.

Declaration kind. theorem.

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

Lean code for Theorem10.26.21●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SymmetryFourSlot.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBlocks_columnOne_fullSupport :
  (∀ (row : Fin 4),
      QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock row 1 ≠ 0) ∧
    ∀ (row : Fin 4),
      QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock row 1 ≠ 0

theorem QuantumBlockEncoding.Robin.warmRobinSymmetryBlocks_columnOne_fullSupport :
  (∀ (row : Fin 4),
      QuantumBlockEncoding.Robin.warmRobinSymmetryPlusBlock
          row 1 ≠
        0) ∧
    ∀ (row : Fin 4),
      QuantumBlockEncoding.Robin.warmRobinSymmetryMinusBlock
          row 1 ≠
        0

Both symmetry blocks have four nonzero entries in column one.