11.5. QuantumBlockEncoding/OpenProblemsAudit.lean🔗

6 explicit public declarations, in source order.

Definition11.5.1

uses 0used by 0✓L∃∀N

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

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. Typed controller state, agent contracts, literature memory, and explicit open-problem records.

Technical source note. Stable list of the published problem identifiers.

Declaration kind. def.

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

Lean code for Definition11.5.1●1 definition

defdefined in QuantumBlockEncoding/OpenProblemsAudit.lean

complete

def QuantumBlockEncoding.openProblemIds : List String

def QuantumBlockEncoding.openProblemIds :
  List String

Stable list of the published problem identifiers.

Definition11.5.2

uses 0used by 0✓L∃∀N

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

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. Typed controller state, agent contracts, literature memory, and explicit open-problem records.

Technical source note. Every public registry entry carries enough data to be actionable.

Declaration kind. def.

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

Lean code for Definition11.5.2●1 definition

defdefined in QuantumBlockEncoding/OpenProblemsAudit.lean

complete

def QuantumBlockEncoding.OpenProblem.actionable
  (problem : QuantumBlockEncoding.OpenProblem) : Prop

def QuantumBlockEncoding.OpenProblem.actionable
  (problem :
    QuantumBlockEncoding.OpenProblem) :
  Prop

Every public registry entry carries enough data to be actionable.

Theorem11.5.3

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Typed controller state, agent contracts, literature memory, and explicit open-problem records.

Technical source note. The current registry contains seven explicitly scoped problems.

Declaration kind. theorem.

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

Lean code for Theorem11.5.3●1 theorem

theoremdefined in QuantumBlockEncoding/OpenProblemsAudit.lean

complete

theorem QuantumBlockEncoding.openProblems_count :
  QuantumBlockEncoding.problemCount = 7

theorem QuantumBlockEncoding.openProblems_count :
  QuantumBlockEncoding.problemCount = 7

The current registry contains seven explicitly scoped problems.

Theorem11.5.4

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Typed controller state, agent contracts, literature memory, and explicit open-problem records.

Technical source note. Problem identifiers are unique, so memories and task packets cannot collide.

Declaration kind. theorem.

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

Lean code for Theorem11.5.4●1 theorem

theoremdefined in QuantumBlockEncoding/OpenProblemsAudit.lean

complete

theorem QuantumBlockEncoding.openProblemIds_nodup :
  QuantumBlockEncoding.openProblemIds.Nodup

theorem QuantumBlockEncoding.openProblemIds_nodup :
  QuantumBlockEncoding.openProblemIds.Nodup

Problem identifiers are unique, so memories and task packets cannot collide.

Theorem11.5.5

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Typed controller state, agent contracts, literature memory, and explicit open-problem records.

Technical source note. Every current problem has a nonempty statement, acceptance test, and source list.

Declaration kind. theorem.

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

Lean code for Theorem11.5.5●1 theorem

theoremdefined in QuantumBlockEncoding/OpenProblemsAudit.lean

complete

theorem QuantumBlockEncoding.openProblems_all_actionable
  (problem : QuantumBlockEncoding.OpenProblem) :
  problem ∈ QuantumBlockEncoding.openProblems → problem.actionable

theorem QuantumBlockEncoding.openProblems_all_actionable
  (problem :
    QuantumBlockEncoding.OpenProblem) :
  problem ∈
      QuantumBlockEncoding.openProblems →
    problem.actionable

Every current problem has a nonempty statement, acceptance test, and source list.

Theorem11.5.6

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Typed controller state, agent contracts, literature memory, and explicit open-problem records.

Technical source note. The registry itself is a compiled artifact even though its entries remain open research.

Declaration kind. theorem.

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

Lean code for Theorem11.5.6●1 theorem

theoremdefined in QuantumBlockEncoding/OpenProblemsAudit.lean

complete

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

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

The registry itself is a compiled artifact even though its entries remain open research.