This definition gives the library's named construction or computation for “warm robin five shift clean formula”. Clean branch predicted by the uniform-five LCU construction.
def warmRobinFiveShiftCleanFormula : Matrix 8 8 Rat := fun row column =>
(1 / 5 : Rat) * ∑ slot : Fin 5,
if warmRobinFiveShiftPerm slot column = row then
warmRobinFiveShiftAmplitude slot column
else 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin five shift clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFiveShiftCleanFormula_eq_target (row column : Fin 8) :
warmRobinFiveShiftCleanFormula row column =
RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 clean formula”. Clean branch predicted by the uniform Hadamard-8 LCU construction.
def warmRobinHadamard8CleanFormula : Matrix 8 8 Rat := fun row column =>
(1 / 8 : Rat) * ∑ slot : Fin 8,
if warmRobinEightSlotPerm slot column = row then
warmRobinEightSlotAmplitude slot column
else 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinHadamard8CleanFormula_eq_target (row column : Fin 8) :
warmRobinHadamard8CleanFormula row column =
RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin seven to eight slot”.
def warmRobinSevenToEightSlot (slot : Fin 7) : Fin 8 :=
⟨match slot.val with | 0 => 0 | x + 1 => x + 2,
by fin_cases slot <;> decide⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin seven slot perm”.
def warmRobinSevenSlotPerm (slot : Fin 7) (column : Fin 8) : Fin 8 :=
warmRobinEightSlotPerm (warmRobinSevenToEightSlot slot) column
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin seven slot weight”.
def warmRobinSevenSlotWeight (slot : Fin 7) (column : Fin 8) : Int :=
match slot.val with
| 0 => if column.val = 1 || column.val = 6 then -31 else -30
| _ => warmRobinEightSlotWeight (warmRobinSevenToEightSlot slot) column
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin seven slot decomposition”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinSevenSlotDecomposition (row column : Fin 8) :
warmRobinIntegerTarget row column =
∑ slot : Fin 7,
if warmRobinSevenSlotPerm slot column = row then
warmRobinSevenSlotWeight slot column
else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin split seven duplicate nonzero access”; the hypotheses and conclusion in the code panel fix its exact scope. The historical split-seven route is a weighted-permutation LCU, not a sparse-access enumeration: two nonzero terms can address the same entry.
theorem warmRobinSplitSeven_duplicate_nonzero_access :
warmRobinSevenSlotPerm (2 : Fin 7) (6 : Fin 8) = 7 ∧
warmRobinSevenSlotPerm (5 : Fin 7) (6 : Fin 8) = 7 ∧
warmRobinSevenSlotWeight (2 : Fin 7) (6 : Fin 8) = 16 ∧
warmRobinSevenSlotWeight (5 : Fin 7) (6 : Fin 8) = 16 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin seven slot amplitude”.
def warmRobinSevenSlotAmplitude (slot : Fin 7) (column : Fin 8) : Rat :=
warmRobinSevenSlotWeight slot column / 32
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin seven slot amplitude bounded”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinSevenSlotAmplitude_bounded (slot : Fin 7) (column : Fin 8) :
|warmRobinSevenSlotAmplitude slot column| ≤ (31 / 32 : Rat) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin seven slot clean formula”.
def warmRobinSevenSlotCleanFormula : Matrix 8 8 Rat := fun row column =>
(1 / 7 : Rat) * ∑ slot : Fin 7,
if warmRobinSevenSlotPerm slot column = row then
warmRobinSevenSlotAmplitude slot column
else 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin seven slot clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinSevenSlotCleanFormula_eq_target (row column : Fin 8) :
warmRobinSevenSlotCleanFormula row column =
RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin historical structural candidate blocked leaf”. Precise promotion blocker for the genuinely structural-only routes.
def warmRobinHistoricalStructuralCandidateBlockedLeaf : String :=
"specialize a matching complex-unitary clean-entry theorem to the compiled Robin clean formula, then refine it to the circuit certificate interface"
/-- Historical compatibility alias scoped to structural-only candidates. -/
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “warm robin structural candidate blocked leaf”. Historical compatibility alias scoped to structural-only candidates.
abbrev warmRobinStructuralCandidateBlockedLeaf : String :=
warmRobinHistoricalStructuralCandidateBlockedLeaf
commit-pinned source · Verso Blueprint panel