Figure4SourceData.lean🔗

15 explicit public declarations, in source order.

Definition10.11.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 d offset”. Offset table for the non-transposed sparse access used after register transport.

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. Offset table for the non-transposed sparse access used after register transport.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

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

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

Offset table for the non-transposed sparse access used after register
transport.

Theorem10.11.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 d 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/Figure4SourceData.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.11.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

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

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

Theorem10.11.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 dt d offsets cancel”; 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/Figure4SourceData.lean:23. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.11.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DT_D_offsets_cancel
  (slot : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinSourceDTOffset slot) +
      ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset slot) ≡
    0 [MOD 8]

theorem QuantumBlockEncoding.Robin.warmRobinFigure4DT_D_offsets_cancel
  (slot : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinSourceDTOffset
          slot) +
      ↑(QuantumBlockEncoding.Robin.warmRobinFigure4DOffset
          slot) ≡
    0 [MOD 8]

Definition10.11.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin periodic integer reference”. Periodic fourth-order integer stencil indexed by cyclic row offset.

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. Periodic fourth-order integer stencil indexed by cyclic row offset.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference :
  QuantumBlockEncoding.Matrix 8 8 ℤ

def QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference :
  QuantumBlockEncoding.Matrix 8 8 ℤ

Periodic fourth-order integer stencil indexed by cyclic row offset.

Theorem10.11.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin periodic rows two through five”; 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/Figure4SourceData.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.11.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPeriodic_rows_two_through_five
  (row : Fin 8) (bulk : 2 ≤ ↑row ∧ ↑row ≤ 5) (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference row
      column

theorem QuantumBlockEncoding.Robin.warmRobinPeriodic_rows_two_through_five
  (row : Fin 8)
  (bulk : 2 ≤ ↑row ∧ ↑row ≤ 5)
  (column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference
      row column

Theorem10.11.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin periodic columns three and four”; 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/Figure4SourceData.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.11.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPeriodic_columns_three_and_four
  (column : Fin 8) (bulk : column = 3 ∨ column = 4) (row : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference row
      column

theorem QuantumBlockEncoding.Robin.warmRobinPeriodic_columns_three_and_four
  (column : Fin 8)
  (bulk : column = 3 ∨ column = 4)
  (row : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference
      row column

Definition10.11.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 transpose bulk”. Figure 4 acts on a row of 'D^T', equivalently a column of 'D'.

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. Figure 4 acts on a row of 'D^T', equivalently a column of 'D'.

Declaration kind. def.

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

Lean code for Definition10.11.7●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

def QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
  (column : Fin 8) : Prop

def QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
  (column : Fin 8) : Prop

Figure 4 acts on a row of `D^T`, equivalently a column of `D`.

Theorem10.11.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 transpose bulk matches periodic”; 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/Figure4SourceData.lean:58. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.11.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk_matches_periodic
  (column : Fin 8)
  (bulk :
    QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk column)
  (row : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference row
      column

theorem QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk_matches_periodic
  (column : Fin 8)
  (bulk :
    QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
      column)
  (row : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference
      row column

Theorem10.11.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 column two not transpose bulk”; 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/Figure4SourceData.lean:64. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.11.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_column_two_not_transpose_bulk :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget 0 2 = -2 ∧
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference 0 2 =
      -1

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_column_two_not_transpose_bulk :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
        0 2 =
      -2 ∧
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference
        0 2 =
      -1

Theorem10.11.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 column five not transpose bulk”; 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/Figure4SourceData.lean:69. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.11.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_column_five_not_transpose_bulk :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget 7 5 = -2 ∧
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference 7 5 =
      -1

theorem QuantumBlockEncoding.Robin.warmRobinFigure4_column_five_not_transpose_bulk :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
        7 5 =
      -2 ∧
    QuantumBlockEncoding.Robin.warmRobinPeriodicIntegerReference
        7 5 =
      -1

Definition10.11.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 bulk coefficient”. Interior derivative coefficients by physical selector 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. Interior derivative coefficients by physical selector slot.

Declaration kind. def.

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

Lean code for Definition10.11.11●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

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

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

Interior derivative coefficients by physical selector slot.

Definition10.11.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin figure 4 boundary coefficient”.

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

Lean code for Definition10.11.12●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

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

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

Definition10.11.13

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.11.13●1 definition

defdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

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

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

Theorem10.11.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient_eq_weight
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient slot
      column =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight slot
          column) /
      32

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient_eq_weight
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
      slot column =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenWeight
          slot column) /
      32

Theorem10.11.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Figure4SourceData.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient_branch
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient slot
      column =
    if
        QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
          column then
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient slot
    else
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryCoefficient
        slot column

theorem QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient_branch
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinFigure4SourceCoefficient
      slot column =
    if
        QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk
          column then
      QuantumBlockEncoding.Robin.warmRobinFigure4BulkCoefficient
        slot
    else
      QuantumBlockEncoding.Robin.warmRobinFigure4BoundaryCoefficient
        slot column