SourceSevenSparseData.lean🔗

18 explicit public declarations, in source order.

Definition10.25.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source dt offset”. The source 'D^T' offset ordering, expressed in the physical selector.

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 'D^T' offset ordering, expressed in the physical selector.

Declaration kind. def.

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

Lean code for Definition10.25.1●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSourceDTOffset (slot : Fin 8) :
  Fin 8

def QuantumBlockEncoding.Robin.warmRobinSourceDTOffset
  (slot : Fin 8) : Fin 8

The source `D^T` offset ordering, expressed in the physical selector.

Theorem10.25.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.25.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceDTOffset_table :
  List.ofFn QuantumBlockEncoding.Robin.warmRobinSourceDTOffset =
    [3, 2, 1, 0, 7, 6, 5, 4]

theorem QuantumBlockEncoding.Robin.warmRobinSourceDTOffset_table :
  List.ofFn
      QuantumBlockEncoding.Robin.warmRobinSourceDTOffset =
    [3, 2, 1, 0, 7, 6, 5, 4]

Definition10.25.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source dt row”. Sparse row addressed by one physical slot at a fixed source column.

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. Sparse row addressed by one physical slot at a fixed source column.

Declaration kind. def.

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

Lean code for Definition10.25.3●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

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

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

Sparse row addressed by one physical slot at a fixed source column.

Definition10.25.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source seven weight”. Exact integer value returned by the source sparse-value oracle.

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

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

Technical source note. Exact integer value returned by the source sparse-value oracle.

Declaration kind. def.

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

Lean code for Definition10.25.4●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

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

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

Exact integer value returned by the source sparse-value oracle.

Theorem10.25.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source seven weight slot 7 zero”; the hypotheses and conclusion in the code panel fix its exact scope. Slot seven is the zero diagonal used only for physical padding.

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. Slot seven is the zero diagonal used only for physical padding.

Declaration kind. theorem.

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

Lean code for Theorem10.25.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight_slot7_zero
  (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight 7 column = 0

theorem QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight_slot7_zero
  (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight
      7 column =
    0

Slot seven is the zero diagonal used only for physical padding.

Theorem10.25.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source dt row bijective in slot”; the hypotheses and conclusion in the code panel fix its exact scope. At a fixed column, the eight physical slots enumerate eight distinct 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. At a fixed column, the eight physical slots enumerate eight distinct rows.

Declaration kind. theorem.

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

Lean code for Theorem10.25.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceDTRow_bijective_in_slot
  (column : Fin 8) :
  Function.Bijective fun slot =>
    QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column

theorem QuantumBlockEncoding.Robin.warmRobinSourceDTRow_bijective_in_slot
  (column : Fin 8) :
  Function.Bijective fun slot =>
    QuantumBlockEncoding.Robin.warmRobinSourceDTRow
      slot column

At a fixed column, the eight physical slots enumerate eight distinct rows.

Theorem10.25.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source dt row bijective in column”; the hypotheses and conclusion in the code panel fix its exact scope. At a fixed slot, cyclic sparse access is a permutation of the columns.

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. At a fixed slot, cyclic sparse access is a permutation of the columns.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceDTRow_bijective_in_column
  (slot : Fin 8) :
  Function.Bijective fun column =>
    QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column

theorem QuantumBlockEncoding.Robin.warmRobinSourceDTRow_bijective_in_column
  (slot : Fin 8) :
  Function.Bijective fun column =>
    QuantumBlockEncoding.Robin.warmRobinSourceDTRow
      slot column

At a fixed slot, cyclic sparse access is a permutation of the columns.

Theorem10.25.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source seven sparse decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. Exact sparse-access decomposition with seven active physical states.

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 sparse-access decomposition with seven active physical states.

Declaration kind. theorem.

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

Lean code for Theorem10.25.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceSevenSparseDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    ∑ slot,
      if
          ↑slot < 7 ∧
            QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot
                column =
              row then
        QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight slot
          column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinSourceSevenSparseDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    ∑ slot,
      if
          ↑slot < 7 ∧
            QuantumBlockEncoding.Robin.warmRobinSourceDTRow
                slot column =
              row then
        QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight
          slot column
      else 0

Exact sparse-access decomposition with seven active physical states.

Definition10.25.9

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.25.9●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSourceND : ℚ

def QuantumBlockEncoding.Robin.warmRobinSourceND :
  ℚ

Definition10.25.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.25.10●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSourceNf : ℚ

def QuantumBlockEncoding.Robin.warmRobinSourceNf :
  ℚ

Definition10.25.11

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.25.11●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSourceKappa : ℚ

def QuantumBlockEncoding.Robin.warmRobinSourceKappa :
  ℚ

Theorem10.25.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source amplitude eq integer div 32”; 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/SourceSevenSparseData.lean:60. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.25.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceAmplitude_eq_integer_div_32
  (row column : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column) / 12 /
      QuantumBlockEncoding.Robin.warmRobinSourceND =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column) / 32

theorem QuantumBlockEncoding.Robin.warmRobinSourceAmplitude_eq_integer_div_32
  (row column : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
            row column) /
        12 /
      QuantumBlockEncoding.Robin.warmRobinSourceND =
    ↑(QuantumBlockEncoding.Robin.warmRobinIntegerTarget
          row column) /
      32

Theorem10.25.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.25.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceAlpha_eq :
  QuantumBlockEncoding.Robin.warmRobinSourceND *
        QuantumBlockEncoding.Robin.warmRobinSourceNf *
      QuantumBlockEncoding.Robin.warmRobinSourceKappa =
    56 / 3

theorem QuantumBlockEncoding.Robin.warmRobinSourceAlpha_eq :
  QuantumBlockEncoding.Robin.warmRobinSourceND *
        QuantumBlockEncoding.Robin.warmRobinSourceNf *
      QuantumBlockEncoding.Robin.warmRobinSourceKappa =
    56 / 3

Definition10.25.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source seven selector probability”. Selector probability in the clean column of padded-seven 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. Selector probability in the clean column of padded-seven PREPARE.

Declaration kind. def.

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

Lean code for Definition10.25.14●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSourceSevenSelectorProbability
  (slot : Fin 8) : ℚ

def QuantumBlockEncoding.Robin.warmRobinSourceSevenSelectorProbability
  (slot : Fin 8) : ℚ

Selector probability in the clean column of padded-seven PREPARE.

Definition10.25.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source seven padded coefficient”. Coefficient loaded by an active sparse slot.

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 loaded by an active sparse slot. The padded slot is assigned the identity coefficient because its clean PREPARE probability is zero.

Declaration kind. def.

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

Lean code for Definition10.25.15●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

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

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

Coefficient loaded by an active sparse slot. The padded slot is assigned
the identity coefficient because its clean PREPARE probability is zero.

Definition10.25.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin source seven clean formula”.

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

Lean code for Definition10.25.16●1 definition

defdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

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

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

Theorem10.25.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source seven clean formula eq integer div 224”; 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/SourceSevenSparseData.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.25.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula_eq_integer_div_224
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula row
      column =
    QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat row column /
      224

theorem QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula_eq_integer_div_224
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula
      row column =
    QuantumBlockEncoding.Robin.warmRobinIntegerTargetRat
        row column /
      224

Theorem10.25.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin source seven clean formula eq target”; 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/SourceSevenSparseData.lean:93. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.25.18●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

complete

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

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