SixSlotOptimal.lean🔗

20 explicit public declarations, in source order.

Definition10.23.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot perm”. Six finite basis permutations, represented column-to-row.

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 finite basis permutations, represented column-to-row.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSixSlotPerm (slot : Fin 6)
  (column : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinSixSlotPerm
  (slot : Fin 6) (column : Fin 8) : Fin 8

Six finite basis permutations, represented column-to-row.

Definition10.23.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot weight”. Integer coefficient table for the six-slot certificate.

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 coefficient table for the six-slot certificate.

Declaration kind. def.

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

Lean code for Definition10.23.2●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

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

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

Integer coefficient table for the six-slot certificate.

Definition10.23.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot cap”. Per-slot absolute coefficient caps.

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. Per-slot absolute coefficient caps.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSixSlotCap (slot : Fin 6) : ℕ

def QuantumBlockEncoding.Robin.warmRobinSixSlotCap
  (slot : Fin 6) : ℕ

Per-slot absolute coefficient caps.

Theorem10.23.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.23.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotPerm_bijective
  (slot : Fin 6) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinSixSlotPerm slot)

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotPerm_bijective
  (slot : Fin 6) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinSixSlotPerm
      slot)

Theorem10.23.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. Exact reconstruction of the integer 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. Exact reconstruction of the integer target.

Declaration kind. theorem.

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

Lean code for Theorem10.23.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSixSlotPerm slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSixSlotWeight slot column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSixSlotPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSixSlotWeight
          slot column
      else 0

Exact reconstruction of the integer target.

Theorem10.23.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot weight nat abs le cap”; the hypotheses and conclusion in the code panel fix its exact scope. Every coefficient is bounded by its declared slot cap.

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 coefficient is bounded by its declared slot cap.

Declaration kind. theorem.

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

Lean code for Theorem10.23.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotWeight_natAbs_le_cap
  (slot : Fin 6) (column : Fin 8) :
  (QuantumBlockEncoding.Robin.warmRobinSixSlotWeight slot
        column).natAbs ≤
    QuantumBlockEncoding.Robin.warmRobinSixSlotCap slot

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotWeight_natAbs_le_cap
  (slot : Fin 6) (column : Fin 8) :
  (QuantumBlockEncoding.Robin.warmRobinSixSlotWeight
        slot column).natAbs ≤
    QuantumBlockEncoding.Robin.warmRobinSixSlotCap
      slot

Every coefficient is bounded by its declared slot cap.

Theorem10.23.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot cap sum eq eighty”; the hypotheses and conclusion in the code panel fix its exact scope. The six caps sum to 80.

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 six caps sum to 80.

Declaration kind. theorem.

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

Lean code for Theorem10.23.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotCap_sum_eq_eighty :
  ∑ slot, QuantumBlockEncoding.Robin.warmRobinSixSlotCap slot = 80

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotCap_sum_eq_eighty :
  ∑ slot,
      QuantumBlockEncoding.Robin.warmRobinSixSlotCap
        slot =
    80

The six caps sum to 80.

Definition10.23.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot prepare probability”. Probability assigned to one selector slot by the intrinsic PREPARE.

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. Probability assigned to one selector slot by the intrinsic PREPARE.

Declaration kind. def.

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

Lean code for Definition10.23.8●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSixSlotPrepareProbability
  (slot : Fin 6) : ℚ

def QuantumBlockEncoding.Robin.warmRobinSixSlotPrepareProbability
  (slot : Fin 6) : ℚ

Probability assigned to one selector slot by the intrinsic PREPARE.

Definition10.23.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot intrinsic amplitude”. Intrinsic clean coefficient 'weight / cap'.

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. Intrinsic clean coefficient 'weight / cap'.

Declaration kind. def.

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

Lean code for Definition10.23.9●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

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

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

Intrinsic clean coefficient `weight / cap`.

Theorem10.23.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot intrinsic amplitude bounded”; the hypotheses and conclusion in the code panel fix its exact scope. All intrinsic amplitude coefficients lie in '[-1,1]'.

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. All intrinsic amplitude coefficients lie in '[-1,1]'.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicAmplitude_bounded
  (slot : Fin 6) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicAmplitude slot
        column| ≤
    1

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicAmplitude_bounded
  (slot : Fin 6) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicAmplitude
        slot column| ≤
    1

All intrinsic amplitude coefficients lie in `[-1,1]`.

Definition10.23.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot fixed amplitude”. Coefficient for the fixed 'M/224' comparison contract.

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. Coefficient for the fixed 'M/224' comparison contract.

Declaration kind. def.

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

Lean code for Definition10.23.11●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

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

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

