QuantumBlockEncoding/Automation.lean

This type lists the allowed alternatives for “automation stage”; its constructors are the cases that downstream code must handle.

inductive AutomationStage where
  | literatureTriage
  | formalSpec
  | circuitSearch
  | candidateScoring
  | leanProof
  | review
  | documented
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “task kind”; its constructors are the cases that downstream code must handle.

inductive TaskKind where
  | operatorBlockEncoding
  | paperBenchmark
  | paperFormalization
  | oracleRealization
  | blockEncodingSearch
  | openProblemProposal
  | conversionWindow
  | proofRepair
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “task status”; its constructors are the cases that downstream code must handle.

inductive TaskStatus where
  | planned
  | active
  | blocked
  | leanCompiles
  | merged
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “artifact language”; its constructors are the cases that downstream code must handle.

inductive ArtifactLanguage where
  | lean
  | latex
  | markdown
  | json
  | csv
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “agent role”; its constructors are the cases that downstream code must handle.

inductive AgentRole where
  | upper
  | middle
  | lower
  | reviewer
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “agent backend kind”; its constructors are the cases that downstream code must handle.

inductive AgentBackendKind where
  | codex
  | claude
  | gpt
  | gemini
  | glm
  | minimax
  | localWrapper
  | custom
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “trial kind”; its constructors are the cases that downstream code must handle.

inductive TrialKind where
  | plan
  | attempt
  | build
  | review
  | proposal
  | compression
  | handoff
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “trial status”; its constructors are the cases that downstream code must handle.

inductive TrialStatus where
  | queued
  | running
  | blocked
  | failed
  | compiled
  | accepted
  | rejected
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “artifact spec”. A proposition-valued field is a requirement until a constructor supplies it.

structure ArtifactSpec where
  path : String
  language : ArtifactLanguage
  purpose : String
  mustCompile : Bool
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “acceptance gate”. A proposition-valued field is a requirement until a constructor supplies it.

structure AcceptanceGate where
  name : String
  command : String
  required : Bool
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “automation task”. A proposition-valued field is a requirement until a constructor supplies it.

structure AutomationTask where
  id : String
  title : String
  kind : TaskKind
  status : TaskStatus
  stage : AutomationStage
  source : String
  targetLean : String
  artifacts : List ArtifactSpec
  gates : List AcceptanceGate
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “agent contract”. A proposition-valued field is a requirement until a constructor supplies it.

structure AgentContract where
  role : AgentRole
  responsibility : String
  writes : List String
  mustLogTrial : Bool
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure TrialRecordSpec where
  logPath : String
  summaryPath : String
  requiredFields : List String
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “post cycle artifact kind”; its constructors are the cases that downstream code must handle.

inductive PostCycleArtifactKind where
  | preferredLanguageSummary
  | chatgptProPrompt
  | retrievalIndex
  | technicalReportUpdate
  | verifierFeedback
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure PostCycleArtifactSpec where
  kind : PostCycleArtifactKind
  pathPattern : String
  selfContainedForExternalModel : Bool
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure WorkflowCheckSpec where
  name : String
  checks : List String
  inspiredBy : String
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “candidate pool”; its constructors are the cases that downstream code must handle.

inductive CandidatePool where
  | insight
  | certified
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “lex elim scheduler mode”; its constructors are the cases that downstream code must handle.

inductive LexElimSchedulerMode where
  | lexElimOut
  | lexElimIn
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “lex objective class”; its constructors are the cases that downstream code must handle.

inductive LexObjectiveClass where
  | hardCorrectness
  | necessaryDiagnostic
  | asymptoticTier
  | concreteResource
  | proofProgress
  | processCost
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure LexObjectiveSpec where
  name : String
  priority : Nat
  objectiveClass : LexObjectiveClass
  hardGate : Bool
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure LexElimSchedulerSpec where
  mode : LexElimSchedulerMode
  useCase : String
  activeSet : String
  eliminationRule : String
  promotionRule : String
  inspiredBy : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure AgentPanelSizeSpec where
  taskClass : String
  upperCount : Nat
  middleCount : Nat
  lowerCount : Nat
  reviewerCount : Nat
  useWhen : String
  avoidWhen : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure AgentBackendProfileSpec where
  role : AgentRole
  slot : String
  allowedBackends : List AgentBackendKind
  commandProfileKey : String
  note : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure WorkflowInvariantSpec where
  name : String
  precondition : String
  requiredEvidence : List String
  rejectionReason : String
  inspiredBy : String
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def leanBuildGate : AcceptanceGate where
  name := "Lean build"
  command := "lake build && lake build Tests"
  required := true
  note := "Every automation run must leave the repository compiling."

commit-pinned source · Verso Blueprint panel

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

def noSorryGate : AcceptanceGate where
  name := "No new sorry by default"
  command := "rg -n \"\\bsorry\\b\" QuantumBlockEncoding Tests -g '!QuantumBlockEncoding/Automation.lean' || true"
  required := false
  note := "Skeleton files may use proposition-valued obligations, but finished tasks should avoid new sorry."

commit-pinned source · Verso Blueprint panel

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

def defaultGates : List AcceptanceGate :=
  [leanBuildGate, noSorryGate]

commit-pinned source · Verso Blueprint panel

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

