QuantumBlockEncoding/SequentialBondPreparation.lean

This abbreviation gives a shorter name to the type or expression used for “core”. A core emits one bit and changes the bond.

abbrev Core (B : Type*) := _root_.Matrix (Fin 2 × B) B ℂ

/-- The square, full local matrix; its nonzero-bit input columns are not
specified by a tensor core and must be supplied by an actual completion. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “stage”. The square, full local matrix; its nonzero-bit input columns are not specified by a tensor core and must be supplied by an actual completion.

abbrev Stage (B : Type*) := _root_.Matrix (Fin 2 × B) (Fin 2 × B) ℂ

/-- State amplitudes after exactly `n` output bits have been emitted. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “bond state”. State amplitudes after exactly 'n' output bits have been emitted.

abbrev BondState (n : Nat) (B : Type*) := PrimitiveBasis n × B → ℂ

/-- Add the next output bit in zero, without changing any existing amplitude. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fresh zero”. Add the next output bit in zero, without changing any existing amplitude.

def freshZero {n : Nat} (v : BondState n B) :
    PrimitiveBasis n × (Fin 2 × B) → ℂ :=
  fun x => if x.2.1 = 0 then v (x.1, x.2.2) else 0

/-- Local stage tensored with the identity on all already emitted bits. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “lift stage”. Local stage tensored with the identity on all already emitted bits.

noncomputable def liftStage (n : Nat) (U : Stage B) :
    _root_.Matrix (PrimitiveBasis n × (Fin 2 × B))
      (PrimitiveBasis n × (Fin 2 × B)) ℂ :=
  (1 : _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ) ⊗ₖ U

omit [Fintype B] [DecidableEq B] in

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem liftStage_apply (n : Nat) (U : Stage B)
    (r c : PrimitiveBasis n × (Fin 2 × B)) :
    liftStage n U r c = if r.1 = c.1 then U r.2 c.2 else 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “step”. A genuine matrix-vector action followed only by a basis regrouping.

noncomputable def step {n : Nat} (U : Stage B) (v : BondState n B) :
    BondState (n + 1) B := fun x =>
  ((liftStage n U).mulVec (freshZero v))
    (Fin.init x.1, (x.1 (Fin.last n), x.2))

omit [DecidableEq B] in
/-- Only the clean-input columns of a local stage affect an emitted state.
The sum over passive prefixes and fresh-bit inputs collapses exactly. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “step apply”; the hypotheses and conclusion in the code panel fix its exact scope. Only the clean-input columns of a local stage affect an emitted state.

theorem step_apply {n : Nat} (U : Stage B) (v : BondState n B)
    (x : PrimitiveBasis (n + 1)) (b : B) :
    step U v (x, b) =
      ∑ a, U (x (Fin.last n), b) (0, a) * v (Fin.init x, a) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “lift stage unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Unitarity of the full local completion gives unitarity after adding arbitrarily many passive emitted wires.

theorem liftStage_unitary (n : Nat) (U : Stage B)
    (hU : U ∈ _root_.Matrix.unitaryGroup (Fin 2 × B) ℂ) :
    liftStage n U ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis n × (Fin 2 × B)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “core slice”. Fixing an emitted bit leaves a bond-to-bond transfer matrix.

def coreSlice (K : Core B) (bit : Fin 2) : _root_.Matrix B B ℂ :=
  fun b a => K (bit, b) a

/-- Chronological tensor contraction. The last emitted core multiplies on
the left, in the same convention as `evalPrimitiveCircuit`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “transfer”. Chronological tensor contraction.

noncomputable def transfer (K : Nat → Core B) :
    (n : Nat) → PrimitiveBasis n → _root_.Matrix B B ℂ
  | 0, _ => 1
  | n + 1, x => coreSlice (K n) (x (Fin.last n)) * transfer K n (Fin.init x)

/-- Explicit initial boundary, followed by sequential matrix actions.
At stage zero there are no output bits and the bond amplitude is `boundary`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “run”. Explicit initial boundary, followed by sequential matrix actions.

noncomputable def run (U : Nat → Stage B) (boundary : B → ℂ) :
    (n : Nat) → BondState n B
  | 0 => fun x => boundary x.2
  | n + 1 => step (U n) (run U boundary n)

