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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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, open-problem records, and source-to-Lean semantic-fidelity audits.

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

defdefined in QuantumBlockEncoding/Automation.lean

complete

def QuantumBlockEncoding.automationTaskCount : ℕ

def QuantumBlockEncoding.automationTaskCount :
  ℕ