def trialRecordSpec : TrialRecordSpec where
  logPath := "runs/trials.jsonl"
  summaryPath := "runs/trials_summary.csv"
  requiredFields := [
    "timestamp",
    "trial_id",
    "task_id",
    "role",
    "kind",
    "status",
    "lean_gate",

commit-pinned source · Verso Blueprint panel

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

def postCycleArtifactSpecs : List PostCycleArtifactSpec :=
  [
    {
      kind := PostCycleArtifactKind.preferredLanguageSummary
      pathPattern := "runs/<run-id>/summary.md"
      selfContainedForExternalModel := false
      note := "Human-facing source/operator audit in the user's configured report language."
    },
    {
      kind := PostCycleArtifactKind.chatgptProPrompt
      pathPattern := "runs/pro-prompts/<task-id>-latest.md"

commit-pinned source · Verso Blueprint panel

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

def workflowCheckSpecs : List WorkflowCheckSpec :=
  [
    {
      name := "Blueprint DAG refinement"
      checks := ["active leaf recorded", "solved nodes preserved", "failed route classified"]
      inspiredBy := "arXiv:2606.06468"
      note := "Goedel-Architect-like blueprint control, specialized to oracle/block-encoding leaves."
    },
    {
      name := "Agent trajectory audit"
      checks := ["required artifacts exist", "role handoff recorded", "stale route not reassigned unchanged"]

commit-pinned source · Verso Blueprint panel

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

def blockEncodingLexObjectiveSpecs : List LexObjectiveSpec :=
  [
    {
      name := "Lean-certified target correctness"
      priority := 0
      objectiveClass := LexObjectiveClass.hardCorrectness
      hardGate := true
      note := "Candidate must keep the fixed operator target and close the advertised unitarity/block-entry theorem before certification."
    },
    {
      name := "Necessary-condition diagnostics"

commit-pinned source · Verso Blueprint panel

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

def lexElimSchedulerSpecs : List LexElimSchedulerSpec :=
  [
    {
      mode := LexElimSchedulerMode.lexElimOut
      useCase := "faithful paper benchmark or delicate theorem closure"
      activeSet := "proof routes and candidate statements for one fixed source theorem"
      eliminationRule := "filter layer-by-layer: source faithfulness, Lean statement correctness, necessary diagnostics, then proof progress"
      promotionRule := "no candidate or route is promoted unless the corresponding Lean/source obligation for the current layer is satisfied"
      inspiredBy := "Xue et al. 2026 LexElim-Out for lexicographic bandits"
    },
    {

commit-pinned source · Verso Blueprint panel

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

def agentPanelSizeSpecs : List AgentPanelSizeSpec :=
  [
    {
      taskClass := "simple local Lean leaf"
      upperCount := 1
      middleCount := 1
      lowerCount := 1
      reviewerCount := 1
      useWhen := "target statement and dependencies are already precise"
      avoidWhen := "source correspondence, candidate population, or verifier feedback is stale"
    },

commit-pinned source · Verso Blueprint panel

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

def agentBackendProfileSpecs : List AgentBackendProfileSpec :=
  [
    {
      role := AgentRole.upper
      slot := "upper strategy and source/target audit"
      allowedBackends := [
        AgentBackendKind.codex,
        AgentBackendKind.claude,
        AgentBackendKind.gpt,
        AgentBackendKind.gemini,
        AgentBackendKind.glm,

commit-pinned source · Verso Blueprint panel

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

def workflowInvariantSpecs : List WorkflowInvariantSpec :=
  [
    {
      name := "Certified candidate promotion"
      precondition := "candidate is proposed by a lower architect, simulator, Python search, ChatGPT Pro, or paper baseline",
      requiredEvidence := ["Lean theorem closes the advertised unitarity/block-entry target", "resource record is attached", "reviewer confirms target operator did not change"],
      rejectionReason := "candidate remains in insight pool and cannot be plotted as solved or used as an evolutionary parent",
      inspiredBy := "arXiv:2606.06523 process verification plus EoH-style candidate archives"
    },
    {
      name := "Closeout artifacts for unfinished long run"

commit-pinned source · Verso Blueprint panel

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

def threeLayerAgentContracts : List AgentContract :=
  [
    {
      role := AgentRole.upper,
      responsibility := "Fix the operator target, choose candidate families or proof leaves, compress trial memory, and reject weak directions.",
      writes := ["runs/<run-id>/10_upper_director.md", "runs/<run-id>/90_handoff.md"],
      mustLogTrial := true
    },
    {
      role := AgentRole.middle,
      responsibility := "Maintain the operator/candidate Lean--Markdown--LaTeX conversion window and proof-obligation ledger.",

commit-pinned source · Verso Blueprint panel

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

def conversionArtifacts (stem : String) : List ArtifactSpec :=
  [
    {
      path := "tasks/" ++ stem ++ ".md",
      language := ArtifactLanguage.markdown,
      purpose := "Human-readable task contract and progress log.",
      mustCompile := false
    },
    {
      path := "paper-notes/" ++ stem ++ ".tex",
      language := ArtifactLanguage.latex,

commit-pinned source · Verso Blueprint panel

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

def seedAutomationTasks : List AutomationTask :=
  [
    {
      id := "QBE-AUTO-001",
      title := "Construct and score a block encoding for a user-specified query operator",
      kind := TaskKind.operatorBlockEncoding,
      status := TaskStatus.active,
      stage := AutomationStage.circuitSearch,
      source := "User-provided operator/matrix A, normalizer alpha, and block projector",
      targetLean := "QuantumBlockEncoding/BlockEncoding.lean",
      artifacts := conversionArtifacts "OperatorBlockEncodingCandidate",

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “automation task count”.

def automationTaskCount : Nat := seedAutomationTasks.length

commit-pinned source · Verso Blueprint panel