PaperSevenPrepare.lean🔗

20 explicit public declarations, in source order.

Definition10.18.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.1●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenHighAngle :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.Robin.warmRobinUniformSevenHighAngle :
  QuantumBlockEncoding.ExactAngle

Definition10.18.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.2●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenTailAngle :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.Robin.warmRobinUniformSevenTailAngle :
  QuantumBlockEncoding.ExactAngle

Definition10.18.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.3●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleAngles
  (bits : QuantumBlockEncoding.PrimitiveBasis 1) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleAngles
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      1) :
  QuantumBlockEncoding.ExactAngle

Definition10.18.4

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.4●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenLowAngles
  (bits : QuantumBlockEncoding.PrimitiveBasis 2) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.Robin.warmRobinUniformSevenLowAngles
  (bits :
    QuantumBlockEncoding.PrimitiveBasis
      2) :
  QuantumBlockEncoding.ExactAngle

Definition10.18.5

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.5●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleWires :
  Fin 1 → Fin 3

def QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleWires :
  Fin 1 → Fin 3

Theorem10.18.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform seven middle wires ne 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/PaperSevenPrepare.lean:35. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleWires_ne_target
  (wire : Fin 1) :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleWires wire ≠ 1

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleWires_ne_target
  (wire : Fin 1) :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenMiddleWires
      wire ≠
    1

Definition10.18.7

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.7●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenLowWires : Fin 2 → Fin 3

def QuantumBlockEncoding.Robin.warmRobinUniformSevenLowWires :
  Fin 2 → Fin 3

Theorem10.18.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform seven low wires ne 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/PaperSevenPrepare.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenLowWires_ne_target
  (wire : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenLowWires wire ≠ 0

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenLowWires_ne_target
  (wire : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenLowWires
      wire ≠
    0

Definition10.18.9

uses 0used by 0✓L∃∀N

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

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/PaperSevenPrepare.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.18.9●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Definition10.18.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.18.10●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 3

def QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 3

Definition10.18.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin uniform seven prepare matrix”. Independent stagewise matrix specification for the padded selector.

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. Independent stagewise matrix specification for the padded selector.

Declaration kind. def.

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

Lean code for Definition10.18.11●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareMatrix :
  Matrix (QuantumBlockEncoding.PrimitiveBasis 3)
    (QuantumBlockEncoding.PrimitiveBasis 3) ℂ

def QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareMatrix :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      3)
    (QuantumBlockEncoding.PrimitiveBasis
      3)
    ℂ

Independent stagewise matrix specification for the padded selector.

Theorem10.18.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram =
    QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareMatrix

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram =
    QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareMatrix

Theorem10.18.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareMatrix ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis 3) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareMatrix ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        3)
      ℂ

Theorem10.18.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform seven prepare no oracle calls”; 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/PaperSevenPrepare.lean:90. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepare_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram.resource.oracleCalls =
    0

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepare_noOracleCalls :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareProgram.resource.oracleCalls =
    0

Theorem10.18.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepare_counts :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareCircuit.ryCount =
      7 ∧
    QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareCircuit.cxCount =
      8

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepare_counts :
  QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareCircuit.ryCount =
      7 ∧
    QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepareCircuit.cxCount =
      8

Definition10.18.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven padded slot”. The source selector has eight physical states even though only seven are active.

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 selector has eight physical states even though only seven are active. This prevents accidental use of 'Fin 7' as a three-qubit register.

Declaration kind. def.

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

Lean code for Definition10.18.16●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPaddedSlot
  (slot : Fin 8) : Option (Fin 7)

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPaddedSlot
  (slot : Fin 8) : Option (Fin 7)

The source selector has eight physical states even though only seven are
active.  This prevents accidental use of `Fin 7` as a three-qubit register.

Theorem10.18.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPaddedSlot_seven :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPaddedSlot 7 = none

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPaddedSlot_seven :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPaddedSlot
      7 =
    none

Definition10.18.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven selector prepare”. The physical three-qubit PREPARE, flattened with the repository's declared little-endian convention.

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 physical three-qubit PREPARE, flattened with the repository's declared little-endian convention.

Declaration kind. def.

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

Lean code for Definition10.18.18●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare :
  Matrix (Fin 8) (Fin 8) ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare :
  Matrix (Fin 8) (Fin 8) ℂ

The physical three-qubit PREPARE, flattened with the repository's declared
little-endian convention.

Theorem10.18.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven selector prepare unitary flat”; 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/PaperSevenPrepare.lean:124. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare_unitary_flat :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare ∈
    Matrix.unitaryGroup (Fin 8) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare_unitary_flat :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare ∈
    Matrix.unitaryGroup (Fin 8) ℂ

Theorem10.18.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform seven prepare probability”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem uses probabilities directly, so no arbitrary clean-column phase convention for '1 / sqrt 7' enters the LCU proof.

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 theorem uses probabilities directly, so no arbitrary clean-column phase convention for '1 / sqrt 7' enters the LCU proof.

Declaration kind. theorem.

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

Lean code for Theorem10.18.20●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepare_probability
  (slot : Fin 8) :
  star
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare
          slot 0) *
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare slot
        0 =
    if ↑slot < 7 then 1 / 7 else 0

theorem QuantumBlockEncoding.Robin.warmRobinUniformSevenPrepare_probability
  (slot : Fin 8) :
  star
        (QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare
          slot 0) *
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare
        slot 0 =
    if ↑slot < 7 then 1 / 7 else 0

The theorem uses probabilities directly, so no arbitrary clean-column
phase convention for `1 / sqrt 7` enters the LCU proof.