QuantumBlockEncoding/OpenProblemsAudit.lean

This definition gives the library's named construction or computation for “open problem ids”. Stable list of the published problem identifiers.

def openProblemIds : List String := openProblems.map OpenProblem.id

/-- Every public registry entry carries enough data to be actionable. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “actionable”. Every public registry entry carries enough data to be actionable.

def OpenProblem.actionable (problem : OpenProblem) : Prop :=
  problem.id ≠ "" ∧
  problem.title ≠ "" ∧
  problem.statement ≠ "" ∧
  problem.acceptanceTest ≠ "" ∧
  problem.references ≠ []

instance (problem : OpenProblem) : Decidable problem.actionable := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “open problems count”; the hypotheses and conclusion in the code panel fix its exact scope. The current registry contains seven explicitly scoped problems.

theorem openProblems_count : problemCount = 7 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “open problem ids nodup”; the hypotheses and conclusion in the code panel fix its exact scope. Problem identifiers are unique, so memories and task packets cannot collide.

theorem openProblemIds_nodup : openProblemIds.Nodup := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “open problems all actionable”; the hypotheses and conclusion in the code panel fix its exact scope. Every current problem has a nonempty statement, acceptance test, and source list.

theorem openProblems_all_actionable :
    ∀ problem ∈ openProblems, problem.actionable := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “open problem registry compiled”; the hypotheses and conclusion in the code panel fix its exact scope. The registry itself is a compiled artifact even though its entries remain open research.

theorem openProblemRegistry_compiled :
    problemCount = 7 ∧ openProblemIds.Nodup ∧
      (∀ problem ∈ openProblems, problem.actionable) := by

commit-pinned source · Verso Blueprint panel