ASPBE Lean Blueprint

11.3. QuantumBlockEncoding/Literature.lean🔗

6 explicit public declarations, in source order.

Definition11.3.1
uses 0used by 0✓L∃∀N

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

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. inductive.

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

Lean code for Definition11.3.1●1 definition
  • inductive(3 constructors)defined in QuantumBlockEncoding/Literature.lean
    complete
    inductive QuantumBlockEncoding.ImplementationStatus : Type
    inductive QuantumBlockEncoding.ImplementationStatus :
  Type

    Constructors

    planned : QuantumBlockEncoding.ImplementationStatus
    skeleton : QuantumBlockEncoding.ImplementationStatus
    formalized : QuantumBlockEncoding.ImplementationStatus
Definition11.3.2
uses 0used by 0✓L∃∀N

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

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. inductive.

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

Lean code for Definition11.3.2●1 definition
  • inductive(7 constructors)defined in QuantumBlockEncoding/Literature.lean
    complete
    inductive QuantumBlockEncoding.PaperRole : Type
    inductive QuantumBlockEncoding.PaperRole : Type

    Constructors

    primaryTarget : QuantumBlockEncoding.PaperRole
    explicitBlockEncoding : QuantumBlockEncoding.PaperRole
    oracleConstruction : QuantumBlockEncoding.PaperRole
    statePreparation : QuantumBlockEncoding.PaperRole
    qsvtFramework : QuantumBlockEncoding.PaperRole
    pdeSimulation : QuantumBlockEncoding.PaperRole
    arithmeticCircuits : QuantumBlockEncoding.PaperRole
Definition11.3.3
uses 0used by 0✓L∃∀N

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

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. structure.

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

Lean code for Definition11.3.3●1 definition
  • structure(9 fields)defined in QuantumBlockEncoding/Literature.lean
    complete
    structure QuantumBlockEncoding.PaperEntry : Type
    structure QuantumBlockEncoding.PaperEntry : Type

    Fields

    key : String
    title : String
    authors : String
    year : ℕ
    role : QuantumBlockEncoding.PaperRole
    status : QuantumBlockEncoding.ImplementationStatus
    targetFile : String
    url : String
    note : String
Definition11.3.4
uses 0used by 0✓L∃∀N

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

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition11.3.4●1 definition
  • defdefined in QuantumBlockEncoding/Literature.lean
    complete
    def QuantumBlockEncoding.literature : List QuantumBlockEncoding.PaperEntry
    def QuantumBlockEncoding.literature :
  List QuantumBlockEncoding.PaperEntry
Definition11.3.5
uses 0used by 0✓L∃∀N

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

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition11.3.5●1 definition
Definition11.3.6
uses 0used by 0✓L∃∀N

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

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition11.3.6●1 definition
  • defdefined in QuantumBlockEncoding/Literature.lean
    complete
    def QuantumBlockEncoding.primaryPapers :
  List QuantumBlockEncoding.PaperEntry
    def QuantumBlockEncoding.primaryPapers :
  List QuantumBlockEncoding.PaperEntry