EvolvedCandidates.lean🔗

15 explicit public declarations, in source order.

Definition10.6.1

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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. Clean branch predicted by the uniform-five LCU construction.

Declaration kind. def.

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

Lean code for Definition10.6.1●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Clean branch predicted by the uniform-five LCU construction.

Theorem10.6.2

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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

Lean code for Theorem10.6.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Definition10.6.3

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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. Clean branch predicted by the uniform Hadamard-8 LCU construction.

Declaration kind. def.

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

Lean code for Definition10.6.3●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Clean branch predicted by the uniform Hadamard-8 LCU construction.

Theorem10.6.4

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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/EvolvedCandidates.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.6.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Definition10.6.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin seven to eight 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. 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/EvolvedCandidates.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.6.5●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSevenToEightSlot (slot : Fin 7) :
  Fin 8

def QuantumBlockEncoding.Robin.warmRobinSevenToEightSlot
  (slot : Fin 7) : Fin 8

Definition10.6.6

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.6.6●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

def QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm (slot : Fin 7)
  (column : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm
  (slot : Fin 7) (column : Fin 8) : Fin 8

Definition10.6.7

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.6.7●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Theorem10.6.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.6.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSevenSlotDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm slot
              column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSevenSlotWeight slot column
      else 0

theorem QuantumBlockEncoding.Robin.warmRobinSevenSlotDecomposition
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinIntegerTarget
      row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSevenSlotWeight
          slot column
      else 0

Theorem10.6.9

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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 historical split-seven route is a weighted-permutation LCU, not a sparse-access enumeration: two nonzero terms can address the same entry.

Declaration kind. theorem.

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

Lean code for Theorem10.6.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSplitSeven_duplicate_nonzero_access :
  QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm 2 6 = 7 ∧
    QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm 5 6 = 7 ∧
      QuantumBlockEncoding.Robin.warmRobinSevenSlotWeight 2 6 = 16 ∧
        QuantumBlockEncoding.Robin.warmRobinSevenSlotWeight 5 6 = 16

theorem QuantumBlockEncoding.Robin.warmRobinSplitSeven_duplicate_nonzero_access :
  QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm
        2 6 =
      7 ∧
    QuantumBlockEncoding.Robin.warmRobinSevenSlotPerm
          5 6 =
        7 ∧
      QuantumBlockEncoding.Robin.warmRobinSevenSlotWeight
            2 6 =
          16 ∧
        QuantumBlockEncoding.Robin.warmRobinSevenSlotWeight
            5 6 =
          16

The historical split-seven route is a weighted-permutation LCU, not a
sparse-access enumeration: two nonzero terms can address the same entry.

Definition10.6.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.6.10●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Theorem10.6.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.6.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinSevenSlotAmplitude_bounded
  (slot : Fin 7) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinSevenSlotAmplitude slot column| ≤
    31 / 32

theorem QuantumBlockEncoding.Robin.warmRobinSevenSlotAmplitude_bounded
  (slot : Fin 7) (column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinSevenSlotAmplitude
        slot column| ≤
    31 / 32

Definition10.6.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin seven slot 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/EvolvedCandidates.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.6.12●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Theorem10.6.13

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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

Lean code for Theorem10.6.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

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

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

Definition10.6.14

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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. Precise promotion blocker for the genuinely structural-only routes.

Declaration kind. def.

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

Lean code for Definition10.6.14●1 definition

defdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHistoricalStructuralCandidateBlockedLeaf :
  String

def QuantumBlockEncoding.Robin.warmRobinHistoricalStructuralCandidateBlockedLeaf :
  String

Precise promotion blocker for the genuinely structural-only routes.

Definition10.6.15

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

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. Historical compatibility alias scoped to structural-only candidates.

Declaration kind. abbrev.

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

Lean code for Definition10.6.15●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/EvolvedCandidates.lean

complete

abbrev QuantumBlockEncoding.Robin.warmRobinStructuralCandidateBlockedLeaf :
  String

abbrev QuantumBlockEncoding.Robin.warmRobinStructuralCandidateBlockedLeaf :
  String

Historical compatibility alias scoped to structural-only candidates.