QuantumBlockEncoding/Core.lean

This abbreviation gives a shorter name to the type or expression used for “matrix”. A finite matrix represented by its entries.

abbrev Matrix (rows cols : Nat) (α : Type u) := Fin rows -> Fin cols -> α

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pointwise eq”. Pointwise equality for finite matrices.

def PointwiseEq {rows cols : Nat} {α : Type u}
    (a b : Matrix rows cols α) : Prop :=
  ∀ i j, a i j = b i j

/-- The zero finite matrix. -/

commit-pinned source · Verso Blueprint panel

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

def zero (rows cols : Nat) (α : Type u) [OfNat α 0] : Matrix rows cols α :=
  fun _ _ => 0

/-- The identity finite matrix. -/

commit-pinned source · Verso Blueprint panel

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

def identity (n : Nat) (α : Type u) [OfNat α 0] [OfNat α 1] :
    Matrix n n α :=
  fun i j => if i = j then 1 else 0

/-- Finite matrix multiplication with the project-local `Matrix` representation. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mul”. Finite matrix multiplication with the project-local 'Matrix' representation.

def mul {rows mid cols : Nat} {α : Type u}
    [OfNat α 0] [HAdd α α α] [HMul α α α]
    (a : Matrix rows mid α) (b : Matrix mid cols α) :
    Matrix rows cols α :=
  fun i j =>
    (List.finRange mid).foldl (fun acc k => acc + a i k * b k j) 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grid size”. Number of grid points in an 'n'-qubit register.

def gridSize (n : Nat) : Nat := 2 ^ n

/--
Small ceiling-log helper for resource bookkeeping.

`clog2 m` is the number of bits needed to address `m` alternatives, with
`clog2 0 = clog2 1 = 0`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “clog 2”. Small ceiling-log helper for resource bookkeeping.

def clog2 (m : Nat) : Nat :=
  if m <= 1 then 0 else Nat.log2 (m - 1) + 1

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem gridSize_zero : gridSize 0 = 1 := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem clog2_zero : clog2 0 = 0 := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem clog2_one : clog2 1 = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “log 2 pred two pow succ”; the hypotheses and conclusion in the code panel fix its exact scope. 'log2 (2^(n+1)-1) = n', the arithmetic fact behind 'clog2_gridSize'.

theorem log2_pred_two_pow_succ (n : Nat) :
    Nat.log2 (2 ^ (n + 1) - 1) = n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clog 2 grid size”; the hypotheses and conclusion in the code panel fix its exact scope. The bit-width of an 'n'-qubit grid is 'n'.

@[simp] theorem clog2_gridSize (n : Nat) : clog2 (gridSize n) = n := by

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “boundary kind”; its constructors are the cases that downstream code must handle. Boundary conditions tracked by this library.

inductive BoundaryKind where
  | periodic
  | robin
  | dirichlet
  | neumann
deriving Repr, DecidableEq

/-- Finite-difference stencil metadata. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “stencil”. A proposition-valued field is a requirement until a constructor supplies it. Finite-difference stencil metadata.

structure Stencil where
  derivativeOrder : Nat
  accuracyOrder : Nat
  leftRadius : Nat
  rightRadius : Nat
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “width”. The number of columns touched by a stencil row before boundary corrections.

def width (s : Stencil) : Nat :=
  s.leftRadius + s.rightRadius + 1

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem width_eq (s : Stencil) :
    s.width = s.leftRadius + s.rightRadius + 1 := rfl

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “bulk window”. A proposition-valued field is a requirement until a constructor supplies it. A central bulk interval '[lower, upper]' inside the computational basis rows.

structure BulkWindow where
  lower : Nat
  upper : Nat
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “paper boundary lines”. Number of boundary-side rows outside the bulk, using the paper's convention.

def paperBoundaryLines (w : BulkWindow) (n : Nat) : Nat :=
  w.lower + gridSize n - w.upper

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “coeff”; its constructors are the cases that downstream code must handle. A lightweight symbolic coefficient language for stencil entries.

inductive Coeff where
  | rat (q : Rat)
  | symbol (name : String)
  | add (a b : Coeff)
  | mul (a b : Coeff)
  | neg (a : Coeff)
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def sub (a b : Coeff) : Coeff := a + (-b)

