This definition gives the library's named construction or computation for “qubit dim”. A finite-dimensional basis size for an 'n'-qubit register.
def qubitDim (qubits : Nat) : Nat :=
gridSize qubits
/--
Structured semantic obligation for the matrix layer.
This mirrors `GHL2025.ObligationRecord` without importing `GHL2025`, so the
semantics backend can stay below paper-specific files in the import graph.
-/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “semantic obligation”. A proposition-valued field is a requirement until a constructor supplies it. Structured semantic obligation for the matrix layer.
structure SemanticObligation where
description : String
source : String
proved : Bool := false
deriving Repr, DecidableEq
/--
One gate together with its matrix on the full `qubits`-qubit Hilbert space.
The matrix is supplied by a lower-level certificate for the gate family.
-/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “gate matrix”. A proposition-valued field is a requirement until a constructor supplies it. One gate together with its matrix on the full 'qubits'-qubit Hilbert space.
structure GateMatrix (α : Type u) (qubits : Nat) where
gate : Gate
matrix : Matrix (qubitDim qubits) (qubitDim qubits) α
unitary : SemanticObligation
/-- Check that a list of gate matrices labels exactly the same circuit gates. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “gate matrices match circuit”. Check that a list of gate matrices labels exactly the same circuit gates.
def gateMatricesMatchCircuit {α : Type u} {qubits : Nat} :
Circuit → List (GateMatrix α qubits) → Bool
| [], [] => true
| gate :: circuitTail, gateMatrix :: matrixTail =>
gateMatrix.gate == gate && gateMatricesMatchCircuit circuitTail matrixTail
| _, _ => false
/--
Evaluate a list of full-space gate matrices to a circuit matrix.
The fold uses the usual right-action convention for a circuit list
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “eval gate matrices”. Evaluate a list of full-space gate matrices to a circuit matrix.
def evalGateMatrices {α : Type u} [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α] {qubits : Nat}
(gates : List (GateMatrix α qubits)) :
Matrix (qubitDim qubits) (qubitDim qubits) α :=
gates.foldl (fun acc gateMatrix => Matrix.mul gateMatrix.matrix acc)
(Matrix.identity (qubitDim qubits) α)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with foldl add mul”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one symbolic matrix-product entry as a concrete finite Rat fold.
theorem evalWith_foldl_add_mul
(env : String → Rat) {rows mid cols : Nat}
(A : Matrix rows mid Coeff) (B : Matrix mid cols Coeff)
(i : Fin rows) (j : Fin cols) (ks : List (Fin mid)) (acc : Coeff) :
Coeff.evalWith env
(ks.foldl (fun acc k => acc + A i k * B k j) acc) =
ks.foldl
(fun acc k => acc + Coeff.evalWith env (A i k) *
Coeff.evalWith env (B k j))
(Coeff.evalWith env acc) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with mul apply”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one entry of 'Matrix.mul' by evaluating each path contribution.
theorem evalWith_mul_apply
(env : String → Rat) {rows mid cols : Nat}
(A : Matrix rows mid Coeff) (B : Matrix mid cols Coeff)
(i : Fin rows) (j : Fin cols) :
Coeff.evalWith env (Matrix.mul A B i j) =
(List.finRange mid).foldl
(fun acc k => acc + Coeff.evalWith env (A i k) *
Coeff.evalWith env (B k j))
0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with mul eq zero of all paths zero”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry as zero when every evaluated path contribution is zero.
theorem evalWith_mul_eq_zero_of_all_paths_zero
(env : String → Rat) {rows mid cols : Nat}
(A : Matrix rows mid Coeff) (B : Matrix mid cols Coeff)
(i : Fin rows) (j : Fin cols)
(hzero : ∀ k : Fin mid,
Coeff.evalWith env (A i k) * Coeff.evalWith env (B k j) = 0) :
Coeff.evalWith env (Matrix.mul A B i j) = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with mul unique path”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry when all evaluated paths except 'k0' vanish.
theorem evalWith_mul_unique_path
(env : String → Rat) {rows mid cols : Nat}
(A : Matrix rows mid Coeff) (B : Matrix mid cols Coeff)
(i : Fin rows) (j : Fin cols) (k0 : Fin mid)
(hzero : ∀ k : Fin mid, k ≠ k0 →
Coeff.evalWith env (A i k) * Coeff.evalWith env (B k j) = 0) :
Coeff.evalWith env (Matrix.mul A B i j) =
Coeff.evalWith env (A i k0) * Coeff.evalWith env (B k0 j) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with mul two path”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry when all evaluated paths except 'k0' and 'k1' vanish.
theorem evalWith_mul_two_path
(env : String → Rat) {rows mid cols : Nat}
(A : Matrix rows mid Coeff) (B : Matrix mid cols Coeff)
(i : Fin rows) (j : Fin cols) (k0 k1 : Fin mid)
(hk0_ne_k1 : k0 ≠ k1)
(hzero : ∀ k : Fin mid, k ≠ k0 → k ≠ k1 →
Coeff.evalWith env (A i k) * Coeff.evalWith env (B k j) = 0) :
Coeff.evalWith env (Matrix.mul A B i j) =
Coeff.evalWith env (A i k0) * Coeff.evalWith env (B k0 j) +
Coeff.evalWith env (A i k1) * Coeff.evalWith env (B k1 j) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with mul identity right apply”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating a symbolic matrix after multiplying on the right by the identity recovers the evaluated entry.
theorem evalWith_mul_identity_right_apply
(env : String → Rat) {n : Nat}
(A : Matrix n n Coeff) (i j : Fin n) :
Coeff.evalWith env (Matrix.mul A (Matrix.identity n Coeff) i j) =
Coeff.evalWith env (A i j) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cast square apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry-level bridge for square matrix casts along a dimension equality.
theorem cast_square_apply {α : Type u} {m n : Nat} (h : m = n)
(M : Matrix m m α) (i j : Fin n) :
(((cast (by rw [h]) M) : Matrix n n α) i j) =
M ⟨i.val, by subst h; exact i.isLt⟩
⟨j.val, by subst h; exact j.isLt⟩ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval with eval gate matrices single”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluation-level single-gate reduction for 'evalGateMatrices'.
theorem evalWith_evalGateMatrices_single
(env : String → Rat) {qubits : Nat}
(gateMatrix : GateMatrix Coeff qubits)
(i j : Fin (qubitDim qubits)) :
Coeff.evalWith env ((evalGateMatrices [gateMatrix]) i j) =
Coeff.evalWith env (gateMatrix.matrix i j) := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “circuit matrix semantics”. A proposition-valued field is a requirement until a constructor supplies it. Circuit-level matrix semantics assembled from gate-level matrices.
structure CircuitMatrixSemantics (α : Type u) [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α] (qubits : Nat) where
circuit : Circuit
gateMatrices : List (GateMatrix α qubits)
gateListMatches : gateMatricesMatchCircuit circuit gateMatrices = true
matrix : Matrix (qubitDim qubits) (qubitDim qubits) α
matrix_eq_eval : Matrix.PointwiseEq matrix (evalGateMatrices gateMatrices)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “of gate matrices”. Build circuit semantics directly from aligned gate matrices.
def ofGateMatrices {α : Type u} [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α] {qubits : Nat}
(circuit : Circuit) (gateMatrices : List (GateMatrix α qubits))
(h : gateMatricesMatchCircuit circuit gateMatrices = true) :
CircuitMatrixSemantics α qubits where
circuit := circuit
gateMatrices := gateMatrices
gateListMatches := h
matrix := evalGateMatrices gateMatrices
matrix_eq_eval := by intro _ _; rfl
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “prepared circuit entry target”. A proposition-valued field is a requirement until a constructor supplies it. Typed target for relating an active circuit-matrix entry to a prepared composition entry.
structure PreparedCircuitEntryTarget
(α : Type u) (activeDim preparedDim : Nat) where
activeMatrix : Matrix activeDim activeDim α
preparedMatrix : Matrix preparedDim preparedDim α
activeRow : Fin activeDim
activeCol : Fin activeDim
preparedRow : Fin preparedDim
preparedCol : Fin preparedDim
activeEntry : α
activeEntry_eq : activeEntry = activeMatrix activeRow activeCol
preparedEntry : α
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “entry equality statement”. The prepared-composition equality required by the target.
def entryEqualityStatement {α : Type u} {activeDim preparedDim : Nat}
(target : PreparedCircuitEntryTarget α activeDim preparedDim) : Prop :=
target.activeEntry = target.preparedEntry
/-- The same equality stated directly on the backing matrices. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “matrix entry equality statement”. The same equality stated directly on the backing matrices.
def matrixEntryEqualityStatement {α : Type u} {activeDim preparedDim : Nat}
(target : PreparedCircuitEntryTarget α activeDim preparedDim) : Prop :=
target.activeMatrix target.activeRow target.activeCol =
target.preparedMatrix target.preparedRow target.preparedCol
/--
The cached entry equality is equivalent to the backing matrix-entry equality.
Paper-specific targets can prove whichever side their local backend exposes
without changing the semantic obligation being tracked.
-/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “entry equality statement iff matrix entry equality statement”; the hypotheses and conclusion in the code panel fix its exact scope. The cached entry equality is equivalent to the backing matrix-entry equality.
theorem entryEqualityStatement_iff_matrixEntryEqualityStatement
{α : Type u} {activeDim preparedDim : Nat}
(target : PreparedCircuitEntryTarget α activeDim preparedDim) :
target.entryEqualityStatement ↔
target.matrixEntryEqualityStatement := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “circuit block encoding claim”. A proposition-valued field is a requirement until a constructor supplies it. A circuit-level block encoding claim bundling a circuit matrix semantics with a block extraction target and a dimension compatibility proof.
structure CircuitBlockEncodingClaim (α : Type u) [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α]
(qubits : Nat) (dim signalDim : Nat) where
semantics : CircuitMatrixSemantics α qubits
target : BlockExtractionTarget α dim dim signalDim
dimCompat : qubitDim qubits = signalDim * dim
blockCorrect : SemanticObligation
/--
Typed contract for a finite-dimensional LCU/block-composition step.
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “finite block composition contract”. A proposition-valued field is a requirement until a constructor supplies it. Typed contract for a finite-dimensional LCU/block-composition step.
structure FiniteBlockCompositionContract (α : Type u) [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α]
(qubits dim signalDim : Nat) where
sourceAnchor : String
lcuSourceAnchor : String
theoremAnchor : String
claim : CircuitBlockEncodingClaim α qubits dim signalDim
expectedTarget : BlockExtractionTarget α dim dim signalDim
targetMatrix : Matrix dim dim α
normalizer : α
claimTargetMatches : claim.target = expectedTarget
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “signal system block row index”. Compound row index for a signal value and a system-row index.
def signalSystemBlockRowIndex (rows : Nat) (signalIdx systemIdx : Nat) : Nat :=
signalIdx * rows + systemIdx
/-- Compound column index for a signal value and a system-column index. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “signal system block col index”. Compound column index for a signal value and a system-column index.
def signalSystemBlockColIndex (cols : Nat) (signalIdx systemIdx : Nat) : Nat :=
signalIdx * cols + systemIdx
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “signal system block row index zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem signalSystemBlockRowIndex_zero (rows systemIdx : Nat) :
signalSystemBlockRowIndex rows 0 systemIdx = systemIdx := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “signal system block col index zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem signalSystemBlockColIndex_zero (cols systemIdx : Nat) :
signalSystemBlockColIndex cols 0 systemIdx = systemIdx := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “signal system block row index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The row compound index stays inside a signal × row matrix.
theorem signalSystemBlockRowIndex_lt {signalDim rows : Nat}
(signalIdx : Fin signalDim) (i : Fin rows) :
signalSystemBlockRowIndex rows signalIdx.val i.val < signalDim * rows := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “signal system block col index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The column compound index stays inside a signal × column matrix.
theorem signalSystemBlockColIndex_lt {signalDim cols : Nat}
(signalIdx : Fin signalDim) (j : Fin cols) :
signalSystemBlockColIndex cols signalIdx.val j.val < signalDim * cols := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “signal system block projection”. Block projection: extract the '(signalIdx, signalIdx)' block from a signal × system matrix.
def signalSystemBlockProjection {α : Type u} [OfNat α 0]
(signalDim rows cols : Nat)
(M : Matrix (signalDim * rows) (signalDim * cols) α)
(signalIdx : Fin signalDim) :
Matrix rows cols α :=
fun i j =>
M ⟨signalSystemBlockRowIndex rows signalIdx.val i.val,
signalSystemBlockRowIndex_lt signalIdx i⟩
⟨signalSystemBlockColIndex cols signalIdx.val j.val,
signalSystemBlockColIndex_lt signalIdx j⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “signal system block projection apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem signalSystemBlockProjection_apply {α : Type u} [OfNat α 0]
{signalDim rows cols : Nat}
(M : Matrix (signalDim * rows) (signalDim * cols) α)
(signalIdx : Fin signalDim) (i : Fin rows) (j : Fin cols) :
signalSystemBlockProjection signalDim rows cols M signalIdx i j =
M ⟨signalSystemBlockRowIndex rows signalIdx.val i.val,
signalSystemBlockRowIndex_lt signalIdx i⟩
⟨signalSystemBlockColIndex cols signalIdx.val j.val,
signalSystemBlockColIndex_lt signalIdx j⟩ := rfl
/--
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “total circuit qubits”. Total qubits needed for a circuit operating on 'system' system qubits and 'signal' signal qubits.
def totalCircuitQubits (system signal : Nat) : Nat :=
system + signal
/--
Build a BlockExtractionTarget from a CircuitMatrixSemantics by computing
the block projection. The circuit matrix is square with dimension
`signalDim * dim`, and we extract the `(signalIdx, signalIdx)` block.
-/
commit-pinned source · Verso Blueprint panel