QuantumBlockEncoding/OpenProblems.lean

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

inductive ProblemStatus where
  | open
  | inProgress
  | formalized
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

structure OpenProblem where
  id : String
  title : String
  status : ProblemStatus
  statement : String
  acceptanceTest : String
  references : List String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def openProblems : List OpenProblem :=
  [
    {
      id := "QBE-001",
      title := "Gate-level Robin derivative block encoding for arbitrary stencil",
      status := ProblemStatus.open,
      statement := "Given a finite-difference stencil and Robin boundary data, synthesize the bulk-plus-boundary circuit for D and prove its block-encoding normalization.",
      acceptanceTest := "A Lean VerifiedBlockEncoding whose concrete matrix semantics equal the requested derivative matrix and whose resource bound is O(kappa*n) plus coefficient-oracle cost.",
      references := ["Guseynov-Huang-Liu 2025, one-term Robin theorem"]
    },
    {

commit-pinned source · Verso Blueprint panel

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

def problemCount : Nat := openProblems.length

commit-pinned source · Verso Blueprint panel