QuantumBlockEncoding/Robin/Figure4Loaders.lean

This definition gives the library's named construction or computation for “warm robin paper literal boundary angle”.

noncomputable def warmRobinPaperLiteralBoundaryAngle
    (coefficient : Rat) : Real :=
  Real.arccos (coefficient : Real)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin executable standard ry boundary angle”.

noncomputable def warmRobinExecutableStandardRyBoundaryAngle
    (coefficient : Rat) : Real :=
  2 * Real.arccos (coefficient : Real)

/--
Corrected reading of Eq. (27) for the standard quantum-computing `R_y`
convention.  The displayed single-`arccos` expression in arXiv:2506.20478 is
retained above only as a literal transcript of the source typo.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin corrected eq 27 boundary angle”. Corrected reading of Eq.

noncomputable def warmRobinCorrectedEq27BoundaryAngle
    (coefficient : Rat) : Real :=
  2 * Real.arccos (coefficient : Real)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin corrected eq 27 boundary angle eq executable”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinCorrectedEq27BoundaryAngle_eq_executable
    (coefficient : Rat) :
    warmRobinCorrectedEq27BoundaryAngle coefficient =
      warmRobinExecutableStandardRyBoundaryAngle coefficient := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin corrected eq 27 standard ry clean amplitude”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinCorrectedEq27_standardRy_cleanAmplitude
    (coefficient : Rat)
    (lower : (-1 : Real) ≤ (coefficient : Real))
    (upper : (coefficient : Real) ≤ 1) :
    standardRyMatrix (warmRobinCorrectedEq27BoundaryAngle coefficient) =
      ComplexLCU.amplitudeRotation (coefficient : Real) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin boundary angle zero guard”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinBoundaryAngle_zero_guard :
    warmRobinPaperLiteralBoundaryAngle 0 = Real.pi / 2 ∧
      warmRobinExecutableStandardRyBoundaryAngle 0 = Real.pi := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bulk coefficient abs le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BulkCoefficient_abs_le_one (slot : Fin 8) :
    |((warmRobinFigure4BulkCoefficient slot : Rat) : Real)| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 source coefficient abs le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4SourceCoefficient_abs_le_one
    (slot column : Fin 8) :
    |((warmRobinFigure4SourceCoefficient slot column : Rat) : Real)| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk control wires”.

def warmRobinFigure4BulkControlWires : Fin 4 → Fin 9
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | _ => 7

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bulk control wires ne target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BulkControlWires_ne_target
    (wire : Fin 4) :
    warmRobinFigure4BulkControlWires wire ≠ (6 : Fin 9) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk control slot”.

def warmRobinFigure4BulkControlSlot (bits : PrimitiveBasis 4) : Fin 8 :=
  ⟨(bits 0).val + 2 * (bits 1).val + 4 * (bits 2).val, by omega⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk loader angle”.

noncomputable def warmRobinFigure4BulkLoaderAngle
    (bits : PrimitiveBasis 4) : ExactAngle :=
  if bits 3 = 1 then
    .twiceArccosRational
      (warmRobinFigure4BulkCoefficient
        (warmRobinFigure4BulkControlSlot bits))
      (warmRobinFigure4BulkCoefficient_abs_le_one _)
  else .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bulk loader ry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BulkLoaderRy
    (bits : PrimitiveBasis 4) :
    standardRyMatrix (warmRobinFigure4BulkLoaderAngle bits).eval =
      if bits 3 = 1 then
        ComplexLCU.amplitudeRotation
          (((warmRobinFigure4BulkCoefficient
            (warmRobinFigure4BulkControlSlot bits) : Rat) : Real))
      else 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk loader circuit”.

noncomputable def warmRobinFigure4BulkLoaderCircuit : PrimitiveCircuit 9 :=
  compileUniformlyControlledRy 4 warmRobinFigure4BulkControlWires 6
    warmRobinFigure4BulkControlWires_ne_target
    warmRobinFigure4BulkLoaderAngle

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk loader program”.

