QuantumBlockEncoding/Robin/SourceSevenSparseData.lean

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.

def warmRobinSourceDTOffset (slot : Fin 8) : Fin 8 :=
  ⟨(slot.val ^^^ 3) % 8, Nat.mod_lt _ (by decide)⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin source dt offset table”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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.

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

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

commit-pinned source · Verso Blueprint panel

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.

def warmRobinSourceSevenWeight (slot column : Fin 8) : Int :=
  warmRobinIntegerTarget (warmRobinSourceDTRow slot column) column

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

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinSourceSevenWeight_slot7_zero (column : Fin 8) :
    warmRobinSourceSevenWeight 7 column = 0 := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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

def warmRobinSourceND : Rat := 8 / 3

commit-pinned source · Verso Blueprint panel

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

def warmRobinSourceNf : Rat := 1

commit-pinned source · Verso Blueprint panel

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

def warmRobinSourceKappa : Rat := 7

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinSourceAmplitude_eq_integer_div_32 (row column : Fin 8) :
    ((warmRobinIntegerTarget row column : Rat) / 12) /
        warmRobinSourceND =
      (warmRobinIntegerTarget row column : Rat) / 32 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin source alpha eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinSourceAlpha_eq :
    warmRobinSourceND * warmRobinSourceNf * warmRobinSourceKappa = 56 / 3 := by

commit-pinned source · Verso Blueprint panel

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.

def warmRobinSourceSevenSelectorProbability (slot : Fin 8) : Rat :=
  if slot.val < 7 then 1 / 7 else 0

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

commit-pinned source · Verso Blueprint panel

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

def warmRobinSourceSevenPaddedCoefficient (slot column : Fin 8) : Rat :=
  if slot.val < 7 then warmRobinSourceSevenWeight slot column / 32 else 1

commit-pinned source · Verso Blueprint panel

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

def warmRobinSourceSevenCleanFormula : Matrix 8 8 Rat := fun row column =>
  ∑ slot : Fin 8,
    if warmRobinSourceDTRow slot column = row then
      warmRobinSourceSevenSelectorProbability slot *
        warmRobinSourceSevenPaddedCoefficient slot column
    else 0

commit-pinned source · Verso Blueprint panel

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.

theorem warmRobinSourceSevenCleanFormula_eq_integer_div_224
    (row column : Fin 8) :
    warmRobinSourceSevenCleanFormula row column =
      warmRobinIntegerTargetRat row column / 224 := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel