QuantumBlockEncoding/Literature.lean

This type lists the allowed alternatives for “implementation status”; its constructors are the cases that downstream code must handle.

inductive ImplementationStatus where
  | planned
  | skeleton
  | formalized
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “paper role”; its constructors are the cases that downstream code must handle.

inductive PaperRole where
  | primaryTarget
  | explicitBlockEncoding
  | oracleConstruction
  | statePreparation
  | qsvtFramework
  | pdeSimulation
  | arithmeticCircuits
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

structure PaperEntry where
  key : String
  title : String
  authors : String
  year : Nat
  role : PaperRole
  status : ImplementationStatus
  targetFile : String
  url : String
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def literature : List PaperEntry :=
  [
    {
      key := "guseynov-huang-liu-2026-robin",
      title := "Quantum framework for simulating linear PDEs with Robin boundary conditions",
      authors := "Nikita Guseynov, Xiajie Huang, Nana Liu",
      year := 2026,
      role := PaperRole.primaryTarget,
      status := ImplementationStatus.formalized,
      targetFile := "QuantumBlockEncoding/GHLHamiltonian.lean",
      url := "https://arxiv.org/abs/2506.20478",

commit-pinned source · Verso Blueprint panel

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

def literatureCount : Nat := literature.length

commit-pinned source · Verso Blueprint panel

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

def primaryPapers : List PaperEntry :=
  literature.filter (fun p => p.role == PaperRole.primaryTarget)

commit-pinned source · Verso Blueprint panel