noncomputable def warmRobinFigure4BulkLoaderProgram : PrimitiveProgram 9 where
  circuit := warmRobinFigure4BulkLoaderCircuit
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bulk loader program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BulkLoaderProgram_eval :
    evalPrimitiveProgram warmRobinFigure4BulkLoaderProgram =
      controlledRyBlockMatrix warmRobinFigure4BulkControlWires 6
        warmRobinFigure4BulkControlWires_ne_target
        warmRobinFigure4BulkLoaderAngle := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4BoundaryControlWires : Fin 7 → Fin 9
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | 3 => 3
  | 4 => 4
  | 5 => 5
  | _ => 7

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 boundary control wires ne target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BoundaryControlWires_ne_target
    (wire : Fin 7) :
    warmRobinFigure4BoundaryControlWires wire ≠ (6 : Fin 9) := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4BoundaryControlSlot (bits : PrimitiveBasis 7) : Fin 8 :=
  ⟨(bits 0).val + 2 * (bits 1).val + 4 * (bits 2).val, by omega⟩

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4BoundaryControlColumn (bits : PrimitiveBasis 7) : Fin 8 :=
  ⟨(bits 3).val + 2 * (bits 4).val + 4 * (bits 5).val, by omega⟩

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinFigure4BoundaryLoaderAngle
    (bits : PrimitiveBasis 7) : ExactAngle :=
  if bits 6 = 0 ∧
      ¬ warmRobinFigure4TransposeBulk
        (warmRobinFigure4BoundaryControlColumn bits) then
    .twiceArccosRational
      (warmRobinFigure4SourceCoefficient
        (warmRobinFigure4BoundaryControlSlot bits)
        (warmRobinFigure4BoundaryControlColumn bits))
      (warmRobinFigure4SourceCoefficient_abs_le_one _ _)
  else .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 boundary loader ry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BoundaryLoaderRy
    (bits : PrimitiveBasis 7) :
    standardRyMatrix (warmRobinFigure4BoundaryLoaderAngle bits).eval =
      if bits 6 = 0 ∧
          ¬ warmRobinFigure4TransposeBulk
            (warmRobinFigure4BoundaryControlColumn bits) then
        ComplexLCU.amplitudeRotation
          (((warmRobinFigure4SourceCoefficient
            (warmRobinFigure4BoundaryControlSlot bits)
            (warmRobinFigure4BoundaryControlColumn bits) : Rat) : Real))
      else 1 := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinFigure4BoundaryLoaderCircuit : PrimitiveCircuit 9 :=
  compileUniformlyControlledRy 7 warmRobinFigure4BoundaryControlWires 6
    warmRobinFigure4BoundaryControlWires_ne_target
    warmRobinFigure4BoundaryLoaderAngle

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinFigure4BoundaryLoaderProgram : PrimitiveProgram 9 where
  circuit := warmRobinFigure4BoundaryLoaderCircuit
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 boundary loader program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BoundaryLoaderProgram_eval :
    evalPrimitiveProgram warmRobinFigure4BoundaryLoaderProgram =
      controlledRyBlockMatrix warmRobinFigure4BoundaryControlWires 6
        warmRobinFigure4BoundaryControlWires_ne_target
        warmRobinFigure4BoundaryLoaderAngle := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 derivative loader program”.

noncomputable def warmRobinFigure4DerivativeLoaderProgram : PrimitiveProgram 9 :=
  PrimitiveProgram.seq warmRobinFigure4BulkLoaderProgram
    warmRobinFigure4BoundaryLoaderProgram

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 derivative loader program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4DerivativeLoaderProgram_eval :
    evalPrimitiveProgram warmRobinFigure4DerivativeLoaderProgram =
      controlledRyBlockMatrix warmRobinFigure4BoundaryControlWires 6
          warmRobinFigure4BoundaryControlWires_ne_target
          warmRobinFigure4BoundaryLoaderAngle *
        controlledRyBlockMatrix warmRobinFigure4BulkControlWires 6
          warmRobinFigure4BulkControlWires_ne_target
          warmRobinFigure4BulkLoaderAngle := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4IndicatorValue (column : Fin 8) : Fin 2 :=
  if warmRobinFigure4TransposeBulk column then 1 else 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 bulk control input”.

def warmRobinFigure4BulkControlInput
    (slot : Fin 8) (indicator : Fin 2) : PrimitiveBasis 4
  | ⟨0, _⟩ => primitiveBits3LE slot 0
  | ⟨1, _⟩ => primitiveBits3LE slot 1
  | ⟨2, _⟩ => primitiveBits3LE slot 2
  | _ => indicator

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4BoundaryControlInput
    (slot column : Fin 8) (indicator : Fin 2) : PrimitiveBasis 7
  | ⟨0, _⟩ => primitiveBits3LE slot 0
  | ⟨1, _⟩ => primitiveBits3LE slot 1
  | ⟨2, _⟩ => primitiveBits3LE slot 2
  | ⟨3, _⟩ => primitiveBits3LE column 0
  | ⟨4, _⟩ => primitiveBits3LE column 1
  | ⟨5, _⟩ => primitiveBits3LE column 2
  | _ => indicator

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bulk control slot input”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BulkControlSlot_input
    (slot : Fin 8) (indicator : Fin 2) :
    warmRobinFigure4BulkControlSlot
      (warmRobinFigure4BulkControlInput slot indicator) = slot := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bulk control input indicator”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BulkControlInput_indicator
    (slot : Fin 8) (indicator : Fin 2) :
    warmRobinFigure4BulkControlInput slot indicator 3 = indicator := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 boundary control slot input”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BoundaryControlSlot_input
    (slot column : Fin 8) (indicator : Fin 2) :
    warmRobinFigure4BoundaryControlSlot
      (warmRobinFigure4BoundaryControlInput slot column indicator) = slot := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 boundary control column input”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BoundaryControlColumn_input
    (slot column : Fin 8) (indicator : Fin 2) :
    warmRobinFigure4BoundaryControlColumn
      (warmRobinFigure4BoundaryControlInput slot column indicator) = column := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 boundary control input indicator”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BoundaryControlInput_indicator
    (slot column : Fin 8) (indicator : Fin 2) :
    warmRobinFigure4BoundaryControlInput slot column indicator 6 = indicator := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 derivative loader clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4DerivativeLoader_cleanEntry
    (slot column : Fin 8) :
    let indicator := warmRobinFigure4IndicatorValue column
    let bulk := standardRyMatrix
      (warmRobinFigure4BulkLoaderAngle
        (warmRobinFigure4BulkControlInput slot indicator)).eval
    let boundary := standardRyMatrix
      (warmRobinFigure4BoundaryLoaderAngle
        (warmRobinFigure4BoundaryControlInput slot column indicator)).eval
    (boundary * bulk) 0 0 =
      ((warmRobinFigure4SourceCoefficient slot column : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel