QuantumBlockEncoding/Robin/PaperSevenT3.lean

This definition gives the library's named construction or computation for “warm robin paper seven selector prepare program”.

noncomputable def warmRobinPaperSevenSelectorPrepareProgram :
    PrimitiveProgram 8 where
  circuit := warmRobinPaperSevenSelectorPrepareCircuit
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven selector prepare program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenSelectorPrepareProgram_eval :
    evalPrimitiveProgram warmRobinPaperSevenSelectorPrepareProgram =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinPaperSevenBitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinPaperSevenFullSystem)
          warmRobinPaperSevenSelectorPrepare) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive program”. Chronological exact primitive source program.

noncomputable def warmRobinPaperSevenPrimitiveProgram : PrimitiveProgram 8 :=
  PrimitiveProgram.seq warmRobinPaperSevenSelectorPrepareProgram
    (PrimitiveProgram.seq warmRobinPaperSevenAmplitudeProgram
      (PrimitiveProgram.seq warmRobinPaperSevenSelectProgram
        warmRobinPaperSevenSelectorPrepareProgram.dagger))

/-- Required T3 semantic root.  Equality includes the exact accumulated global
phase and uses the actual reversible extension on dirty `q7`. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven primitive eval eq logical”; the hypotheses and conclusion in the code panel fix its exact scope. Required T3 semantic root.

theorem warmRobinPaperSevenPrimitive_eval_eq_logical :
    evalPrimitiveProgram warmRobinPaperSevenPrimitiveProgram =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinPaperSevenBitsEquiv.symm
        warmRobinPaperSevenWorkspaceLogicalUnitary := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven bits equiv encode”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinPaperSevenBitsEquiv_encode
    (coefficient : Fin 2) (selector : Fin 8)
    (system : WarmRobinPaperSevenFullSystem) :
    warmRobinPaperSevenBitsEquiv
        (warmRobinPaperSevenEncodeBits coefficient selector system) =
      (coefficient, (selector, system)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive flat unitary”. Flat eight-qubit unitary used by the operator-first block-encoding API.

noncomputable def warmRobinPaperSevenPrimitiveFlatUnitary :
    _root_.Matrix (Fin (gridSize 8)) (Fin (gridSize 8)) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 8)
    (evalPrimitiveProgram warmRobinPaperSevenPrimitiveProgram)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven primitive flat unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenPrimitiveFlatUnitary_unitary :
    warmRobinPaperSevenPrimitiveFlatUnitary ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 8)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive clean index”.

noncomputable def warmRobinPaperSevenPrimitiveCleanIndex
    (system : Fin 8) : Fin (gridSize 8) :=
  primitiveBasisLEEquiv 8
    (warmRobinPaperSevenEncodeBits 0 0 (system, 0))

/-- The physical primitive program has the exact `M/224 = A/(56/3)` clean
block; no numerical matrix comparison is used. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven primitive clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The physical primitive program has the exact 'M/224 = A/(56/3)' clean block; no numerical matrix comparison is used.

theorem warmRobinPaperSevenPrimitive_cleanBlock (row column : Fin 8) :
    warmRobinPaperSevenPrimitiveFlatUnitary
        (warmRobinPaperSevenPrimitiveCleanIndex row)
        (warmRobinPaperSevenPrimitiveCleanIndex column) =
      ((RobinEvolution.warmRobinTarget row column /
        RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive block contains target”.

def warmRobinPaperSevenPrimitiveBlockContainsTarget : Prop :=
  ∀ row column : Fin 8,
    warmRobinPaperSevenPrimitiveFlatUnitary
        (warmRobinPaperSevenPrimitiveCleanIndex row)
        (warmRobinPaperSevenPrimitiveCleanIndex column) =
      warmRobinQueryTarget.operator row column /
        warmRobinQueryTarget.normalizer

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven primitive block contains target proof”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenPrimitiveBlockContainsTarget_proof :
    warmRobinPaperSevenPrimitiveBlockContainsTarget := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven full system equiv workspace”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenFullSystemEquiv_workspace
    (slot : Fin 8) (system : WarmRobinPaperSevenFullSystem) :
    (warmRobinPaperSevenFullSystemEquiv slot system).2 = system.2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven primitive workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix-level workspace restoration: a clean input column has no amplitude on a dirty workspace output row.

theorem warmRobinPaperSevenPrimitive_workspaceClean
    (row column : PrimitiveBasis 8)
    (columnClean : column 7 = 0) (rowDirty : row 7 ≠ 0) :
    evalPrimitiveProgram warmRobinPaperSevenPrimitiveProgram row column = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive presentation”.

noncomputable def warmRobinPaperSevenPrimitivePresentation : Circuit :=
  warmRobinPaperSevenPrimitiveProgram.circuit.map fun gate =>
    match gate with
    | .x target => .oneQubit "X" target.val
    | .ry target _ => .rotationY target.val "exact-angle"
    | .rz target _ => .rotationZ target.val "exact-angle"
    | .cx control target _ => .cnot control.val target.val

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive resource”.

noncomputable def warmRobinPaperSevenPrimitiveResource : Resource :=
  warmRobinPaperSevenPrimitiveProgram.resource

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven primitive resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenPrimitive_resource_faithful :
    warmRobinPaperSevenPrimitiveResource =
      warmRobinPaperSevenPrimitiveProgram.circuit.resource := rfl

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive operator candidate”.

noncomputable def warmRobinPaperSevenPrimitiveOperatorCandidate :
    OperatorBlockEncodingCandidate ℂ 3 where
  auxiliaryQubits := 5
  target := warmRobinQueryTarget
  unitary := warmRobinPaperSevenPrimitiveFlatUnitary
  layout := {
    systemQubits := 3
    signalQubits := 4
    pureAncillas := 1
  }
  circuit := warmRobinPaperSevenPrimitivePresentation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive refinement”.

noncomputable def warmRobinPaperSevenPrimitiveRefinement :
    PrimitiveProgramRefinement 8 where
  program := warmRobinPaperSevenPrimitiveProgram
  target := _root_.Matrix.reindexAlgEquiv ℂ ℂ
    warmRobinPaperSevenBitsEquiv.symm
    warmRobinPaperSevenWorkspaceLogicalUnitary
  exact := warmRobinPaperSevenPrimitive_eval_eq_logical

/-- Exact primitive verified block encoding for the paper-seven source route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven primitive verified block encoding”. Exact primitive verified block encoding for the paper-seven source route.

noncomputable def warmRobinPaperSevenPrimitiveVerifiedBlockEncoding :
    VerifiedOperatorBlockEncoding ℂ 3 where
  candidate := warmRobinPaperSevenPrimitiveOperatorCandidate
  unitaryProof := warmRobinPaperSevenPrimitiveFlatUnitary_unitary
  blockProof := warmRobinPaperSevenPrimitiveBlockContainsTarget_proof

commit-pinned source · Verso Blueprint panel