5.3. QuantumBlockEncoding/Core.lean🔗

36 explicit public declarations, in source order.

Definition5.3.1

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A finite matrix represented by its entries.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/Core.lean:15. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.1●1 definition

abbrevdefined in QuantumBlockEncoding/Core.lean

complete

abbrev QuantumBlockEncoding.Matrix.{u} (rows cols : ℕ) (α : Type u) : Type u

abbrev QuantumBlockEncoding.Matrix.{u}
  (rows cols : ℕ) (α : Type u) : Type u

A finite matrix represented by its entries.

Definition5.3.2

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Pointwise equality for finite matrices.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:20. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.2●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Matrix.PointwiseEq.{u} {rows cols : ℕ} {α : Type u}
  (a b : QuantumBlockEncoding.Matrix rows cols α) : Prop

def QuantumBlockEncoding.Matrix.PointwiseEq.{u}
  {rows cols : ℕ} {α : Type u}
  (a b :
    QuantumBlockEncoding.Matrix rows cols
      α) :
  Prop

Pointwise equality for finite matrices.

Definition5.3.3

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The zero finite matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:25. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.3●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Matrix.zero.{u} (rows cols : ℕ) (α : Type u)
  [OfNat α 0] : QuantumBlockEncoding.Matrix rows cols α

def QuantumBlockEncoding.Matrix.zero.{u}
  (rows cols : ℕ) (α : Type u)
  [OfNat α 0] :
  QuantumBlockEncoding.Matrix rows cols α

The zero finite matrix.

Definition5.3.4

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The identity finite matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:29. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.4●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Matrix.identity.{u} (n : ℕ) (α : Type u)
  [OfNat α 0] [OfNat α 1] : QuantumBlockEncoding.Matrix n n α

def QuantumBlockEncoding.Matrix.identity.{u}
  (n : ℕ) (α : Type u) [OfNat α 0]
  [OfNat α 1] :
  QuantumBlockEncoding.Matrix n n α

The identity finite matrix.

Definition5.3.5

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Finite matrix multiplication with the project-local 'Matrix' representation.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:34. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.5●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Matrix.mul.{u} {rows mid cols : ℕ} {α : Type u}
  [OfNat α 0] [HAdd α α α] [HMul α α α]
  (a : QuantumBlockEncoding.Matrix rows mid α)
  (b : QuantumBlockEncoding.Matrix mid cols α) :
  QuantumBlockEncoding.Matrix rows cols α

def QuantumBlockEncoding.Matrix.mul.{u}
  {rows mid cols : ℕ} {α : Type u}
  [OfNat α 0] [HAdd α α α] [HMul α α α]
  (a :
    QuantumBlockEncoding.Matrix rows mid
      α)
  (b :
    QuantumBlockEncoding.Matrix mid cols
      α) :
  QuantumBlockEncoding.Matrix rows cols α

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

Definition5.3.6

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Number of grid points in an 'n'-qubit register.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.6●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.gridSize (n : ℕ) : ℕ

def QuantumBlockEncoding.gridSize (n : ℕ) : ℕ

Number of grid points in an `n`-qubit register.

Definition5.3.7

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. 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'.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.7●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.clog2 (m : ℕ) : ℕ

def QuantumBlockEncoding.clog2 (m : ℕ) : ℕ

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`.

Theorem5.3.8

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:55. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.8●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.gridSize_zero : QuantumBlockEncoding.gridSize 0 = 1

theorem QuantumBlockEncoding.gridSize_zero :
  QuantumBlockEncoding.gridSize 0 = 1

Theorem5.3.9

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:57. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.9●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.clog2_zero : QuantumBlockEncoding.clog2 0 = 0

theorem QuantumBlockEncoding.clog2_zero :
  QuantumBlockEncoding.clog2 0 = 0

Theorem5.3.10

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:60. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.10●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.clog2_one : QuantumBlockEncoding.clog2 1 = 0

theorem QuantumBlockEncoding.clog2_one :
  QuantumBlockEncoding.clog2 1 = 0

Theorem5.3.11

uses 0used by 0✓L∃∀N

Plain-English reading. 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'.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. 'log2 (2^(n+1)-1) = n', the arithmetic fact behind 'clog2_gridSize'.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:64. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.11●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.log2_pred_two_pow_succ (n : ℕ) :
  (2 ^ (n + 1) - 1).log2 = n

theorem QuantumBlockEncoding.log2_pred_two_pow_succ
  (n : ℕ) : (2 ^ (n + 1) - 1).log2 = n

`log2 (2^(n+1)-1) = n`, the arithmetic fact behind `clog2_gridSize`.

Theorem5.3.12

uses 0used by 0✓L∃∀N

Plain-English reading. 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'.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The bit-width of an 'n'-qubit grid is 'n'.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:94. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.12●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.clog2_gridSize (n : ℕ) :
  QuantumBlockEncoding.clog2 (QuantumBlockEncoding.gridSize n) = n

theorem QuantumBlockEncoding.clog2_gridSize
  (n : ℕ) :
  QuantumBlockEncoding.clog2
      (QuantumBlockEncoding.gridSize n) =
    n

The bit-width of an `n`-qubit grid is `n`.

Definition5.3.13

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Boundary conditions tracked by this library.

Declaration kind. inductive.

Source: QuantumBlockEncoding/Core.lean:103. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.13●1 definition

inductive(4 constructors)defined in QuantumBlockEncoding/Core.lean

complete

inductive QuantumBlockEncoding.BoundaryKind : Type

inductive QuantumBlockEncoding.BoundaryKind : Type

Boundary conditions tracked by this library.

Constructors

periodic : QuantumBlockEncoding.BoundaryKind

robin : QuantumBlockEncoding.BoundaryKind

dirichlet : QuantumBlockEncoding.BoundaryKind

neumann : QuantumBlockEncoding.BoundaryKind

Definition5.3.14

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Finite-difference stencil metadata.

Declaration kind. structure.

Source: QuantumBlockEncoding/Core.lean:111. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.14●1 definition

structure(4 fields)defined in QuantumBlockEncoding/Core.lean

complete

structure QuantumBlockEncoding.Stencil : Type

structure QuantumBlockEncoding.Stencil : Type

Finite-difference stencil metadata.

Fields

derivativeOrder : ℕ

accuracyOrder : ℕ

leftRadius : ℕ

rightRadius : ℕ

Definition5.3.15

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The number of columns touched by a stencil row before boundary corrections.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:121. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.15●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Stencil.width (s : QuantumBlockEncoding.Stencil) :
  ℕ

def QuantumBlockEncoding.Stencil.width
  (s : QuantumBlockEncoding.Stencil) : ℕ

The number of columns touched by a stencil row before boundary corrections.

Theorem5.3.16

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:124. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.16●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Stencil.width_eq
  (s : QuantumBlockEncoding.Stencil) :
  s.width = s.leftRadius + s.rightRadius + 1

theorem QuantumBlockEncoding.Stencil.width_eq
  (s : QuantumBlockEncoding.Stencil) :
  s.width =
    s.leftRadius + s.rightRadius + 1

Definition5.3.17

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A central bulk interval '[lower, upper]' inside the computational basis rows. The first project version stores the bounds as data; stronger proofs about range validity can be added when the matrix semantics are imported.

Declaration kind. structure.

Source: QuantumBlockEncoding/Core.lean:134. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.17●1 definition

structure(2 fields)defined in QuantumBlockEncoding/Core.lean

complete

structure QuantumBlockEncoding.BulkWindow : Type

structure QuantumBlockEncoding.BulkWindow : Type

A central bulk interval `[lower, upper]` inside the computational basis rows.
The first project version stores the bounds as data; stronger proofs about
range validity can be added when the matrix semantics are imported.

Fields

lower : ℕ

upper : ℕ

Definition5.3.18

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Number of boundary-side rows outside the bulk, using the paper's convention.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:142. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.18●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.BulkWindow.paperBoundaryLines
  (w : QuantumBlockEncoding.BulkWindow) (n : ℕ) : ℕ

def QuantumBlockEncoding.BulkWindow.paperBoundaryLines
  (w : QuantumBlockEncoding.BulkWindow)
  (n : ℕ) : ℕ

Number of boundary-side rows outside the bulk, using the paper's convention.

Definition5.3.19

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A lightweight symbolic coefficient language for stencil entries.

Declaration kind. inductive.

Source: QuantumBlockEncoding/Core.lean:148. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.19●1 definition

inductive(5 constructors)defined in QuantumBlockEncoding/Core.lean

complete

inductive QuantumBlockEncoding.Coeff : Type

inductive QuantumBlockEncoding.Coeff : Type

A lightweight symbolic coefficient language for stencil entries.

Constructors

rat (q : ℚ) : QuantumBlockEncoding.Coeff

symbol (name : String) : QuantumBlockEncoding.Coeff

add (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff

mul (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff

neg (a : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff

Definition5.3.20

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:170. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.20●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Coeff.sub (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff

def QuantumBlockEncoding.Coeff.sub
  (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff

Definition5.3.21

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Evaluate a symbolic 'Coeff' to a concrete 'Rat' given an environment.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:176. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.21●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Coeff.evalWith (env : String → ℚ) :
  QuantumBlockEncoding.Coeff → ℚ

def QuantumBlockEncoding.Coeff.evalWith
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff → ℚ

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

Theorem5.3.22

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:183. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.22●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_rat (env : String → ℚ) (q : ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat q) =
    q

theorem QuantumBlockEncoding.Coeff.evalWith_rat
  (env : String → ℚ) (q : ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat q) =
    q

Theorem5.3.23

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:186. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.23●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_symbol (env : String → ℚ)
  (name : String) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.symbol name) =
    env name

theorem QuantumBlockEncoding.Coeff.evalWith_symbol
  (env : String → ℚ) (name : String) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.symbol
        name) =
    env name

Theorem5.3.24

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:189. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.24●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_add (env : String → ℚ)
  (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env (a.add b) =
    QuantumBlockEncoding.Coeff.evalWith env a +
      QuantumBlockEncoding.Coeff.evalWith env b

theorem QuantumBlockEncoding.Coeff.evalWith_add
  (env : String → ℚ)
  (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env
      (a.add b) =
    QuantumBlockEncoding.Coeff.evalWith
        env a +
      QuantumBlockEncoding.Coeff.evalWith
        env b

Theorem5.3.25

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:192. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.25●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_mul (env : String → ℚ)
  (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env (a.mul b) =
    QuantumBlockEncoding.Coeff.evalWith env a *
      QuantumBlockEncoding.Coeff.evalWith env b

theorem QuantumBlockEncoding.Coeff.evalWith_mul
  (env : String → ℚ)
  (a b : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env
      (a.mul b) =
    QuantumBlockEncoding.Coeff.evalWith
        env a *
      QuantumBlockEncoding.Coeff.evalWith
        env b

Theorem5.3.26

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:195. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.26●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_neg (env : String → ℚ)
  (a : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env a.neg =
    -QuantumBlockEncoding.Coeff.evalWith env a

theorem QuantumBlockEncoding.Coeff.evalWith_neg
  (env : String → ℚ)
  (a : QuantumBlockEncoding.Coeff) :
  QuantumBlockEncoding.Coeff.evalWith env
      a.neg =
    -QuantumBlockEncoding.Coeff.evalWith
        env a

Theorem5.3.27

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Trivial reflexivity lemma for the zero rational coefficient.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:199. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.27●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

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

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

Trivial reflexivity lemma for the zero rational coefficient.

Theorem5.3.28

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Evaluating 'Coeff.rat 0' yields '0' under any environment.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:202. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.28●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_rat_zero (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 0) =
    0

theorem QuantumBlockEncoding.Coeff.evalWith_rat_zero
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 0) =
    0

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

Theorem5.3.29

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Evaluating 'Coeff.rat 1' yields '1' under any environment.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:206. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.29●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_rat_one (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 1) =
    1

theorem QuantumBlockEncoding.Coeff.evalWith_rat_one
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 1) =
    1

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

Theorem5.3.30

uses 0used by 0✓L∃∀N

Plain-English reading. 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'.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Evaluating 'Coeff.add (Coeff.rat a) (Coeff.rat b)' yields 'a + b'.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:210. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.30●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

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

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

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

Theorem5.3.31

uses 0used by 0✓L∃∀N

Plain-English reading. 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'.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Evaluating 'Coeff.mul (Coeff.rat a) (Coeff.rat b)' yields 'a * b'.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:215. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.31●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

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

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

Evaluating `Coeff.mul (Coeff.rat a) (Coeff.rat b)` yields `a * b`.

Theorem5.3.32

uses 0used by 0✓L∃∀N

Plain-English reading. 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'.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Evaluating 'Coeff.neg (Coeff.rat a)' yields '-a'.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:220. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.32●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

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

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

Evaluating `Coeff.neg (Coeff.rat a)` yields `-a`.

Theorem5.3.33

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. If a Coeff value is 'Coeff.rat 0', it evaluates to '0' under any environment.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:225. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.33●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_eq_zero_of_rat_zero
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 0) =
    0

theorem QuantumBlockEncoding.Coeff.evalWith_eq_zero_of_rat_zero
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 0) =
    0

If a Coeff value is `Coeff.rat 0`, it evaluates to `0` under any environment.

Theorem5.3.34

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. If a Coeff value is 'Coeff.rat 1', it evaluates to '1' under any environment.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Core.lean:229. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.3.34●1 theorem

theoremdefined in QuantumBlockEncoding/Core.lean

complete

theorem QuantumBlockEncoding.Coeff.evalWith_eq_one_of_rat_one
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 1) =
    1

theorem QuantumBlockEncoding.Coeff.evalWith_eq_one_of_rat_one
  (env : String → ℚ) :
  QuantumBlockEncoding.Coeff.evalWith env
      (QuantumBlockEncoding.Coeff.rat 1) =
    1

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

Definition5.3.35

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/Core.lean:232. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.35●1 definition

defdefined in QuantumBlockEncoding/Core.lean

complete

def QuantumBlockEncoding.Coeff.divNat (a : QuantumBlockEncoding.Coeff)
  (n : ℕ) : QuantumBlockEncoding.Coeff

def QuantumBlockEncoding.Coeff.divNat
  (a : QuantumBlockEncoding.Coeff)
  (n : ℕ) : QuantumBlockEncoding.Coeff

Definition5.3.36

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. One symbolic nonzero entry in a finite-difference row.

Declaration kind. structure.

Source: QuantumBlockEncoding/Core.lean:238. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition5.3.36●1 definition

structure(2 fields)defined in QuantumBlockEncoding/Core.lean

complete

structure QuantumBlockEncoding.StencilEntry : Type

structure QuantumBlockEncoding.StencilEntry : Type

One symbolic nonzero entry in a finite-difference row.

Fields

offset : ℤ

coeff : QuantumBlockEncoding.Coeff