/-- Local clean-column equalities suffice to identify the complete state
with the tensor contraction at every length; no global state action is assumed. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run eq transfer”; the hypotheses and conclusion in the code panel fix its exact scope. Local clean-column equalities suffice to identify the complete state with the tensor contraction at every length; no global state action is assumed.

theorem run_eq_transfer (U : Nat → Stage B) (K : Nat → Core B)
    (cleanColumns : ∀ t bit b a, U t (bit, b) (0, a) = K t (bit, b) a)
    (boundary : B → ℂ) (n : Nat) (x : PrimitiveBasis n) (b : B) :
    run U boundary n (x, b) = (transfer K n x).mulVec boundary b := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “basis boundary”. Initial computational-basis boundary for the bond.

def basisBoundary (initial : B) : B → ℂ := fun b => if b = initial then 1 else 0

/-- Starting from a basis boundary extracts the corresponding transfer column. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run basis boundary”; the hypotheses and conclusion in the code panel fix its exact scope. Starting from a basis boundary extracts the corresponding transfer column.

theorem run_basisBoundary (U : Nat → Stage B) (K : Nat → Core B)
    (cleanColumns : ∀ t bit b a, U t (bit, b) (0, a) = K t (bit, b) a)
    (initial : B) (n : Nat) (x : PrimitiveBasis n) (b : B) :
    run U (basisBoundary initial) n (x, b) = transfer K n x b initial := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “transfer boundary supported”; the hypotheses and conclusion in the code panel fix its exact scope. If every core is zero outside the next active bond set, its contracted state has that support.

theorem transfer_boundary_supported (K : Nat → Core B)
    (active : Nat → B → Prop) (boundary : B → ℂ)
    (initialSupport : ∀ b, ¬ active 0 b → boundary b = 0)
    (coreSupport : ∀ t bit b a, ¬ active (t + 1) b → K t (bit, b) a = 0)
    (n : Nat) (x : PrimitiveBasis n) (b : B) (inactive : ¬ active n b) :
    (transfer K n x).mulVec boundary b = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run eq transfer of supported”; the hypotheses and conclusion in the code panel fix its exact scope. Rank-changing version of 'run_eq_transfer': only columns for occupied input bond labels must agree.

theorem run_eq_transfer_of_supported (U : Nat → Stage B) (K : Nat → Core B)
    (active : Nat → B → Prop) (boundary : B → ℂ)
    (initialSupport : ∀ b, ¬ active 0 b → boundary b = 0)
    (coreSupport : ∀ t bit b a, ¬ active (t + 1) b → K t (bit, b) a = 0)
    (cleanColumns : ∀ t bit b a, active t a → U t (bit, b) (0, a) = K t (bit, b) a)
    (n : Nat) (x : PrimitiveBasis n) (b : B) :
    run U boundary n (x, b) = (transfer K n x).mulVec boundary b := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run supported”; the hypotheses and conclusion in the code panel fix its exact scope. No leakage to inactive labels at any intermediate stage.

theorem run_supported (U : Nat → Stage B) (K : Nat → Core B)
    (active : Nat → B → Prop) (boundary : B → ℂ)
    (initialSupport : ∀ b, ¬ active 0 b → boundary b = 0)
    (coreSupport : ∀ t bit b a, ¬ active (t + 1) b → K t (bit, b) a = 0)
    (cleanColumns : ∀ t bit b a, active t a → U t (bit, b) (0, a) = K t (bit, b) a)
    (n : Nat) (x : PrimitiveBasis n) (b : B) (inactive : ¬ active n b) :
    run U boundary n (x, b) = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “terminal core”. A terminal bond of dimension one, embedded at a chosen padded label.

def terminalCore (clean : B) (T : _root_.Matrix (Fin 2) B ℂ) : Core B :=
  fun out a => if out.2 = clean then T out.1 a else 0

/-- Appending a rank-one terminal bond factors the *whole* state as a clean
bond times the contracted output amplitude; this is not a projection theorem. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “step terminal core”; the hypotheses and conclusion in the code panel fix its exact scope. Appending a rank-one terminal bond factors the *whole* state as a clean bond times the contracted output amplitude; this is not a projection theorem.

theorem step_terminalCore {n : Nat} (U : Stage B) (v : BondState n B)
    (clean : B) (T : _root_.Matrix (Fin 2) B ℂ)
    (cleanColumns : ∀ bit b a, U (bit, b) (0, a) = terminalCore clean T (bit, b) a)
    (x : PrimitiveBasis (n + 1)) (b : B) :
    step U v (x, b) = if b = clean then
      ∑ a, T (x (Fin.last n)) a * v (Fin.init x, a) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “step terminal core no leakage”; the hypotheses and conclusion in the code panel fix its exact scope. Zero leakage to every non-clean bond label, with no measurement or postselection.

theorem step_terminalCore_no_leakage {n : Nat} (U : Stage B) (v : BondState n B)
    (clean : B) (T : _root_.Matrix (Fin 2) B ℂ)
    (cleanColumns : ∀ bit b a, U (bit, b) (0, a) = terminalCore clean T (bit, b) a)
    (x : PrimitiveBasis (n + 1)) (b : B) (h : b ≠ clean) :
    step U v (x, b) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “step terminal core of supported”; the hypotheses and conclusion in the code panel fix its exact scope. Padded-register terminal cleanup on the occupied input subspace only.

theorem step_terminalCore_of_supported {n : Nat} (U : Stage B) (v : BondState n B)
    (active : B → Prop) (clean : B) (T : _root_.Matrix (Fin 2) B ℂ)
    (support : ∀ p a, ¬ active a → v (p, a) = 0)
    (cleanColumns : ∀ bit b a, active a →
      U (bit, b) (0, a) = terminalCore clean T (bit, b) a)
    (x : PrimitiveBasis (n + 1)) (b : B) :
    step U v (x, b) = if b = clean then
      ∑ a, T (x (Fin.last n)) a * v (Fin.init x, a) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run terminal clean”; the hypotheses and conclusion in the code panel fix its exact scope. Complete state action after a supported sequential run and one terminal stage.

theorem run_terminal_clean (U : Nat → Stage B) (K : Nat → Core B)
    (active : Nat → B → Prop) (boundary : B → ℂ)
    (initialSupport : ∀ b, ¬ active 0 b → boundary b = 0)
    (coreSupport : ∀ t bit b a, ¬ active (t + 1) b → K t (bit, b) a = 0)
    (cleanColumns : ∀ t bit b a, active t a → U t (bit, b) (0, a) = K t (bit, b) a)
    (n : Nat) (lastU : Stage B) (clean : B) (T : _root_.Matrix (Fin 2) B ℂ)
    (lastColumns : ∀ bit b a, active n a →
      lastU (bit, b) (0, a) = terminalCore clean T (bit, b) a)
    (x : PrimitiveBasis (n + 1)) (b : B) :
    step lastU (run U boundary n) (x, b) = if b = clean then
      ∑ a, T (x (Fin.last n)) a *

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “local basis equiv”. The local primitive circuit uses the low 'q' wires for the bond and its highest wire for the fresh emitted bit.

def localBasisEquiv (q : Nat) : PrimitiveBasis (q + 1) ≃ Fin 2 × PrimitiveBasis q :=
  (lastBasisEquiv q).trans (Equiv.prodComm _ _)

/-- Exact local stage supplied by a primitive circuit, not an opaque oracle. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “circuit stage”. Exact local stage supplied by a primitive circuit, not an opaque oracle.

noncomputable def circuitStage {q : Nat} (c : PrimitiveCircuit (q + 1)) :
    Stage (PrimitiveBasis q) :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ (localBasisEquiv q) (evalPrimitiveCircuit c)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem circuitStage_apply {q : Nat} (c : PrimitiveCircuit (q + 1))
    (bit bit' : Fin 2) (b a : PrimitiveBasis q) :
    circuitStage c (bit, b) (bit', a) =
      evalPrimitiveCircuit c (Fin.snoc b bit) (Fin.snoc a bit') := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “circuit stage unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Primitive stages have checked full unitarity, independently of whether their active columns implement the intended tensor cores.

theorem circuitStage_unitary {q : Nat} (c : PrimitiveCircuit (q + 1)) :
    circuitStage c ∈ _root_.Matrix.unitaryGroup (Fin 2 × PrimitiveBasis q) ℂ :=
  Robin.ComplexLCU.reindex_unitary _ _ (evalPrimitiveCircuit_unitary c)

/-- Direct instantiation with primitive-circuit stages. The sole compiler
alignment premise is stated on active clean-input columns, in actual
`evalPrimitiveCircuit` semantics. This does not synthesize these circuits or
prove a gate-count bound. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run circuit stages eq transfer”; the hypotheses and conclusion in the code panel fix its exact scope. Direct instantiation with primitive-circuit stages.

theorem run_circuitStages_eq_transfer {q : Nat}
    (circuits : Nat → PrimitiveCircuit (q + 1)) (K : Nat → Core (PrimitiveBasis q))
    (active : Nat → PrimitiveBasis q → Prop) (boundary : PrimitiveBasis q → ℂ)
    (initialSupport : ∀ b, ¬ active 0 b → boundary b = 0)
    (coreSupport : ∀ t bit b a, ¬ active (t + 1) b → K t (bit, b) a = 0)
    (compilerColumns : ∀ t bit b a, active t a →
      evalPrimitiveCircuit (circuits t) (Fin.snoc b bit) (Fin.snoc a 0) = K t (bit, b) a)
    (n : Nat) (x : PrimitiveBasis n) (b : PrimitiveBasis q) :
    run (fun t => circuitStage (circuits t)) boundary n (x, b) =
      (transfer K n x).mulVec boundary b := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude mass”. Sum of amplitude squared moduli, represented as a complex scalar with zero imaginary part.

noncomputable def amplitudeMass {I : Type*} [Fintype I] (v : I → ℂ) : ℂ :=
  ∑ i, star (v i) * v i

/-- Full unitary matrix action preserves total amplitude mass. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude mass mul vec”; the hypotheses and conclusion in the code panel fix its exact scope. Full unitary matrix action preserves total amplitude mass.

theorem amplitudeMass_mulVec {I : Type*} [Fintype I] [DecidableEq I]
    (M : _root_.Matrix I I ℂ) (v : I → ℂ)
    (hM : M ∈ _root_.Matrix.unitaryGroup I ℂ) :
    amplitudeMass (M.mulVec v) = amplitudeMass v := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude mass fresh zero”; the hypotheses and conclusion in the code panel fix its exact scope. Introducing a zero bit is norm-preserving, not a postselection.

theorem amplitudeMass_freshZero {n : Nat} (v : BondState n B) :
    amplitudeMass (freshZero v) = amplitudeMass v := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “step basis equiv”. The regrouping of passive prefix, newly emitted bit, and bond labels.

def stepBasisEquiv (n : Nat) (B : Type*) :
    PrimitiveBasis (n + 1) × B ≃ PrimitiveBasis n × (Fin 2 × B) :=
  (Equiv.prodCongr (lastBasisEquiv n) (Equiv.refl B)).trans
    (Equiv.prodAssoc _ _ _)

/-- Sequential stages preserve total mass even when their occupied bond
subspaces have different dimensions. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude mass step”; the hypotheses and conclusion in the code panel fix its exact scope. Sequential stages preserve total mass even when their occupied bond subspaces have different dimensions.

theorem amplitudeMass_step {n : Nat} (U : Stage B) (v : BondState n B)
    (hU : U ∈ _root_.Matrix.unitaryGroup (Fin 2 × B) ℂ) :
    amplitudeMass (step U v) = amplitudeMass v := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude mass run”; the hypotheses and conclusion in the code panel fix its exact scope. Full sequential action is norm-preserving for every length.

theorem amplitudeMass_run (U : Nat → Stage B) (boundary : B → ℂ)
    (unitary : ∀ t, U t ∈ _root_.Matrix.unitaryGroup (Fin 2 × B) ℂ) (n : Nat) :
    amplitudeMass (run U boundary n) = amplitudeMass boundary := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude mass run basis boundary”; the hypotheses and conclusion in the code panel fix its exact scope. A unitary sequential run starting at one bond basis label has total probability one at every stage.

theorem amplitudeMass_run_basisBoundary (U : Nat → Stage B) (initial : B)
    (unitary : ∀ t, U t ∈ _root_.Matrix.unitaryGroup (Fin 2 × B) ℂ) (n : Nat) :
    amplitudeMass (run U (basisBoundary initial) n) = 1 := by

commit-pinned source · Verso Blueprint panel