QuantumBlockEncoding/Examples/RobinHeat.lean

This definition gives the library's named construction or computation for “fourth order second derivative”.

def fourthOrderSecondDerivative : Stencil where
  derivativeOrder := 2
  accuracyOrder := 4
  leftRadius := 2
  rightRadius := 2

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “central bulk entries”.

def centralBulkEntries : List StencilEntry :=
  [
    { offset := -2, coeff := Coeff.rat ((-1 : Rat) / 12) },
    { offset := -1, coeff := Coeff.rat ((4 : Rat) / 3) },
    { offset := 0, coeff := Coeff.rat ((-5 : Rat) / 2) },
    { offset := 1, coeff := Coeff.rat ((4 : Rat) / 3) },
    { offset := 2, coeff := Coeff.rat ((-1 : Rat) / 12) }
  ]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “a 1 dx”.

def A1dx : Coeff := Coeff.symbol "A1*dx"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “b 1 dx”.

def B1dx : Coeff := Coeff.symbol "B1*dx"

/-- First row after eliminating the left Robin ghost points. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left boundary row 0”. First row after eliminating the left Robin ghost points.

def leftBoundaryRow0 : List StencilEntry :=
  [
    { offset := 0, coeff := Coeff.rat ((-5 : Rat) / 2) + (Coeff.rat ((7 : Rat) / 3) * A1dx) },
    { offset := 1, coeff := Coeff.rat ((8 : Rat) / 3) },
    { offset := 2, coeff := Coeff.rat ((-1 : Rat) / 6) }
  ]

/-- Second row after eliminating the left Robin ghost points. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left boundary row 1”. Second row after eliminating the left Robin ghost points.

def leftBoundaryRow1 : List StencilEntry :=
  [
    { offset := -1, coeff := Coeff.rat ((4 : Rat) / 3) - (Coeff.rat ((1 : Rat) / 6) * A1dx) },
    { offset := 0, coeff := Coeff.rat ((-31 : Rat) / 12) },
    { offset := 1, coeff := Coeff.rat ((4 : Rat) / 3) },
    { offset := 2, coeff := Coeff.rat ((-1 : Rat) / 12) }
  ]

/-- Penultimate row after eliminating the right Robin ghost points. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “right boundary row nm 2”. Penultimate row after eliminating the right Robin ghost points.

def rightBoundaryRowNm2 : List StencilEntry :=
  [
    { offset := -2, coeff := Coeff.rat ((-1 : Rat) / 12) },
    { offset := -1, coeff := Coeff.rat ((4 : Rat) / 3) },
    { offset := 0, coeff := Coeff.rat ((-31 : Rat) / 12) },
    { offset := 1, coeff := Coeff.rat ((4 : Rat) / 3) + (Coeff.rat ((1 : Rat) / 6) * B1dx) }
  ]

/-- Last row after eliminating the right Robin ghost points. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “right boundary row nm 1”. Last row after eliminating the right Robin ghost points.

def rightBoundaryRowNm1 : List StencilEntry :=
  [
    { offset := -2, coeff := Coeff.rat ((-1 : Rat) / 6) },
    { offset := -1, coeff := Coeff.rat ((8 : Rat) / 3) },
    { offset := 0, coeff := Coeff.rat ((-5 : Rat) / 2) - (Coeff.rat ((7 : Rat) / 3) * B1dx) }
  ]

commit-pinned source · Verso Blueprint panel

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

def robinWindow (n : Nat) : BulkWindow where
  lower := 2
  upper := gridSize n - 3

commit-pinned source · Verso Blueprint panel

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

def oneTermParameters (n : Nat) : GHL2025.OneTermRobinParameters where
  n := n
  kappa := 7
  functionPieces := 1
  polynomialDegreeCost := 1

commit-pinned source · Verso Blueprint panel

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

theorem fourthOrderStencilWidth :
    fourthOrderSecondDerivative.width = 5 := rfl

commit-pinned source · Verso Blueprint panel

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

theorem robinHeatAncillas (n : Nat) :
    (GHL2025.oneTermRobinResource (oneTermParameters n)).pureAncilla = 2 * n := rfl

commit-pinned source · Verso Blueprint panel