QuantumBlockEncoding/BlockEncodingClassics.lean

This definition gives the library's named construction or computation for “perm matrix”. Permutation-matrix entries for a finite basis map.

def permMatrix {n : Nat} (p : Fin n -> Fin n) : Matrix n n Rat :=
  fun row col => if row = p col then 1 else 0

/-- Column inner products for rational matrix-level orthogonality checks. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “column inner”. Column inner products for rational matrix-level orthogonality checks.

def columnInner {n : Nat} (U : Matrix n n Rat) (i j : Fin n) : Rat :=
  (List.finRange n).foldl (fun acc k => acc + U k i * U k j) 0

/-- Row inner products for rational matrix-level orthogonality checks. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “row inner”. Row inner products for rational matrix-level orthogonality checks.

def rowInner {n : Nat} (U : Matrix n n Rat) (i j : Fin n) : Rat :=
  (List.finRange n).foldl (fun acc k => acc + U i k * U j k) 0

/--
Rational orthogonality predicate for real-valued finite matrix backends:
`U^T U = I` and `U U^T = I`, expressed entrywise.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “is rational orthogonal”. Rational orthogonality predicate for real-valued finite matrix backends: 'U^T U = I' and 'U U^T = I', expressed entrywise.

def IsRationalOrthogonal {n : Nat} (U : Matrix n n Rat) : Prop :=
  (∀ i j : Fin n, columnInner U i j = Matrix.identity n Rat i j) ∧
    (∀ i j : Fin n, rowInner U i j = Matrix.identity n Rat i j)

/-- Clean block induced by an embedding of the system basis into a larger basis. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “clean block by”. Clean block induced by an embedding of the system basis into a larger basis.

def cleanBlockBy {system total : Nat} (embed : Fin system -> Fin total)
    (U : Matrix total total Rat) : Matrix system system Rat :=
  fun row col => U (embed row) (embed col)

/--
Canonical product-register embedding.  If the full Hilbert basis is represented
as `ancilla × system`, this maps `(a, s)` to the flattened index
`a * system + s`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “product index”. Canonical product-register embedding.

def productIndex {ancilla system : Nat} (a : Fin ancilla) (s : Fin system) :
    Fin (ancilla * system) :=
  ⟨a.val * system + s.val, by
    have hspos : 0 < system := Nat.lt_of_le_of_lt (Nat.zero_le s.val) s.isLt
    have hlt : a.val * system + s.val < (a.val + 1) * system := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “clean block product”. Clean block for a flattened 'ancilla × system' matrix.

def cleanBlockProduct {ancilla system : Nat} (zero : Fin ancilla)
    (U : Matrix (ancilla * system) (ancilla * system) Rat) :
    Matrix system system Rat :=
  cleanBlockBy (productIndex zero) U

/--
Core `BE.PermMatrix.CleanBlock` leaf: the clean block of a permutation matrix is
just the finite image predicate restricted to clean embedded rows and columns.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean block by perm matrix entry”; the hypotheses and conclusion in the code panel fix its exact scope. Core 'BE.PermMatrix.CleanBlock' leaf: the clean block of a permutation matrix is just the finite image predicate restricted to clean embedded rows and columns.

theorem cleanBlockBy_permMatrix_entry {system total : Nat}
    (embed : Fin system -> Fin total) (p : Fin total -> Fin total)
    (row col : Fin system) :
    cleanBlockBy embed (permMatrix p) row col =
      if embed row = p (embed col) then 1 else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean block product perm matrix entry”; the hypotheses and conclusion in the code panel fix its exact scope. Product-register version of 'cleanBlockBy_permMatrix_entry'.

theorem cleanBlockProduct_permMatrix_entry {ancilla system : Nat}
    (zero : Fin ancilla) (p : Fin (ancilla * system) -> Fin (ancilla * system))
    (row col : Fin system) :
    cleanBlockProduct zero (permMatrix p) row col =
      if productIndex zero row = p (productIndex zero col) then 1 else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean block by perm matrix eq target of entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise bridge from a finite image calculation to an exact clean block.

theorem cleanBlockBy_permMatrix_eq_target_of_entry {system total : Nat}
    (embed : Fin system -> Fin total) (p : Fin total -> Fin total)
    (A : Matrix system system Rat)
    (h :
      forall row col : Fin system,
        (if embed row = p (embed col) then 1 else 0) = A row col) :
    Matrix.PointwiseEq (cleanBlockBy embed (permMatrix p)) A := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean block product eq target of entry”; the hypotheses and conclusion in the code panel fix its exact scope. Pointwise extension principle for product-register clean blocks.

theorem cleanBlockProduct_eq_target_of_entry {ancilla system : Nat}
    (zero : Fin ancilla) (p : Fin (ancilla * system) -> Fin (ancilla * system))
    (A : Matrix system system Rat)
    (h :
      forall row col : Fin system,
        (if productIndex zero row = p (productIndex zero col) then 1 else 0) =
          A row col) :
    Matrix.PointwiseEq (cleanBlockProduct zero (permMatrix p)) A := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “kronecker rat”. Kronecker delta over the project-local rational matrix backend.

def kroneckerRat {n : Nat} (i j : Fin n) : Rat :=
  if i = j then 1 else 0

/--
Column one-sparse matrix with support map `c`: column `j` has its possible
nonzero entry at row `c j`, with amplitude `amp j`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one sparse matrix”. Column one-sparse matrix with support map 'c': column 'j' has its possible nonzero entry at row 'c j', with amplitude 'amp j'.

def oneSparseMatrix {n : Nat} (c : Fin n -> Fin n) (amp : Fin n -> Rat) :
    Matrix n n Rat :=
  fun row col => amp col * kroneckerRat row (c col)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one sparse matrix entry if”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem oneSparseMatrix_entry_if {n : Nat}
    (c : Fin n -> Fin n) (amp : Fin n -> Rat) (row col : Fin n) :
    oneSparseMatrix c amp row col = if row = c col then amp col else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one sparse from support”; the hypotheses and conclusion in the code panel fix its exact scope. One-sparse reconstruction leaf.

theorem oneSparse_from_support {n : Nat}
    (A : Matrix n n Rat) (c : Fin n -> Fin n)
    (hSupport : forall row col : Fin n, row ≠ c col -> A row col = 0) :
    Matrix.PointwiseEq (oneSparseMatrix c (fun col => A (c col) col)) A := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one sparse certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying one-sparse certificate.

structure OneSparseCertificate (n : Nat) where
  supportMap : Fin n -> Fin n
  target : Matrix n n Rat
  supportProof :
    forall row col : Fin n, row ≠ supportMap col -> target row col = 0

commit-pinned source · Verso Blueprint panel

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

def cleanBlock {n : Nat} (cert : OneSparseCertificate n) : Matrix n n Rat :=
  oneSparseMatrix cert.supportMap (fun col => cert.target (cert.supportMap col) col)

commit-pinned source · Verso Blueprint panel

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

theorem correct {n : Nat} (cert : OneSparseCertificate n) :
    Matrix.PointwiseEq cert.cleanBlock cert.target :=
  oneSparse_from_support cert.target cert.supportMap cert.supportProof

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse column clean entry”. Column sparse clean-entry expression: a finite sum over slot indices of value oracle entries times location deltas.

def sparseColumnCleanEntry {rows cols slots : Nat}
    (loc : Fin cols -> Fin slots -> Fin rows)
    (value : Fin slots -> Fin cols -> Rat) : Matrix rows cols Rat :=
  fun row col =>
    (List.finRange slots).foldl
      (fun acc slot => acc + value slot col * kroneckerRat row (loc col slot))
      0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “perm matrix column inner of injective”; the hypotheses and conclusion in the code panel fix its exact scope. Column Gram entries of a permutation matrix collapse by injectivity.

theorem permMatrix_columnInner_of_injective {n : Nat}
    (p : Fin n -> Fin n) (hp : Function.Injective p) :
    ∀ i j : Fin n,
      columnInner (permMatrix p) i j = Matrix.identity n Rat i j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “perm matrix row inner of bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Row Gram entries of a permutation matrix collapse by bijectivity.

theorem permMatrix_rowInner_of_bijective {n : Nat}
    (p : Fin n -> Fin n)
    (hp : Function.Injective p ∧ Function.Surjective p) :
    ∀ i j : Fin n,
      rowInner (permMatrix p) i j = Matrix.identity n Rat i j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “perm matrix is rational orthogonal of bijective”; the hypotheses and conclusion in the code panel fix its exact scope. A bijective finite image induces a rational orthogonal permutation matrix.

theorem permMatrix_isRationalOrthogonal_of_bijective {n : Nat}
    (p : Fin n -> Fin n)
    (hp : Function.Injective p ∧ Function.Surjective p) :
    IsRationalOrthogonal (permMatrix p) :=
  ⟨permMatrix_columnInner_of_injective p hp.1,
    permMatrix_rowInner_of_bijective p hp⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse column clean entry no hit”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseColumnCleanEntry_no_hit {rows cols slots : Nat}
    (loc : Fin cols -> Fin slots -> Fin rows)
    (value : Fin slots -> Fin cols -> Rat)
    (row : Fin rows) (col : Fin cols)
    (hmiss : forall slot : Fin slots, row ≠ loc col slot) :
    sparseColumnCleanEntry loc value row col = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse column clean entry unique slot”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseColumnCleanEntry_unique_slot {rows cols slots : Nat}
    (loc : Fin cols -> Fin slots -> Fin rows)
    (value : Fin slots -> Fin cols -> Rat)
    (row : Fin rows) (col : Fin cols) (hit : Fin slots)
    (hhit : row = loc col hit)
    (hmiss : forall slot : Fin slots, slot ≠ hit -> row ≠ loc col slot) :
    sparseColumnCleanEntry loc value row col = value hit col := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “row column sparse delta entry”. General row/column sparse delta expression.

def rowColumnSparseDeltaEntry {rows cols slots : Nat}
    (colLoc : Fin cols -> Fin slots -> Fin rows)
    (rowLoc : Fin rows -> Fin slots -> Fin cols)
    (value : Fin rows -> Fin cols -> Rat) : Matrix rows cols Rat :=
  fun row col =>
    (List.finRange slots).foldl
      (fun acc slot =>
        acc +
          (List.finRange slots).foldl
            (fun inner rowSlot =>
              inner +

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “sparse column certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying sparse-column contract.

structure SparseColumnCertificate (rows cols slots : Nat) where
  cleanBlock : Matrix rows cols Rat
  target : Matrix rows cols Rat
  normalizer : Rat
  locationOracle : String
  valueOracle : String
  blockProof : Matrix.PointwiseEq cleanBlock target

commit-pinned source · Verso Blueprint panel

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

theorem correct {rows cols slots : Nat}
    (cert : SparseColumnCertificate rows cols slots) :
    Matrix.PointwiseEq cert.cleanBlock cert.target :=
  cert.blockProof

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “row column sparse certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying row/column sparse contract for the general sparse route.

structure RowColumnSparseCertificate (rows cols slots : Nat) where
  cleanBlock : Matrix rows cols Rat
  target : Matrix rows cols Rat
  normalizer : Rat
  columnOracle : String
  rowOracle : String
  valueOracle : String
  blockProof : Matrix.PointwiseEq cleanBlock target

commit-pinned source · Verso Blueprint panel

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

theorem correct {rows cols slots : Nat}
    (cert : RowColumnSparseCertificate rows cols slots) :
    Matrix.PointwiseEq cert.cleanBlock cert.target :=
  cert.blockProof

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “value to amplitude contract”. A proposition-valued field is a requirement until a constructor supplies it. Value-to-amplitude oracle contract.

structure ValueToAmplitudeContract (rows cols : Nat) where
  cleanAmplitude : Matrix rows cols Rat
  targetAmplitude : Matrix rows cols Rat
  valueOracleDescription : String
  rotationDescription : String
  cleanupStatement : Prop
  cleanupProof : cleanupStatement
  amplitudeProof : Matrix.PointwiseEq cleanAmplitude targetAmplitude

commit-pinned source · Verso Blueprint panel

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

theorem correct {rows cols : Nat} (cert : ValueToAmplitudeContract rows cols) :
    Matrix.PointwiseEq cert.cleanAmplitude cert.targetAmplitude :=
  cert.amplitudeProof

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “is symmetric”. Symmetric matrix predicate for the rational backend.

def IsSymmetric {n : Nat} (A : Matrix n n Rat) : Prop :=
  forall i j : Fin n, A i j = A j i

/-- A symmetric full matrix has a symmetric clean block under any embedding. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean block by symmetric of symmetric”; the hypotheses and conclusion in the code panel fix its exact scope. A symmetric full matrix has a symmetric clean block under any embedding.

theorem cleanBlockBy_symmetric_of_symmetric {system total : Nat}
    (embed : Fin system -> Fin total) (U : Matrix total total Rat)
    (hU : IsSymmetric U) :
    IsSymmetric (cleanBlockBy embed U) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fin 2 zero”. Two-by-two scalar dilation block.

def fin2Zero : Fin 2 := ⟨0, by decide⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fin 2 one”.

def fin2One : Fin 2 := ⟨1, by decide⟩

commit-pinned source · Verso Blueprint panel

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

def scalarDilation (x y : Rat) : Matrix 2 2 Rat :=
  fun row col =>
    if row = fin2Zero ∧ col = fin2Zero then x
    else if row = fin2Zero ∧ col = fin2One then y
    else if row = fin2One ∧ col = fin2Zero then y
    else -x

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem scalarDilation_cleanEntry (x y : Rat) :
    scalarDilation x y fin2Zero fin2Zero = x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation offdiag 01”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem scalarDilation_offdiag01 (x y : Rat) :
    scalarDilation x y fin2Zero fin2One = y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation offdiag 10”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem scalarDilation_offdiag10 (x y : Rat) :
    scalarDilation x y fin2One fin2Zero = y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation diag 11”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem scalarDilation_diag11 (x y : Rat) :
    scalarDilation x y fin2One fin2One = -x := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “scalar dilation row dot”. Two-entry row dot product for the scalar dilation block.

def scalarDilationRowDot (x y : Rat) (rowA rowB : Fin 2) : Rat :=
  scalarDilation x y rowA fin2Zero * scalarDilation x y rowB fin2Zero +
    scalarDilation x y rowA fin2One * scalarDilation x y rowB fin2One

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation row 0 norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem scalarDilation_row0_normSq (x y : Rat) :
    scalarDilationRowDot x y fin2Zero fin2Zero = x * x + y * y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation row 1 norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem scalarDilation_row1_normSq (x y : Rat) :
    scalarDilationRowDot x y fin2One fin2One = x * x + y * y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation row 0 unit norm of”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem scalarDilation_row0_unit_norm_of (x y : Rat)
    (hunit : x * x + y * y = 1) :
    scalarDilationRowDot x y fin2Zero fin2Zero = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation row 1 unit norm of”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem scalarDilation_row1_unit_norm_of (x y : Rat)
    (hunit : x * x + y * y = 1) :
    scalarDilationRowDot x y fin2One fin2One = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation rows 01 orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem scalarDilation_rows01_orthogonal (x y : Rat) :
    scalarDilationRowDot x y fin2Zero fin2One = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “scalar dilation rows 10 orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem scalarDilation_rows10_orthogonal (x y : Rat) :
    scalarDilationRowDot x y fin2One fin2Zero = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “chebyshev t”. Chebyshev polynomial values, kept as a small executable recurrence.

def chebyshevT : Nat -> Rat -> Rat
  | 0, _ => 1
  | 1, x => x
  | n + 2, x => 2 * x * chebyshevT (n + 1) x - chebyshevT n x

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem chebyshevT_zero (x : Rat) : chebyshevT 0 x = 1 := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem chebyshevT_one (x : Rat) : chebyshevT 1 x = x := rfl

commit-pinned source · Verso Blueprint panel

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

theorem chebyshevT_two (x : Rat) : chebyshevT 2 x = 2 * x * x - 1 := rfl

commit-pinned source · Verso Blueprint panel

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

theorem chebyshevT_succ_succ (n : Nat) (x : Rat) :
    chebyshevT (n + 2) x = 2 * x * chebyshevT (n + 1) x - chebyshevT n x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “chebyshev t three recurrence”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem chebyshevT_three_recurrence (x : Rat) :
    chebyshevT 3 x = 2 * x * (2 * x * x - 1) - x := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “chebyshev t four recurrence”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem chebyshevT_four_recurrence (x : Rat) :
    chebyshevT 4 x = 2 * x * chebyshevT 3 x - chebyshevT 2 x := rfl

/--
Proof-carrying exact clean-block package.  This is smaller than the full
operator-candidate record and is intended for reusable theorem arithmetic.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “exact clean block”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying exact clean-block package.

structure ExactCleanBlock (system total : Nat) where
  U : Matrix total total Rat
  A : Matrix system system Rat
  embed : Fin system -> Fin total
  blockProof : Matrix.PointwiseEq (cleanBlockBy embed U) A

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “clean”. The certified clean block associated with a proof-carrying package.

def clean {system total : Nat} (cert : ExactCleanBlock system total) :
    Matrix system system Rat :=
  cleanBlockBy cert.embed cert.U

commit-pinned source · Verso Blueprint panel

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

theorem clean_eq_target {system total : Nat}
    (cert : ExactCleanBlock system total) :
    Matrix.PointwiseEq cert.clean cert.A :=
  cert.blockProof

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “qubitization chebyshev contract”. A proposition-valued field is a requirement until a constructor supplies it. Qubitization/Chebyshev proof-carrying contract.

structure QubitizationChebyshevContract (system total : Nat) where
  input : ExactCleanBlock system total
  degree : Nat
  output : Matrix system system Rat
  sideConditions : Prop
  chebyshevStatement : Prop
  sideConditionProof : sideConditions
  chebyshevProof : chebyshevStatement

/--
Abstract partial-permutation certificate.  A concrete task supplies the

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “partial permutation certificate”. Abstract partial-permutation certificate.

def partialPermutationCertificate {system total : Nat}
    (embed : Fin system -> Fin total) (p : Fin total -> Fin total)
    (A : Matrix system system Rat)
    (h :
      forall row col : Fin system,
        (if embed row = p (embed col) then 1 else 0) = A row col) :
    ExactCleanBlock system total where
  U := permMatrix p
  A := A
  embed := embed
  blockProof := cleanBlockBy_permMatrix_eq_target_of_entry embed p A h

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term lcu”. One-term LCU leaf.

def oneTermLCU (A : Matrix system system Rat) : Matrix system system Rat :=
  A

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term lcu clean block”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem oneTermLCU_cleanBlock (A : Matrix system system Rat) :
    Matrix.PointwiseEq (oneTermLCU A) A := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “matrix scale”. Pointwise scalar multiplication for the project-local matrix backend.

def matrixScale (c : Rat) (A : Matrix rows cols Rat) : Matrix rows cols Rat :=
  fun row col => c * A row col

/-- Pointwise addition for the project-local matrix backend. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “matrix add”. Pointwise addition for the project-local matrix backend.

def matrixAdd (A B : Matrix rows cols Rat) : Matrix rows cols Rat :=
  fun row col => A row col + B row col

/-- Two-term weighted sum, the finite clean-block algebra behind a 2-term LCU. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “weighted sum 2”. Two-term weighted sum, the finite clean-block algebra behind a 2-term LCU.

def weightedSum2 (leftWeight rightWeight : Rat)
    (left right : Matrix rows cols Rat) : Matrix rows cols Rat :=
  fun row col => leftWeight * left row col + rightWeight * right row col

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “weighted sum 2 entry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem weightedSum2_entry {rows cols : Nat}
    (leftWeight rightWeight : Rat)
    (left right : Matrix rows cols Rat) (row : Fin rows) (col : Fin cols) :
    weightedSum2 leftWeight rightWeight left right row col =
      leftWeight * left row col + rightWeight * right row col := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “weighted sum 2 congr pointwise”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem weightedSum2_congr_pointwise {rows cols : Nat}
    {A A' B B' : Matrix rows cols Rat}
    (leftWeight rightWeight : Rat)
    (hA : Matrix.PointwiseEq A A') (hB : Matrix.PointwiseEq B B') :
    Matrix.PointwiseEq
      (weightedSum2 leftWeight rightWeight A B)
      (weightedSum2 leftWeight rightWeight A' B') := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “lcu certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying LCU contract.

structure LCUCertificate (system : Nat) where
  cleanBlock : Matrix system system Rat
  target : Matrix system system Rat
  normalizer : Rat
  termCount : Nat
  blockProof : Matrix.PointwiseEq cleanBlock target

commit-pinned source · Verso Blueprint panel

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

theorem correct {system : Nat} (cert : LCUCertificate system) :
    Matrix.PointwiseEq cert.cleanBlock cert.target :=
  cert.blockProof

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “two term lcu certificate”. Two-term LCU arithmetic after both selected clean blocks have already been proved.

def twoTermLCUCertificate {system : Nat}
    (left right : LCUCertificate system)
    (leftWeight rightWeight : Rat) : LCUCertificate system where
  cleanBlock := weightedSum2 leftWeight rightWeight left.cleanBlock right.cleanBlock
  target := weightedSum2 leftWeight rightWeight left.target right.target
  normalizer := leftWeight * left.normalizer + rightWeight * right.normalizer
  termCount := left.termCount + right.termCount
  blockProof :=
    weightedSum2_congr_pointwise leftWeight rightWeight
      left.blockProof right.blockProof

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “two term lcu certificate clean block entry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem twoTermLCUCertificate_cleanBlock_entry {system : Nat}
    (left right : LCUCertificate system)
    (leftWeight rightWeight : Rat)
    (row col : Fin system) :
    (twoTermLCUCertificate left right leftWeight rightWeight).cleanBlock row col =
      leftWeight * left.target row col + rightWeight * right.target row col := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “to lcu certificate”. Promote an exact clean-block certificate to the LCU-style arithmetic layer.

def ExactCleanBlock.toLCUCertificate {system total : Nat}
    (cert : ExactCleanBlock system total) (normalizer : Rat := 1) :
    LCUCertificate system where
  cleanBlock := cert.clean
  target := cert.A
  normalizer := normalizer
  termCount := 1
  blockProof := cert.blockProof

/--
Product arithmetic at the exact clean-block level.  This is the shared proof

commit-pinned source · Verso Blueprint panel

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

theorem matrix_mul_congr_pointwise {rows mid cols : Nat}
    {A A' : Matrix rows mid Rat} {B B' : Matrix mid cols Rat}
    (hA : Matrix.PointwiseEq A A') (hB : Matrix.PointwiseEq B B') :
    Matrix.PointwiseEq (Matrix.mul A B) (Matrix.mul A' B') := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “product clean block certificate”. Exact product certificate for already-extracted clean blocks.

def productCleanBlockCertificate {rows : Nat}
    (left : LCUCertificate rows) -- target square case used by current tasks
    (right : LCUCertificate rows) :
    LCUCertificate rows where
  cleanBlock := Matrix.mul left.cleanBlock right.cleanBlock
  target := Matrix.mul left.target right.target
  normalizer := left.normalizer * right.normalizer
  termCount := left.termCount * right.termCount
  blockProof := matrix_mul_congr_pointwise left.blockProof right.blockProof

/-- Product bridge for exact clean-block certificates via the arithmetic layer. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “product exact clean block certificate”. Product bridge for exact clean-block certificates via the arithmetic layer.

def productExactCleanBlockCertificate {system totalLeft totalRight : Nat}
    (left : ExactCleanBlock system totalLeft)
    (right : ExactCleanBlock system totalRight) : LCUCertificate system :=
  productCleanBlockCertificate
    (ExactCleanBlock.toLCUCertificate left)
    (ExactCleanBlock.toLCUCertificate right)

/-- Tensor-style resource score: parallel depth is the maximum of two depths. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “tensor resource cost”. Tensor-style resource score: parallel depth is the maximum of two depths.

def tensorResourceCost (x y : BlockEncodingCost) : BlockEncodingCost where
  auxiliaryQubits := x.auxiliaryQubits + y.auxiliaryQubits
  gateCount := x.gateCount + y.gateCount
  depth := max x.depth y.depth
  oracleCalls := x.oracleCalls + y.oracleCalls

commit-pinned source · Verso Blueprint panel

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

theorem tensorResourceCost_gateCount (x y : BlockEncodingCost) :
    (tensorResourceCost x y).gateCount = x.gateCount + y.gateCount := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “tensor resource cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem tensorResourceCost_depth (x y : BlockEncodingCost) :
    (tensorResourceCost x y).depth = max x.depth y.depth := rfl

/-- Product-style resource score: sequential depth adds. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “product resource cost”. Product-style resource score: sequential depth adds.

def productResourceCost (x y : BlockEncodingCost) : BlockEncodingCost where
  auxiliaryQubits := x.auxiliaryQubits + y.auxiliaryQubits
  gateCount := x.gateCount + y.gateCount
  depth := x.depth + y.depth
  oracleCalls := x.oracleCalls + y.oracleCalls

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “product resource cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem productResourceCost_depth (x y : BlockEncodingCost) :
    (productResourceCost x y).depth = x.depth + y.depth := rfl

/--
Hermitian-dilation target shape.  The complete block-matrix construction will
live in a richer matrix backend; the important reusable Lean leaf is that a
non-Hermitian target is explicitly converted into a named downstream target,
not silently treated as Hermitian.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “hermitian dilation contract”. A proposition-valued field is a requirement until a constructor supplies it. Hermitian-dilation target shape.

structure HermitianDilationContract (n : Nat) where
  source : Matrix n n Rat
  dilation : Matrix (2 * n) (2 * n) Rat
  entryFormula : Prop
  entryProof : entryFormula

/--
QSVT consumer contract.  QSVT is deliberately downstream of a proved block
encoding: this record cannot be built without an input block certificate.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “qsvt consumer contract”. A proposition-valued field is a requirement until a constructor supplies it. QSVT consumer contract.

structure QSVTConsumerContract (system total : Nat) where
  input : ExactCleanBlock system total
  polynomialDescription : String
  sideConditions : Prop
  outputStatement : Prop
  sideConditionProof : sideConditions
  outputProof : outputStatement

/-- Zero-error approximate incumbent at the clean-block level. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “zero error approx clean block”. A proposition-valued field is a requirement until a constructor supplies it. Zero-error approximate incumbent at the clean-block level.

structure ZeroErrorApproxCleanBlock (system total : Nat) where
  exact : ExactCleanBlock system total
  epsilon : Rat := 0
  approximationBound : Prop :=
    Matrix.PointwiseEq (cleanBlockBy exact.embed exact.U) exact.A
  approximationProof : approximationBound

/--
Any exact clean-block certificate can be used as a zero-error approximate
incumbent in the adaptive exact-to-approximate ABEIS policy.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “exact as zero error approx clean block”. Any exact clean-block certificate can be used as a zero-error approximate incumbent in the adaptive exact-to-approximate ABEIS policy.

def exactAsZeroErrorApproxCleanBlock {system total : Nat}
    (cert : ExactCleanBlock system total) :
    ZeroErrorApproxCleanBlock system total where
  exact := cert
  epsilon := 0
  approximationBound := Matrix.PointwiseEq (cleanBlockBy cert.embed cert.U) cert.A
  approximationProof := cert.blockProof

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exact as zero error approx clean block bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem exactAsZeroErrorApproxCleanBlock_bound {system total : Nat}
    (cert : ExactCleanBlock system total) :
    (exactAsZeroErrorApproxCleanBlock cert).approximationBound :=
  cert.blockProof

commit-pinned source · Verso Blueprint panel