QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean

This definition gives the library's named construction or computation for “mottonen conditional angles”.

noncomputable def mottonenConditionalAngles (bits : PrimitiveBasis 1) : ExactAngle :=
  if bits 0 = 0 then ryAngle35 else ryAngle513

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mottonen dense ucry circuit”.

noncomputable def mottonenDenseUcryCircuit : PrimitiveCircuit 2 :=
  compileUniformlyControlledRy 1 groverRudolphControlWire (0 : Fin 2)
    groverRudolphControlWire_ne_target mottonenConditionalAngles

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense ucry entry zero of context ne”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseUcry_entry_zero_of_context_ne
    (row column : Fin (gridSize 2))
    (contextNe :
      (splitPrimitiveWire (0 : Fin 2) (primitiveLEBits 2 row)).2 ≠
        (splitPrimitiveWire (0 : Fin 2) (primitiveLEBits 2 column)).2) :
    evalPrimitiveCircuitLE mottonenDenseUcryCircuit row column = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense ucry entry 00”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseUcry_entry_00 :
    evalPrimitiveCircuitLE mottonenDenseUcryCircuit (0 : Fin 4) (0 : Fin 4) =
      (3 : ℂ) / 5 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense ucry entry 10”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseUcry_entry_10 :
    evalPrimitiveCircuitLE mottonenDenseUcryCircuit (1 : Fin 4) (0 : Fin 4) =
      (4 : ℂ) / 5 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense ucry entry 22”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseUcry_entry_22 :
    evalPrimitiveCircuitLE mottonenDenseUcryCircuit (2 : Fin 4) (2 : Fin 4) =
      (5 : ℂ) / 13 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense ucry entry 32”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseUcry_entry_32 :
    evalPrimitiveCircuitLE mottonenDenseUcryCircuit (3 : Fin 4) (2 : Fin 4) =
      (12 : ℂ) / 13 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse control wire”.

def sparseControlWire : Fin 1 → Fin 3 := fun _ => 2

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse control wire ne target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseControlWire_ne_target :
    ∀ control, sparseControlWire control ≠ (1 : Fin 3) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse conditional angles”.

noncomputable def sparseConditionalAngles (bits : PrimitiveBasis 1) : ExactAngle :=
  if bits 0 = 0 then ryAngle35 else ryAngleZero

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse pruned ucry circuit”.

noncomputable def sparsePrunedUcryCircuit : PrimitiveCircuit 3 :=
  compileUniformlyControlledRy 1 sparseControlWire (1 : Fin 3)
    sparseControlWire_ne_target sparseConditionalAngles

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse pruned ucry entry zero of context ne”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparsePrunedUcry_entry_zero_of_context_ne
    (row column : Fin (gridSize 3))
    (contextNe :
      (splitPrimitiveWire (1 : Fin 3) (primitiveLEBits 3 row)).2 ≠
        (splitPrimitiveWire (1 : Fin 3) (primitiveLEBits 3 column)).2) :
    evalPrimitiveCircuitLE sparsePrunedUcryCircuit row column = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse pruned ucry entry 00”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparsePrunedUcry_entry_00 :
    evalPrimitiveCircuitLE sparsePrunedUcryCircuit (0 : Fin 8) (0 : Fin 8) =
      (3 : ℂ) / 5 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse pruned ucry entry 20”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparsePrunedUcry_entry_20 :
    evalPrimitiveCircuitLE sparsePrunedUcryCircuit (2 : Fin 8) (0 : Fin 8) =
      (4 : ℂ) / 5 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse pruned ucry entry 44”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparsePrunedUcry_entry_44 :
    evalPrimitiveCircuitLE sparsePrunedUcryCircuit (4 : Fin 8) (4 : Fin 8) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse pruned ucry entry 64”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparsePrunedUcry_entry_64 :
    evalPrimitiveCircuitLE sparsePrunedUcryCircuit (6 : Fin 8) (4 : Fin 8) = 0 := by

commit-pinned source · Verso Blueprint panel