QuantumBlockEncoding/Robin/Figure4SourceData.lean

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.

def warmRobinFigure4DOffset (slot : Fin 8) : Fin 8 :=
  ⟨(slot.val + 5) % 8, Nat.mod_lt _ (by decide)⟩

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinFigure4DT_D_offsets_cancel (slot : Fin 8) :
    (warmRobinSourceDTOffset slot).val +
        (warmRobinFigure4DOffset slot).val ≡ 0 [MOD 8] := by

commit-pinned source · Verso Blueprint panel

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.

def warmRobinPeriodicIntegerReference : Matrix 8 8 Int := fun row column =>
  match (row.val + 8 - column.val) % 8 with
  | 0 => -30
  | 1 | 7 => 16
  | 2 | 6 => -1
  | _ => 0

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinPeriodic_rows_two_through_five (row : Fin 8)
    (bulk : 2 ≤ row.val ∧ row.val ≤ 5) :
    ∀ column, warmRobinIntegerTarget row column =
      warmRobinPeriodicIntegerReference row column := by

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinPeriodic_columns_three_and_four (column : Fin 8)
    (bulk : column = 3 ∨ column = 4) :
    ∀ row, warmRobinIntegerTarget row column =
      warmRobinPeriodicIntegerReference row column := by

commit-pinned source · Verso Blueprint panel

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'.

def warmRobinFigure4TransposeBulk (column : Fin 8) : Prop :=
  column = 3 ∨ column = 4

instance (column : Fin 8) : Decidable (warmRobinFigure4TransposeBulk column) :=
  by

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinFigure4TransposeBulk_matches_periodic
    (column : Fin 8) (bulk : warmRobinFigure4TransposeBulk column) :
    ∀ row, warmRobinIntegerTarget row column =
      warmRobinPeriodicIntegerReference row column :=
  warmRobinPeriodic_columns_three_and_four column bulk

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinFigure4_column_two_not_transpose_bulk :
    warmRobinIntegerTarget 0 2 = -2 ∧
      warmRobinPeriodicIntegerReference 0 2 = -1 := by

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinFigure4_column_five_not_transpose_bulk :
    warmRobinIntegerTarget 7 5 = -2 ∧
      warmRobinPeriodicIntegerReference 7 5 = -1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk coefficient”. Interior derivative coefficients by physical selector slot.

def warmRobinFigure4BulkCoefficient (slot : Fin 8) : Rat :=
  match slot.val with
  | 0 => 0
  | 1 => -1 / 32
  | 2 => 16 / 32
  | 3 => -30 / 32
  | 4 => 16 / 32
  | 5 => -1 / 32
  | _ => 0

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4BoundaryCoefficient (slot column : Fin 8) : Rat :=
  warmRobinSourceSevenWeight slot column / 32

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4SourceCoefficient (slot column : Fin 8) : Rat :=
  warmRobinIntegerTarget (warmRobinSourceDTRow slot column) column / 32

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinFigure4SourceCoefficient_eq_weight (slot column : Fin 8) :
    warmRobinFigure4SourceCoefficient slot column =
      warmRobinSourceSevenWeight slot column / 32 := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel