QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

This definition gives the library's named construction or computation for “pad”.

def pad {m : Nat} (c : PrimitiveCircuit m) : (extra : Nat) → PrimitiveCircuit (m + extra)
  | 0 => c
  | extra + 1 => (pad c extra).map liftGate

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pad matrix”.

noncomputable def padMatrix {m : Nat}
    (M : _root_.Matrix (PrimitiveBasis m) (PrimitiveBasis m) ℂ) :
    (extra : Nat) → _root_.Matrix (PrimitiveBasis (m + extra)) (PrimitiveBasis (m + extra)) ℂ
  | 0 => M
  | extra + 1 => liftLastMatrix (padMatrix M extra)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval pad”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem eval_pad {m : Nat} (c : PrimitiveCircuit m) (extra : Nat) :
    evalPrimitiveCircuit (pad c extra) = padMatrix (evalPrimitiveCircuit c) extra := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pad matrix append”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem padMatrix_append {m : Nat}
    (M : _root_.Matrix (PrimitiveBasis m) (PrimitiveBasis m) ℂ)
    (t : Nat) (a b : PrimitiveBasis m) (x y : PrimitiveBasis t) :
    padMatrix M t (Fin.append a x) (Fin.append b y) =
      if x = y then M a b else 0 := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem pad_ryCount {m : Nat} (c : PrimitiveCircuit m) (extra : Nat) :
    (pad c extra).ryCount = c.ryCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pad cx count”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem pad_cxCount {m : Nat} (c : PrimitiveCircuit m) (extra : Nat) :
    (pad c extra).cxCount = c.cxCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pad gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem pad_gateCount {m : Nat} (c : PrimitiveCircuit m) (extra : Nat) :
    (pad c extra).gateCount = c.gateCount := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “stage wires”. Preserve bond indices and send the local fresh bit to the new highest wire.

def stageWires (q t : Nat) : Fin ((q + 1) + t) ≃ Fin ((q + t) + 1) where
  toFun := Fin.addCases
    (Fin.lastCases (Fin.last (q + t)) (fun i => (Fin.castAdd t i).castSucc))
    (fun i => (Fin.natAdd q i).castSucc)
  invFun := Fin.lastCases (Fin.castAdd t (Fin.last q))
    (Fin.addCases (fun i => Fin.castAdd t i.castSucc) (Fin.natAdd (q + 1)))
  left_inv i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “stage wires fresh”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem stageWires_fresh (q t : Nat) :
    stageWires q t (Fin.castAdd t (Fin.last q)) = Fin.last (q + t) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “stage wires bond”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem stageWires_bond (q t : Nat) (i : Fin q) :
    (stageWires q t (Fin.castAdd t i.castSucc)).val = i.val := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “stage wires basis”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem stageWires_basis (q t : Nat) (b : PrimitiveBasis q)
    (x : PrimitiveBasis t) (bit : Fin 2) :
    (fun w : Fin ((q + 1) + t) =>
      (Fin.snoc (Fin.append b x) bit : PrimitiveBasis ((q + t) + 1)) (stageWires q t w)) =
      Fin.append (Fin.snoc b bit) x := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “place stage”.

def placeStage {q : Nat} (t : Nat) (c : PrimitiveCircuit (q + 1)) :
    PrimitiveCircuit ((q + t) + 1) :=
  PrimitiveWireRename.circuit (stageWires q t) (pad c t)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “placed matrix”.

noncomputable def placedMatrix {q : Nat} (t : Nat)
    (M : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℂ) :
    _root_.Matrix (PrimitiveBasis ((q + t) + 1)) (PrimitiveBasis ((q + t) + 1)) ℂ :=
  PrimitiveWireRename.matrix (stageWires q t) (padMatrix M t)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval place stage”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem eval_placeStage {q : Nat} (t : Nat) (c : PrimitiveCircuit (q + 1)) :
    evalPrimitiveCircuit (placeStage t c) = placedMatrix t (evalPrimitiveCircuit c) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “placed matrix apply”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem placedMatrix_apply {q : Nat} (t : Nat)
    (M : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℂ)
    (a b : PrimitiveBasis q) (x y : PrimitiveBasis t) (u v : Fin 2) :
    placedMatrix t M (Fin.snoc (Fin.append a x) u) (Fin.snoc (Fin.append b y) v) =
      if x = y then M (Fin.snoc a u) (Fin.snoc b v) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “place stage ry count”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem placeStage_ryCount {q : Nat} (t : Nat) (c : PrimitiveCircuit (q + 1)) :
    (placeStage t c).ryCount = c.ryCount := by simp [placeStage]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “place stage cx count”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem placeStage_cxCount {q : Nat} (t : Nat) (c : PrimitiveCircuit (q + 1)) :
    (placeStage t c).cxCount = c.cxCount := by simp [placeStage]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “place stage gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem placeStage_gateCount {q : Nat} (t : Nat) (c : PrimitiveCircuit (q + 1)) :
    (placeStage t c).gateCount = c.gateCount := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “assemble”. Assemble one actual primitive list, with each bond stage on its final wires.

def assemble (q : Nat) (stages : Nat → PrimitiveCircuit (q + 1)) :
    (n : Nat) → PrimitiveCircuit (q + n)
  | 0 => []
  | n + 1 => (assemble q stages n).map liftGate ++ placeStage n (stages n)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “assembled matrix”.

noncomputable def assembledMatrix (q : Nat)
    (stages : Nat → PrimitiveCircuit (q + 1)) :
    (n : Nat) → _root_.Matrix (PrimitiveBasis (q + n)) (PrimitiveBasis (q + n)) ℂ
  | 0 => 1
  | n + 1 => placedMatrix n (evalPrimitiveCircuit (stages n)) *
      liftLastMatrix (assembledMatrix q stages n)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval assemble”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem eval_assemble (q : Nat) (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) :
    evalPrimitiveCircuit (assemble q stages n) = assembledMatrix q stages n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “assembled matrix clean column”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem assembledMatrix_clean_column (q : Nat)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat)
    (a b : PrimitiveBasis q) (x : PrimitiveBasis n) :
    assembledMatrix q stages n (Fin.append b x) (Fin.append a (fun _ => 0)) =
      SequentialBondPreparation.run (fun t => SequentialBondPreparation.circuitStage (stages t))
        (SequentialBondPreparation.basisBoundary a) n (x, b) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “assemble clean column”; the hypotheses and conclusion in the code panel fix its exact scope. A flattened primitive circuit has exactly the sequential state action; the fresh data inputs are all zero and every output amplitude is covered.

theorem assemble_clean_column (q : Nat)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat)
    (a b : PrimitiveBasis q) (x : PrimitiveBasis n) :
    evalPrimitiveCircuit (assemble q stages n)
        (Fin.append b x) (Fin.append a (fun _ => 0)) =
      SequentialBondPreparation.run (fun t => SequentialBondPreparation.circuitStage (stages t))
        (SequentialBondPreparation.basisBoundary a) n (x, b) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run boundary decomposition”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem run_boundary_decomposition {q : Nat}
    (U : Nat → SequentialBondPreparation.Stage (PrimitiveBasis q))
    (v : PrimitiveBasis q → ℂ) (n : Nat) (x : PrimitiveBasis n) (b : PrimitiveBasis q) :
    SequentialBondPreparation.run U v n (x, b) =
      ∑ a, SequentialBondPreparation.run U (SequentialBondPreparation.basisBoundary a)
        n (x, b) * v a := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “with initial”. The initial bond vector is prepared by an actual circuit, never supplied as a free state.

def withInitial {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) : PrimitiveCircuit (q + n) :=
  pad initial n ++ assemble q stages n

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “with initial column”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem withInitial_column {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat)
    (a b : PrimitiveBasis q) (x : PrimitiveBasis n) :
    evalPrimitiveCircuit (withInitial initial stages n)
        (Fin.append b x) (Fin.append a (fun _ => 0)) =
      SequentialBondPreparation.run (fun t => SequentialBondPreparation.circuitStage (stages t))
        (fun c => evalPrimitiveCircuit initial c a) n (x, b) := by

commit-pinned source · Verso Blueprint panel

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

theorem assemble_ryCount (q : Nat) (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) :
    (assemble q stages n).ryCount = ∑ t ∈ Finset.range n, (stages t).ryCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “assemble cx count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem assemble_cxCount (q : Nat) (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) :
    (assemble q stages n).cxCount = ∑ t ∈ Finset.range n, (stages t).cxCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “assemble no oracle”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem assemble_noOracle (q : Nat) (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) :
    (assemble q stages n).resource.oracleCalls = 0 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “with initial ry count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem withInitial_ryCount {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) :
    (withInitial initial stages n).ryCount = initial.ryCount +
      ∑ t ∈ Finset.range n, (stages t).ryCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “with initial cx count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem withInitial_cxCount {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) :
    (withInitial initial stages n).cxCount = initial.cxCount +
      ∑ t ∈ Finset.range n, (stages t).cxCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “with initial primitive bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem withInitial_primitive_bound {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n bound : Nat)
    (h : ∀ t < n, (stages t).ryCount + (stages t).cxCount ≤ bound) :
    (withInitial initial stages n).ryCount + (withInitial initial stages n).cxCount ≤
      initial.ryCount + initial.cxCount + n * bound := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “output wires”. Place the first emitted bit at the most-significant data wire, and the bond after the data register.

def outputWires (q n : Nat) : Fin (q + n) ≃ Fin (n + q) where
  toFun := Fin.addCases (Fin.natAdd n) (fun i => Fin.castAdd q i.rev)
  invFun := Fin.addCases (fun i => Fin.natAdd q i.rev) (Fin.castAdd n)
  left_inv i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “output wires basis”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem outputWires_basis (q n : Nat) (b : PrimitiveBasis q) (x : PrimitiveBasis n) :
    (fun w => Fin.append x b (outputWires q n w)) =
      Fin.append b (fun i => x i.rev) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “public circuit”. Physical output convention: low data wires are little-endian, clean bond wires follow them.

def publicCircuit {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat) : PrimitiveCircuit (n + q) :=
  PrimitiveWireRename.circuit (outputWires q n) (withInitial initial stages n)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “public circuit column”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem publicCircuit_column {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n : Nat)
    (a b : PrimitiveBasis q) (x : PrimitiveBasis n) :
    evalPrimitiveCircuit (publicCircuit initial stages n)
        (Fin.append x b) (Fin.append (fun _ => 0) a) =
      SequentialBondPreparation.run (fun t => SequentialBondPreparation.circuitStage (stages t))
        (fun c => evalPrimitiveCircuit initial c a) n ((fun i => x i.rev), b) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “public circuit primitive bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem publicCircuit_primitive_bound {q : Nat} (initial : PrimitiveCircuit q)
    (stages : Nat → PrimitiveCircuit (q + 1)) (n bound : Nat)
    (h : ∀ t < n, (stages t).ryCount + (stages t).cxCount ≤ bound) :
    (publicCircuit initial stages n).ryCount + (publicCircuit initial stages n).cxCount ≤
      initial.ryCount + initial.cxCount + n * bound := by

commit-pinned source · Verso Blueprint panel