instance : HSub Coeff Coeff Coeff where
  hSub := sub

/-- Evaluate a symbolic `Coeff` to a concrete `Rat` given an environment. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “eval with”. Evaluate a symbolic 'Coeff' to a concrete 'Rat' given an environment.

def evalWith (env : String → Rat) : Coeff → Rat
  | rat q => q
  | symbol name => env name
  | add a b => evalWith env a + evalWith env b
  | mul a b => evalWith env a * evalWith env b
  | neg a => -(evalWith env a)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalWith_rat (env : String → Rat) (q : Rat) :
    evalWith env (rat q) = q := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalWith_symbol (env : String → Rat) (name : String) :
    evalWith env (symbol name) = env name := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalWith_add (env : String → Rat) (a b : Coeff) :
    evalWith env (add a b) = evalWith env a + evalWith env b := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalWith_mul (env : String → Rat) (a b : Coeff) :
    evalWith env (mul a b) = evalWith env a * evalWith env b := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalWith_neg (env : String → Rat) (a : Coeff) :
    evalWith env (neg a) = -(evalWith env a) := rfl

/-- Trivial reflexivity lemma for the zero rational coefficient. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat zero”; the hypotheses and conclusion in the code panel fix its exact scope. Trivial reflexivity lemma for the zero rational coefficient.

theorem rat_zero : Coeff.rat 0 = Coeff.rat 0 := rfl

/-- Evaluating `Coeff.rat 0` yields `0` under any environment. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with rat zero”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.rat 0' yields '0' under any environment.

@[simp] theorem evalWith_rat_zero (env : String → Rat) :
    evalWith env (Coeff.rat 0) = (0 : Rat) := rfl

/-- Evaluating `Coeff.rat 1` yields `1` under any environment. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with rat one”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.rat 1' yields '1' under any environment.

@[simp] theorem evalWith_rat_one (env : String → Rat) :
    evalWith env (Coeff.rat 1) = (1 : Rat) := rfl

/-- Evaluating `Coeff.add (Coeff.rat a) (Coeff.rat b)` yields `a + b`. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with rat add”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.add (Coeff.rat a) (Coeff.rat b)' yields 'a + b'.

theorem evalWith_rat_add (env : String → Rat) (a b : Rat) :
    evalWith env (Coeff.add (Coeff.rat a) (Coeff.rat b)) = a + b := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with rat mul”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.mul (Coeff.rat a) (Coeff.rat b)' yields 'a * b'.

theorem evalWith_rat_mul (env : String → Rat) (a b : Rat) :
    evalWith env (Coeff.mul (Coeff.rat a) (Coeff.rat b)) = a * b := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with rat neg”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.neg (Coeff.rat a)' yields '-a'.

theorem evalWith_rat_neg (env : String → Rat) (a : Rat) :
    evalWith env (Coeff.neg (Coeff.rat a)) = -a := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with eq zero of rat zero”; the hypotheses and conclusion in the code panel fix its exact scope. If a Coeff value is 'Coeff.rat 0', it evaluates to '0' under any environment.

theorem evalWith_eq_zero_of_rat_zero (env : String → Rat) :
    evalWith env (Coeff.rat 0) = (0 : Rat) := rfl

/-- If a Coeff value is `Coeff.rat 1`, it evaluates to `1` under any environment. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval with eq one of rat one”; the hypotheses and conclusion in the code panel fix its exact scope. If a Coeff value is 'Coeff.rat 1', it evaluates to '1' under any environment.

theorem evalWith_eq_one_of_rat_one (env : String → Rat) :
    evalWith env (Coeff.rat 1) = (1 : Rat) := rfl

commit-pinned source · Verso Blueprint panel

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

def divNat (a : Coeff) (n : Nat) : Coeff :=
  a * Coeff.rat ((1 : Rat) / n)

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “stencil entry”. A proposition-valued field is a requirement until a constructor supplies it. One symbolic nonzero entry in a finite-difference row.

structure StencilEntry where
  offset : Int
  coeff : Coeff
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel