ASPBE Lean Blueprint

11.1. QuantumBlockEncoding/Automation.lean🔗

39 explicit public declarations, in source order.

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

Plain-English reading. This type lists the allowed alternatives for “automation stage”; 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/Automation.lean:12. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.1●1 definition
  • inductive(7 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.AutomationStage : Type
    inductive QuantumBlockEncoding.AutomationStage :
  Type

    Constructors

    literatureTriage : QuantumBlockEncoding.AutomationStage
    formalSpec : QuantumBlockEncoding.AutomationStage
    circuitSearch : QuantumBlockEncoding.AutomationStage
    candidateScoring : QuantumBlockEncoding.AutomationStage
    leanProof : QuantumBlockEncoding.AutomationStage
    review : QuantumBlockEncoding.AutomationStage
    documented : QuantumBlockEncoding.AutomationStage
Definition11.1.2
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “task kind”; 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/Automation.lean:22. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.2●1 definition
  • inductive(8 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.TaskKind : Type
    inductive QuantumBlockEncoding.TaskKind : Type

    Constructors

    operatorBlockEncoding : QuantumBlockEncoding.TaskKind
    paperBenchmark : QuantumBlockEncoding.TaskKind
    paperFormalization : QuantumBlockEncoding.TaskKind
    oracleRealization : QuantumBlockEncoding.TaskKind
    blockEncodingSearch : QuantumBlockEncoding.TaskKind
    openProblemProposal : QuantumBlockEncoding.TaskKind
    conversionWindow : QuantumBlockEncoding.TaskKind
    proofRepair : QuantumBlockEncoding.TaskKind
Definition11.1.3
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “task 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/Automation.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.3●1 definition
  • inductive(5 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.TaskStatus : Type
    inductive QuantumBlockEncoding.TaskStatus : Type

    Constructors

    planned : QuantumBlockEncoding.TaskStatus
    active : QuantumBlockEncoding.TaskStatus
    blocked : QuantumBlockEncoding.TaskStatus
    leanCompiles : QuantumBlockEncoding.TaskStatus
    merged : QuantumBlockEncoding.TaskStatus
Definition11.1.4
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “artifact language”; 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/Automation.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.4●1 definition
  • inductive(5 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.ArtifactLanguage : Type
    inductive QuantumBlockEncoding.ArtifactLanguage :
  Type

    Constructors

    lean : QuantumBlockEncoding.ArtifactLanguage
    latex : QuantumBlockEncoding.ArtifactLanguage
    markdown : QuantumBlockEncoding.ArtifactLanguage
    json : QuantumBlockEncoding.ArtifactLanguage
    csv : QuantumBlockEncoding.ArtifactLanguage
Definition11.1.5
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “agent 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/Automation.lean:49. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.5●1 definition
  • inductive(4 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.AgentRole : Type
    inductive QuantumBlockEncoding.AgentRole : Type

    Constructors

    upper : QuantumBlockEncoding.AgentRole
    middle : QuantumBlockEncoding.AgentRole
    lower : QuantumBlockEncoding.AgentRole
    reviewer : QuantumBlockEncoding.AgentRole
Definition11.1.6
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “agent backend kind”; 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/Automation.lean:56. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.6●1 definition
  • inductive(8 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.AgentBackendKind : Type
    inductive QuantumBlockEncoding.AgentBackendKind :
  Type

    Constructors

    codex : QuantumBlockEncoding.AgentBackendKind
    claude : QuantumBlockEncoding.AgentBackendKind
    gpt : QuantumBlockEncoding.AgentBackendKind
    gemini : QuantumBlockEncoding.AgentBackendKind
    glm : QuantumBlockEncoding.AgentBackendKind
    minimax : QuantumBlockEncoding.AgentBackendKind
    localWrapper : QuantumBlockEncoding.AgentBackendKind
    custom : QuantumBlockEncoding.AgentBackendKind
Definition11.1.7
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “trial kind”; 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/Automation.lean:67. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.7●1 definition
  • inductive(7 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.TrialKind : Type
    inductive QuantumBlockEncoding.TrialKind : Type

    Constructors

    plan : QuantumBlockEncoding.TrialKind
    attempt : QuantumBlockEncoding.TrialKind
    build : QuantumBlockEncoding.TrialKind
    review : QuantumBlockEncoding.TrialKind
    proposal : QuantumBlockEncoding.TrialKind
    compression : QuantumBlockEncoding.TrialKind
    handoff : QuantumBlockEncoding.TrialKind
Definition11.1.8
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “trial 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/Automation.lean:77. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.8●1 definition
  • inductive(7 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.TrialStatus : Type
    inductive QuantumBlockEncoding.TrialStatus : Type

    Constructors

    queued : QuantumBlockEncoding.TrialStatus
    running : QuantumBlockEncoding.TrialStatus
    blocked : QuantumBlockEncoding.TrialStatus
    failed : QuantumBlockEncoding.TrialStatus
    compiled : QuantumBlockEncoding.TrialStatus
    accepted : QuantumBlockEncoding.TrialStatus
    rejected : QuantumBlockEncoding.TrialStatus
Definition11.1.9
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “artifact spec”. 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/Automation.lean:87. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.9●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.ArtifactSpec : Type
    structure QuantumBlockEncoding.ArtifactSpec : Type

    Fields

    path : String
    language : QuantumBlockEncoding.ArtifactLanguage
    purpose : String
    mustCompile : Bool
Definition11.1.10
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “acceptance gate”. 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/Automation.lean:94. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.10●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.AcceptanceGate : Type
    structure QuantumBlockEncoding.AcceptanceGate : Type

    Fields

    name : String
    command : String
    required : Bool
    note : String
Definition11.1.11
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “automation task”. 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/Automation.lean:101. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.11●1 definition
  • structure(9 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.AutomationTask : Type
    structure QuantumBlockEncoding.AutomationTask : Type

    Fields

    id : String
    title : String
    kind : QuantumBlockEncoding.TaskKind
    status : QuantumBlockEncoding.TaskStatus
    stage : QuantumBlockEncoding.AutomationStage
    source : String
    targetLean : String
    artifacts : List QuantumBlockEncoding.ArtifactSpec
    gates : List QuantumBlockEncoding.AcceptanceGate
Definition11.1.12
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “agent contract”. 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/Automation.lean:113. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.12●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.AgentContract : Type
    structure QuantumBlockEncoding.AgentContract : Type

    Fields

    role : QuantumBlockEncoding.AgentRole
    responsibility : String
    writes : List String
    mustLogTrial : Bool
Definition11.1.13
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “trial record spec”. 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/Automation.lean:120. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.13●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.TrialRecordSpec : Type
    structure QuantumBlockEncoding.TrialRecordSpec :
  Type

    Fields

    logPath : String
    summaryPath : String
    requiredFields : List String
    note : String
Definition11.1.14
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “post cycle artifact kind”; 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/Automation.lean:127. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.14●1 definition
  • inductive(5 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.PostCycleArtifactKind : Type
    inductive QuantumBlockEncoding.PostCycleArtifactKind :
  Type

    Constructors

    preferredLanguageSummary :
  QuantumBlockEncoding.PostCycleArtifactKind
    chatgptProPrompt :
  QuantumBlockEncoding.PostCycleArtifactKind
    retrievalIndex : QuantumBlockEncoding.PostCycleArtifactKind
    technicalReportUpdate :
  QuantumBlockEncoding.PostCycleArtifactKind
    verifierFeedback :
  QuantumBlockEncoding.PostCycleArtifactKind
Definition11.1.15
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “post cycle artifact spec”. 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/Automation.lean:135. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.15●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.PostCycleArtifactSpec : Type
    structure QuantumBlockEncoding.PostCycleArtifactSpec :
  Type

    Fields

    kind : QuantumBlockEncoding.PostCycleArtifactKind
    pathPattern : String
    selfContainedForExternalModel : Bool
    note : String
Definition11.1.16
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “workflow check spec”. 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/Automation.lean:142. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.16●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.WorkflowCheckSpec : Type
    structure QuantumBlockEncoding.WorkflowCheckSpec :
  Type

    Fields

    name : String
    checks : List String
    inspiredBy : String
    note : String
Definition11.1.17
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “candidate pool”; 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/Automation.lean:149. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.17●1 definition
  • inductive(2 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.CandidatePool : Type
    inductive QuantumBlockEncoding.CandidatePool : Type

    Constructors

    insight : QuantumBlockEncoding.CandidatePool
    certified : QuantumBlockEncoding.CandidatePool
Definition11.1.18
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “lex elim scheduler mode”; 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/Automation.lean:154. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.18●1 definition
  • inductive(2 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.LexElimSchedulerMode : Type
    inductive QuantumBlockEncoding.LexElimSchedulerMode :
  Type

    Constructors

    lexElimOut : QuantumBlockEncoding.LexElimSchedulerMode
    lexElimIn : QuantumBlockEncoding.LexElimSchedulerMode
Definition11.1.19
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “lex objective class”; 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/Automation.lean:159. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.19●1 definition
  • inductive(6 constructors)defined in QuantumBlockEncoding/Automation.lean
    complete
    inductive QuantumBlockEncoding.LexObjectiveClass : Type
    inductive QuantumBlockEncoding.LexObjectiveClass :
  Type

    Constructors

    hardCorrectness : QuantumBlockEncoding.LexObjectiveClass
    necessaryDiagnostic : QuantumBlockEncoding.LexObjectiveClass
    asymptoticTier : QuantumBlockEncoding.LexObjectiveClass
    concreteResource : QuantumBlockEncoding.LexObjectiveClass
    proofProgress : QuantumBlockEncoding.LexObjectiveClass
    processCost : QuantumBlockEncoding.LexObjectiveClass
Definition11.1.20
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “lex objective spec”. 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/Automation.lean:168. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.20●1 definition
  • structure(5 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.LexObjectiveSpec : Type
    structure QuantumBlockEncoding.LexObjectiveSpec :
  Type

    Fields

    name : String
    priority : ℕ
    objectiveClass : QuantumBlockEncoding.LexObjectiveClass
    hardGate : Bool
    note : String
Definition11.1.21
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “lex elim scheduler spec”. 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/Automation.lean:176. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.21●1 definition
  • structure(6 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.LexElimSchedulerSpec : Type
    structure QuantumBlockEncoding.LexElimSchedulerSpec :
  Type

    Fields

    mode : QuantumBlockEncoding.LexElimSchedulerMode
    useCase : String
    activeSet : String
    eliminationRule : String
    promotionRule : String
    inspiredBy : String
Definition11.1.22
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “agent panel size spec”. 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/Automation.lean:185. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.22●1 definition
  • structure(7 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.AgentPanelSizeSpec : Type
    structure QuantumBlockEncoding.AgentPanelSizeSpec :
  Type

    Fields

    taskClass : String
    upperCount : ℕ
    middleCount : ℕ
    lowerCount : ℕ
    reviewerCount : ℕ
    useWhen : String
    avoidWhen : String
Definition11.1.23
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “agent backend profile spec”. 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/Automation.lean:195. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.23●1 definition
  • structure(5 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.AgentBackendProfileSpec : Type
    structure QuantumBlockEncoding.AgentBackendProfileSpec :
  Type

    Fields

    role : QuantumBlockEncoding.AgentRole
    slot : String
    allowedBackends : List QuantumBlockEncoding.AgentBackendKind
    commandProfileKey : String
    note : String
Definition11.1.24
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “workflow invariant spec”. 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/Automation.lean:203. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.24●1 definition
  • structure(5 fields)defined in QuantumBlockEncoding/Automation.lean
    complete
    structure QuantumBlockEncoding.WorkflowInvariantSpec : Type
    structure QuantumBlockEncoding.WorkflowInvariantSpec :
  Type

    Fields

    name : String
    precondition : String
    requiredEvidence : List String
    rejectionReason : String
    inspiredBy : String
Definition11.1.25
uses 0used by 0✓L∃∀N

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

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/Automation.lean:211. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.25●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.leanBuildGate : QuantumBlockEncoding.AcceptanceGate
    def QuantumBlockEncoding.leanBuildGate :
  QuantumBlockEncoding.AcceptanceGate
Definition11.1.26
uses 0used by 0✓L∃∀N

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

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/Automation.lean:217. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.26●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.noSorryGate : QuantumBlockEncoding.AcceptanceGate
    def QuantumBlockEncoding.noSorryGate :
  QuantumBlockEncoding.AcceptanceGate
Definition11.1.27
uses 0used by 0✓L∃∀N

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

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/Automation.lean:223. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.27●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.defaultGates :
  List QuantumBlockEncoding.AcceptanceGate
    def QuantumBlockEncoding.defaultGates :
  List QuantumBlockEncoding.AcceptanceGate
Definition11.1.28
uses 0used by 0✓L∃∀N

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

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/Automation.lean:226. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.28●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.trialRecordSpec :
  QuantumBlockEncoding.TrialRecordSpec
    def QuantumBlockEncoding.trialRecordSpec :
  QuantumBlockEncoding.TrialRecordSpec
Definition11.1.29
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “post cycle artifact specs”.

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/Automation.lean:243. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.29●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.postCycleArtifactSpecs :
  List QuantumBlockEncoding.PostCycleArtifactSpec
    def QuantumBlockEncoding.postCycleArtifactSpecs :
  List
    QuantumBlockEncoding.PostCycleArtifactSpec
Definition11.1.30
uses 0used by 0✓L∃∀N

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

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/Automation.lean:271. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.30●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.workflowCheckSpecs :
  List QuantumBlockEncoding.WorkflowCheckSpec
    def QuantumBlockEncoding.workflowCheckSpecs :
  List
    QuantumBlockEncoding.WorkflowCheckSpec
Definition11.1.31
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “block encoding lex objective specs”.

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/Automation.lean:287. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.31●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.blockEncodingLexObjectiveSpecs :
  List QuantumBlockEncoding.LexObjectiveSpec
    def QuantumBlockEncoding.blockEncodingLexObjectiveSpecs :
  List
    QuantumBlockEncoding.LexObjectiveSpec
Definition11.1.32
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lex elim scheduler specs”.

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/Automation.lean:333. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.32●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.lexElimSchedulerSpecs :
  List QuantumBlockEncoding.LexElimSchedulerSpec
    def QuantumBlockEncoding.lexElimSchedulerSpecs :
  List
    QuantumBlockEncoding.LexElimSchedulerSpec
Definition11.1.33
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “agent panel size specs”.

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/Automation.lean:353. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.33●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.agentPanelSizeSpecs :
  List QuantumBlockEncoding.AgentPanelSizeSpec
    def QuantumBlockEncoding.agentPanelSizeSpecs :
  List
    QuantumBlockEncoding.AgentPanelSizeSpec
Definition11.1.34
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “agent backend profile specs”.

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/Automation.lean:393. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.34●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.agentBackendProfileSpecs :
  List QuantumBlockEncoding.AgentBackendProfileSpec
    def QuantumBlockEncoding.agentBackendProfileSpecs :
  List
    QuantumBlockEncoding.AgentBackendProfileSpec
Definition11.1.35
uses 0used by 0✓L∃∀N

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

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/Automation.lean:493. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.35●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.workflowInvariantSpecs :
  List QuantumBlockEncoding.WorkflowInvariantSpec
    def QuantumBlockEncoding.workflowInvariantSpecs :
  List
    QuantumBlockEncoding.WorkflowInvariantSpec
Definition11.1.36
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “three layer agent contracts”.

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/Automation.lean:518. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.36●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.threeLayerAgentContracts :
  List QuantumBlockEncoding.AgentContract
    def QuantumBlockEncoding.threeLayerAgentContracts :
  List QuantumBlockEncoding.AgentContract
Definition11.1.37
uses 0used by 0✓L∃∀N

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

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/Automation.lean:546. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.37●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.conversionArtifacts (stem : String) :
  List QuantumBlockEncoding.ArtifactSpec
    def QuantumBlockEncoding.conversionArtifacts
  (stem : String) :
  List QuantumBlockEncoding.ArtifactSpec
Definition11.1.38
uses 0used by 0✓L∃∀N

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

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/Automation.lean:568. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.38●1 definition
  • defdefined in QuantumBlockEncoding/Automation.lean
    complete
    def QuantumBlockEncoding.seedAutomationTasks :
  List QuantumBlockEncoding.AutomationTask
    def QuantumBlockEncoding.seedAutomationTasks :
  List QuantumBlockEncoding.AutomationTask
Definition11.1.39
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “automation task 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/Automation.lean:605. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition11.1.39●1 definition