Coefficient for the fixed `M/224` comparison contract.

Theorem10.23.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot fixed amplitude bounded”; the hypotheses and conclusion in the code panel fix its exact scope. Fixed-normalizer amplitudes are uniformly bounded by '5/14'.

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. Fixed-normalizer amplitudes are uniformly bounded by '5/14'.

Declaration kind. theorem.

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

Lean code for Theorem10.23.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotFixedAmplitude_bounded
  (slot : Fin 6) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinSixSlotFixedAmplitude slot
        column| ≤
    5 / 14

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotFixedAmplitude_bounded
  (slot : Fin 6) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinSixSlotFixedAmplitude
        slot column| ≤
    5 / 14

Fixed-normalizer amplitudes are uniformly bounded by `5/14`.

Definition10.23.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot intrinsic clean formula”. Structural clean formula at the intrinsic normalizer.

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 at the intrinsic normalizer.

Declaration kind. def.

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

Lean code for Definition10.23.13●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicCleanFormula :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicCleanFormula :
  QuantumBlockEncoding.Matrix 8 8 ℚ

Structural clean formula at the intrinsic normalizer.

Theorem10.23.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot intrinsic clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The intrinsic formula is exactly 'A / (20/3) = M/80'.

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 intrinsic formula is exactly 'A / (20/3) = M/80'.

Declaration kind. theorem.

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

Lean code for Theorem10.23.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicCleanFormula_eq_target
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicCleanFormula row
      column =
    QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
      (20 / 3)

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicCleanFormula_eq_target
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSixSlotIntrinsicCleanFormula
      row column =
    QuantumBlockEncoding.RobinEvolution.warmRobinTarget
        row column /
      (20 / 3)

The intrinsic formula is exactly `A / (20/3) = M/80`.

Definition10.23.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin six slot fixed clean formula”. Structural clean formula under the established fixed normalizer.

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 under the established fixed normalizer.

Declaration kind. def.

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

Lean code for Definition10.23.15●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSixSlotFixedCleanFormula :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.Robin.warmRobinSixSlotFixedCleanFormula :
  QuantumBlockEncoding.Matrix 8 8 ℚ

Structural clean formula under the established fixed normalizer.

Theorem10.23.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot fixed clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The fixed formula is exactly 'A / (56/3) = 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 fixed formula is exactly 'A / (56/3) = M/224'.

Declaration kind. theorem.

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

Lean code for Theorem10.23.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotFixedCleanFormula_eq_target
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSixSlotFixedCleanFormula row
      column =
    QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
      QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotFixedCleanFormula_eq_target
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSixSlotFixedCleanFormula
      row column =
    QuantumBlockEncoding.RobinEvolution.warmRobinTarget
        row column /
      QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer

The fixed formula is exactly `A / (56/3) = M/224`.

Definition10.23.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin integer column l 1”. Absolute column sum of the integer 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. Absolute column sum of the integer target.

Declaration kind. def.

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

Lean code for Definition10.23.17●1 definition

defdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

def QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1 (column : Fin 8) : ℕ

def QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1
  (column : Fin 8) : ℕ

Absolute column sum of the integer target.

Theorem10.23.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin integer column l 1 le eighty”; 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/SixSlotOptimal.lean:143. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.23.18●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1_le_eighty
  (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1 column ≤ 80

theorem QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1_le_eighty
  (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1
      column ≤
    80

Theorem10.23.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin integer column one l 1 eq eighty”; 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/SixSlotOptimal.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.23.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinIntegerColumnOneL1_eq_eighty :
  QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1 1 = 80

theorem QuantumBlockEncoding.Robin.warmRobinIntegerColumnOneL1_eq_eighty :
  QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1
      1 =
    80

Theorem10.23.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin six slot cap sum eq max column l 1”; the hypotheses and conclusion in the code panel fix its exact scope. The cap sum attains the largest absolute column sum of the 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 cap sum attains the largest absolute column sum of the target.

Declaration kind. theorem.

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

Lean code for Theorem10.23.20●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SixSlotOptimal.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotCap_sum_eq_maxColumnL1 :
  ∑ slot, QuantumBlockEncoding.Robin.warmRobinSixSlotCap slot =
    QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1 1

theorem QuantumBlockEncoding.Robin.warmRobinSixSlotCap_sum_eq_maxColumnL1 :
  ∑ slot,
      QuantumBlockEncoding.Robin.warmRobinSixSlotCap
        slot =
    QuantumBlockEncoding.Robin.warmRobinIntegerColumnL1
      1

The cap sum attains the largest absolute column sum of the target.