QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

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

noncomputable def mottonenConditionalAngles : PrimitiveBasis 1 → ExactAngle :=
  StatePreparationPaperEntryCertificates.mottonenConditionalAngles

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 :=
  StatePreparationPaperEntryCertificates.mottonenDenseUcryCircuit

commit-pinned source · Verso Blueprint panel

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

noncomputable def mottonenDensePrimitiveCircuit : PrimitiveCircuit 2 :=
  [PrimitiveGate.ry (1 : Fin 2) ryAngle513] ++ mottonenDenseUcryCircuit

commit-pinned source · Verso Blueprint panel

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

noncomputable def mottonenRootState : StateVector (gridSize 2) ℂ :=
  (5 / 13 : ℂ) • basisKet (gridSize 2) (0 : Fin 4) +
    (12 / 13 : ℂ) • basisKet (gridSize 2) (2 : Fin 4)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen root ry col zero”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenRootRy_col_zero :
    (evalPrimitiveCircuitLE [PrimitiveGate.ry (1 : Fin 2) ryAngle513]).col
        (0 : Fin 4) = mottonenRootState := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen root ry prepares”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenRootRy_prepares :
    applyVec
        (evalPrimitiveCircuitLE [PrimitiveGate.ry (1 : Fin 2) ryAngle513])
        (zeroKet 2) = mottonenRootState := by

commit-pinned source · Verso Blueprint panel

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

theorem mottonenDenseUcry_on_root :
    applyVec (evalPrimitiveCircuitLE mottonenDenseUcryCircuit) mottonenRootState =
      mottonenDenseState := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense primitive prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDensePrimitive_prepares_target :
    applyVec (evalPrimitiveCircuitLE mottonenDensePrimitiveCircuit) (zeroKet 2) =
      mottonenDenseTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def mottonenDensePrimitiveRoute :
    ExactPrimitiveStatePreparationRoute 2 where
  target := mottonenDenseTarget
  circuit := mottonenDensePrimitiveCircuit
  normalizationProof := mottonenDenseTarget_normalized
  preparationProof := mottonenDensePrimitive_prepares_target

commit-pinned source · Verso Blueprint panel

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

theorem mottonenDenseVerified_cost :
    mottonenDensePrimitiveRoute.cost =
      { auxiliaryQubits := 0, gateCount := 5, depth := 4, oracleCalls := 0 } := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “zero angle compiled ucry eval eq one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem zeroAngleCompiledUcry_eval_eq_one
    {qubits controls : Nat}
    (wires : Fin controls → Fin qubits) (target : Fin qubits)
    (distinct : ∀ control, wires control ≠ target) :
    evalPrimitiveCircuit
        (compileUniformlyControlledRy controls wires target distinct
          (fun _ => ryAngleZero)) = 1 := 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 :=
  StatePreparationPaperEntryCertificates.sparseControlWire

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 : PrimitiveBasis 1 → ExactAngle :=
  StatePreparationPaperEntryCertificates.sparseConditionalAngles

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 :=
  StatePreparationPaperEntryCertificates.sparsePrunedUcryCircuit

commit-pinned source · Verso Blueprint panel

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

noncomputable def sparsePrunedCircuit : PrimitiveCircuit 3 :=
  [PrimitiveGate.ry (2 : Fin 3) ryAngle513] ++ sparsePrunedUcryCircuit

commit-pinned source · Verso Blueprint panel

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

noncomputable def sparseRootState : StateVector (gridSize 3) ℂ :=
  (5 / 13 : ℂ) • basisKet (gridSize 3) (0 : Fin 8) +
    (12 / 13 : ℂ) • basisKet (gridSize 3) (4 : Fin 8)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse root ry col zero”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseRootRy_col_zero :
    (evalPrimitiveCircuitLE [PrimitiveGate.ry (2 : Fin 3) ryAngle513]).col
        (0 : Fin 8) = sparseRootState := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse root ry prepares”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseRootRy_prepares :
    applyVec
        (evalPrimitiveCircuitLE [PrimitiveGate.ry (2 : Fin 3) ryAngle513])
        (zeroKet 3) = sparseRootState := by

commit-pinned source · Verso Blueprint panel

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

theorem sparsePrunedUcry_on_root :
    applyVec (evalPrimitiveCircuitLE sparsePrunedUcryCircuit) sparseRootState = sparseThreeState := by

commit-pinned source · Verso Blueprint panel

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

theorem sparsePruned_prepares_target :
    applyVec (evalPrimitiveCircuitLE sparsePrunedCircuit) (zeroKet 3) =
      sparseThreeTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def sparsePrunedRoute : ExactPrimitiveStatePreparationRoute 3 where
  target := sparseThreeTarget
  circuit := sparsePrunedCircuit
  normalizationProof := sparseThreeTarget_normalized
  preparationProof := sparsePruned_prepares_target

commit-pinned source · Verso Blueprint panel

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

def sparseDenseControlWires : Fin 2 → Fin 3
  | ⟨0, _⟩ => 1
  | _ => 2

commit-pinned source · Verso Blueprint panel

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

theorem sparseDenseControlWires_ne_target :
    ∀ control, sparseDenseControlWires control ≠ (0 : Fin 3) := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def sparseZeroFillCircuit : PrimitiveCircuit 3 :=
  compileUniformlyControlledRy 2 sparseDenseControlWires (0 : Fin 3)
    sparseDenseControlWires_ne_target (fun _ => ryAngleZero)

commit-pinned source · Verso Blueprint panel

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

noncomputable def sparseDenseTreeCircuit : PrimitiveCircuit 3 :=
  sparsePrunedCircuit ++ sparseZeroFillCircuit

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse zero fill eval eq one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseZeroFill_eval_eq_one :
    evalPrimitiveCircuit sparseZeroFillCircuit = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse zero fill eval le eq one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseZeroFill_evalLE_eq_one :
    evalPrimitiveCircuitLE sparseZeroFillCircuit = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse dense tree eval le eq pruned”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseDenseTree_evalLE_eq_pruned :
    evalPrimitiveCircuitLE sparseDenseTreeCircuit =
      evalPrimitiveCircuitLE sparsePrunedCircuit := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse dense tree prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseDenseTree_prepares_target :
    applyVec (evalPrimitiveCircuitLE sparseDenseTreeCircuit) (zeroKet 3) =
      sparseThreeTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse dense tree route”.

noncomputable def sparseDenseTreeRoute : ExactPrimitiveStatePreparationRoute 3 where
  target := sparseThreeTarget
  circuit := sparseDenseTreeCircuit
  normalizationProof := sparseThreeTarget_normalized
  preparationProof := sparseDenseTree_prepares_target

commit-pinned source · Verso Blueprint panel

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

theorem sparsePrunedVerified_cost :
    sparsePrunedRoute.cost =
      { auxiliaryQubits := 0, gateCount := 5, depth := 4, oracleCalls := 0 } := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse dense tree verified cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseDenseTreeVerified_cost :
    sparseDenseTreeRoute.cost =
      { auxiliaryQubits := 0, gateCount := 15, depth := 13, oracleCalls := 0 } := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse pruned better than dense tree”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparsePruned_betterThan_denseTree :
    sparsePrunedRoute.cost.betterThan sparseDenseTreeRoute.cost := by

commit-pinned source · Verso Blueprint panel