QuantumBlockEncoding/CubicAmplitudePrimitive.lean

This definition gives the library's named construction or computation for “cubic n 2 control wires”. The first two wires are system controls and wire two is the clean signal.

def cubicN2ControlWires : Fin 2 → Fin 3
  | 0 => 0
  | _ => 1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 control wires ne signal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicN2ControlWires_ne_signal (wire : Fin 2) :
    cubicN2ControlWires wire ≠ (2 : Fin 3) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 control index”. Decode the two little-endian system controls.

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

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 amplitude abs le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicN2Amplitude_abs_le_one (bits : PrimitiveBasis 2) :
    |((CubicStatePreparation.cubicAmplitude 2
      (cubicN2ControlIndex bits) : Rat) : Real)| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 angle”. Exact standard-RY angle for the selected cubic amplitude.

noncomputable def cubicN2Angle (bits : PrimitiveBasis 2) : ExactAngle :=
  .twiceArccosRational
    (CubicStatePreparation.cubicAmplitude 2 (cubicN2ControlIndex bits))
    (cubicN2Amplitude_abs_le_one bits)

/-- Four-way uniformly controlled rotation, compiled to primitive gates. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive circuit”. Four-way uniformly controlled rotation, compiled to primitive gates.

noncomputable def cubicN2PrimitiveCircuit : PrimitiveCircuit 3 :=
  compileUniformlyControlledRy 2 cubicN2ControlWires 2
    cubicN2ControlWires_ne_signal cubicN2Angle

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive program”.

noncomputable def cubicN2PrimitiveProgram : PrimitiveProgram 3 where
  circuit := cubicN2PrimitiveCircuit
  globalPhase := .rational 0

/-- Exact matrix semantics of the emitted gate list. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive circuit eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact matrix semantics of the emitted gate list.

theorem cubicN2PrimitiveCircuit_eval :
    evalPrimitiveCircuit cubicN2PrimitiveCircuit =
      controlledRyBlockMatrix cubicN2ControlWires 2
        cubicN2ControlWires_ne_signal cubicN2Angle := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicN2PrimitiveProgram_eval :
    evalPrimitiveProgram cubicN2PrimitiveProgram =
      controlledRyBlockMatrix cubicN2ControlWires 2
        cubicN2ControlWires_ne_signal cubicN2Angle := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 encode bits”. Encode a signal value and a two-qubit system index into three named wires.

def cubicN2EncodeBits (signal : Fin 2) (system : Fin 4) : PrimitiveBasis 3
  | 0 => ⟨system.val % 2, by omega⟩
  | 1 => ⟨(system.val / 2) % 2, by omega⟩
  | _ => signal

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 encode bits signal”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem cubicN2EncodeBits_signal (signal : Fin 2) (system : Fin 4) :
    cubicN2EncodeBits signal system 2 = signal := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 control index encode”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem cubicN2ControlIndex_encode
    (signal : Fin 2) (system : Fin 4) :
    cubicN2ControlIndex
        (primitiveControlAssignment cubicN2ControlWires 2
          cubicN2ControlWires_ne_signal
          (splitPrimitiveWire 2 (cubicN2EncodeBits signal system)).2) =
      system := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 encode bits context eq iff”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem cubicN2EncodeBits_context_eq_iff
    (leftSignal rightSignal : Fin 2) (left right : Fin 4) :
    (splitPrimitiveWire 2 (cubicN2EncodeBits leftSignal left)).2 =
        (splitPrimitiveWire 2 (cubicN2EncodeBits rightSignal right)).2 ↔
      left = right := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive program clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The primitive program's clean signal block is exactly the cubic diagonal.

theorem cubicN2PrimitiveProgram_cleanEntry (row column : Fin 4) :
    evalPrimitiveProgram cubicN2PrimitiveProgram
        (cubicN2EncodeBits 0 row) (cubicN2EncodeBits 0 column) =
      ((cubicDiagonalOperator 2 row column : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive flat unitary”. Flat little-endian unitary used by the operator-certificate interface.

noncomputable def cubicN2PrimitiveFlatUnitary :
    _root_.Matrix (Fin (gridSize 3)) (Fin (gridSize 3)) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 3)
    (evalPrimitiveProgram cubicN2PrimitiveProgram)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive flat unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicN2PrimitiveFlatUnitary_unitary :
    cubicN2PrimitiveFlatUnitary ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 3)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive clean index”.

noncomputable def cubicN2PrimitiveCleanIndex (system : Fin 4) : Fin (gridSize 3) :=
  primitiveBasisLEEquiv 3 (cubicN2EncodeBits 0 system)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicN2PrimitiveFlatUnitary_cleanBlock (row column : Fin 4) :
    cubicN2PrimitiveFlatUnitary
        (cubicN2PrimitiveCleanIndex row)
        (cubicN2PrimitiveCleanIndex column) =
      ((cubicDiagonalOperator 2 row column : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 complex target”.

noncomputable def cubicN2ComplexTarget :
    QueryOperatorTarget ℂ (gridSize 2) (gridSize 2) where
  operator := fun row column => ((cubicDiagonalOperator 2 row column : Rat) : ℂ)
  normalizer := 1
  source := "finite two-qubit exact cubic amplitude oracle"
  semanticContract := "clean signal block equals diag((j/4)^3)"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive presentation”.

noncomputable def cubicN2PrimitivePresentation : Circuit :=
  cubicN2PrimitiveCircuit.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 “cubic n 2 primitive resource”.

noncomputable def cubicN2PrimitiveResource : Resource :=
  cubicN2PrimitiveProgram.resource

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive operator candidate”.

noncomputable def cubicN2PrimitiveOperatorCandidate :
    OperatorBlockEncodingCandidate ℂ 2 where
  auxiliaryQubits := 1
  target := cubicN2ComplexTarget
  unitary := cubicN2PrimitiveFlatUnitary
  layout := {
    systemQubits := 2
    signalQubits := 1
    pureAncillas := 0
  }
  circuit := cubicN2PrimitivePresentation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic n 2 primitive verified block encoding”. Exact unitarity and clean-block promotion for the finite cubic route.

noncomputable def cubicN2PrimitiveVerifiedBlockEncoding :
    VerifiedOperatorBlockEncoding ℂ 2 where
  candidate := cubicN2PrimitiveOperatorCandidate
  unitaryProof := cubicN2PrimitiveFlatUnitary_unitary
  blockProof := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. No opaque oracle survives in the accepted primitive resource row.

theorem cubicN2Primitive_oracleCalls_eq_zero :
    cubicN2PrimitiveResource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

/-- Resource ownership is definitional rather than a handwritten tuple. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic n 2 primitive resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. Resource ownership is definitional rather than a handwritten tuple.

theorem cubicN2Primitive_resource_faithful :
    cubicN2PrimitiveResource = cubicN2PrimitiveCircuit.resource := rfl

commit-pinned source · Verso Blueprint panel