11.2. QuantumBlockEncoding/AutomationTrace.lean🔗

15 explicit public declarations, in source order.

Definition11.2.1

uses 0used by 0✓L∃∀N

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

Lean code for Definition11.2.1●1 definition

inductive(6 constructors)defined in QuantumBlockEncoding/AutomationTrace.lean

complete

inductive QuantumBlockEncoding.ThreeLayerPhase : Type

inductive QuantumBlockEncoding.ThreeLayerPhase :
  Type

Constructors

upperPlanning : QuantumBlockEncoding.ThreeLayerPhase

middleRefinement : QuantumBlockEncoding.ThreeLayerPhase

lowerAttempt : QuantumBlockEncoding.ThreeLayerPhase

reviewerAudit : QuantumBlockEncoding.ThreeLayerPhase

accepted : QuantumBlockEncoding.ThreeLayerPhase

rejected : QuantumBlockEncoding.ThreeLayerPhase

Definition11.2.2

uses 0used by 0✓L∃∀N

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

Lean code for Definition11.2.2●1 definition

structure(7 fields)defined in QuantumBlockEncoding/AutomationTrace.lean

complete

structure QuantumBlockEncoding.ThreeLayerHandoff : Type

structure QuantumBlockEncoding.ThreeLayerHandoff :
  Type

Fields

source : QuantumBlockEncoding.ThreeLayerPhase

target : QuantumBlockEncoding.ThreeLayerPhase

role : QuantumBlockEncoding.AgentRole

trialLogged : Bool

artifactCount : ℕ

leanGatePassed : Bool

reviewerApproved : Bool

Definition11.2.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “valid flag”. Executable transition guard.

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. Executable transition guard. Acceptance is possible only from review.

Declaration kind. def.

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

Lean code for Definition11.2.3●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.ThreeLayerHandoff.validFlag
  (handoff : QuantumBlockEncoding.ThreeLayerHandoff) : Bool

def QuantumBlockEncoding.ThreeLayerHandoff.validFlag
  (handoff :
    QuantumBlockEncoding.ThreeLayerHandoff) :
  Bool

Executable transition guard.  Acceptance is possible only from review.

Definition11.2.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “valid”. Propositional view of the executable transition guard.

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. Propositional view of the executable transition guard.

Declaration kind. def.

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

Lean code for Definition11.2.4●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.ThreeLayerHandoff.valid
  (handoff : QuantumBlockEncoding.ThreeLayerHandoff) : Prop

def QuantumBlockEncoding.ThreeLayerHandoff.valid
  (handoff :
    QuantumBlockEncoding.ThreeLayerHandoff) :
  Prop

Propositional view of the executable transition guard.

Definition11.2.5

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “three layer trace”. A proposition-valued field is a requirement until a constructor supplies it. One execution trace with an explicit starting phase.

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. One execution trace with an explicit starting phase.

Declaration kind. structure.

Source: QuantumBlockEncoding/AutomationTrace.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.2.5●1 definition

structure(2 fields)defined in QuantumBlockEncoding/AutomationTrace.lean

complete

structure QuantumBlockEncoding.ThreeLayerTrace : Type

structure QuantumBlockEncoding.ThreeLayerTrace :
  Type

One execution trace with an explicit starting phase.

Fields

start : QuantumBlockEncoding.ThreeLayerPhase

handoffs : List QuantumBlockEncoding.ThreeLayerHandoff

Definition11.2.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “advance”. Follow a handoff only when it starts at the current phase and is valid.

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. Follow a handoff only when it starts at the current phase and is valid.

Declaration kind. def.

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

Lean code for Definition11.2.6●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.ThreeLayerTrace.advance :
  QuantumBlockEncoding.ThreeLayerPhase →
    QuantumBlockEncoding.ThreeLayerHandoff →
      Option QuantumBlockEncoding.ThreeLayerPhase

def QuantumBlockEncoding.ThreeLayerTrace.advance :
  QuantumBlockEncoding.ThreeLayerPhase →
    QuantumBlockEncoding.ThreeLayerHandoff →
      Option
        QuantumBlockEncoding.ThreeLayerPhase

Follow a handoff only when it starts at the current phase and is valid.

Definition11.2.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “final phase”. Execute a trace left-to-right, rejecting the first invalid handoff.

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. Execute a trace left-to-right, rejecting the first invalid handoff.

Declaration kind. def.

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

Lean code for Definition11.2.7●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.ThreeLayerTrace.finalPhase
  (trace : QuantumBlockEncoding.ThreeLayerTrace) :
  Option QuantumBlockEncoding.ThreeLayerPhase

def QuantumBlockEncoding.ThreeLayerTrace.finalPhase
  (trace :
    QuantumBlockEncoding.ThreeLayerTrace) :
  Option
    QuantumBlockEncoding.ThreeLayerPhase

Execute a trace left-to-right, rejecting the first invalid handoff.

Definition11.2.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “all valid”. Every handoff in a trace is locally valid.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. Every handoff in a trace is locally valid.

Declaration kind. def.

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

Lean code for Definition11.2.8●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.ThreeLayerTrace.allValid
  (trace : QuantumBlockEncoding.ThreeLayerTrace) : Prop

def QuantumBlockEncoding.ThreeLayerTrace.allValid
  (trace :
    QuantumBlockEncoding.ThreeLayerTrace) :
  Prop

Every handoff in a trace is locally valid.

Definition11.2.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “three layer canonical trace”. Canonical upper-to-reviewer trace used as the finite teaching witness.

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. Canonical upper-to-reviewer trace used as the finite teaching witness.

Declaration kind. def.

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

Lean code for Definition11.2.9●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.threeLayerCanonicalTrace :
  QuantumBlockEncoding.ThreeLayerTrace

def QuantumBlockEncoding.threeLayerCanonicalTrace :
  QuantumBlockEncoding.ThreeLayerTrace

Canonical upper-to-reviewer trace used as the finite teaching witness.

Theorem11.2.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “three layer canonical trace all valid”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Technical source note. The 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. theorem.

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

Lean code for Theorem11.2.10●1 theorem

theoremdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

theorem QuantumBlockEncoding.threeLayerCanonicalTrace_allValid :
  QuantumBlockEncoding.threeLayerCanonicalTrace.allValid

theorem QuantumBlockEncoding.threeLayerCanonicalTrace_allValid :
  QuantumBlockEncoding.threeLayerCanonicalTrace.allValid

Theorem11.2.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “three layer canonical trace reaches accepted”; the hypotheses and conclusion in the code panel fix its exact scope. The canonical trace reaches acceptance without an external semantic axiom.

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

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

Technical source note. The canonical trace reaches acceptance without an external semantic axiom.

Declaration kind. theorem.

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

Lean code for Theorem11.2.11●1 theorem

theoremdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

theorem QuantumBlockEncoding.threeLayerCanonicalTrace_reachesAccepted :
  QuantumBlockEncoding.threeLayerCanonicalTrace.finalPhase =
    some QuantumBlockEncoding.ThreeLayerPhase.accepted

theorem QuantumBlockEncoding.threeLayerCanonicalTrace_reachesAccepted :
  QuantumBlockEncoding.threeLayerCanonicalTrace.finalPhase =
    some
      QuantumBlockEncoding.ThreeLayerPhase.accepted

The canonical trace reaches acceptance without an external semantic axiom.

Theorem11.2.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “three layer accepted requires lean gate”; the hypotheses and conclusion in the code panel fix its exact scope. Any locally valid acceptance transition records a passing Lean gate.

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

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

Technical source note. Any locally valid acceptance transition records a passing Lean gate.

Declaration kind. theorem.

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

Lean code for Theorem11.2.12●1 theorem

theoremdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

theorem QuantumBlockEncoding.threeLayerAccepted_requiresLeanGate
  (handoff : QuantumBlockEncoding.ThreeLayerHandoff)
  (valid : handoff.valid)
  (accepted :
    handoff.target = QuantumBlockEncoding.ThreeLayerPhase.accepted) :
  handoff.leanGatePassed = true

theorem QuantumBlockEncoding.threeLayerAccepted_requiresLeanGate
  (handoff :
    QuantumBlockEncoding.ThreeLayerHandoff)
  (valid : handoff.valid)
  (accepted :
    handoff.target =
      QuantumBlockEncoding.ThreeLayerPhase.accepted) :
  handoff.leanGatePassed = true

Any locally valid acceptance transition records a passing Lean gate.

Theorem11.2.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “three layer accepted requires reviewer approval”; the hypotheses and conclusion in the code panel fix its exact scope. Any locally valid acceptance transition also records reviewer approval.

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

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

Technical source note. Any locally valid acceptance transition also records reviewer approval.

Declaration kind. theorem.

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

Lean code for Theorem11.2.13●1 theorem

theoremdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

theorem QuantumBlockEncoding.threeLayerAccepted_requiresReviewerApproval
  (handoff : QuantumBlockEncoding.ThreeLayerHandoff)
  (valid : handoff.valid)
  (accepted :
    handoff.target = QuantumBlockEncoding.ThreeLayerPhase.accepted) :
  handoff.reviewerApproved = true

theorem QuantumBlockEncoding.threeLayerAccepted_requiresReviewerApproval
  (handoff :
    QuantumBlockEncoding.ThreeLayerHandoff)
  (valid : handoff.valid)
  (accepted :
    handoff.target =
      QuantumBlockEncoding.ThreeLayerPhase.accepted) :
  handoff.reviewerApproved = true

Any locally valid acceptance transition also records reviewer approval.

Definition11.2.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “three layer failed gate trace”. Removing the final Lean gate prevents the same trace from being accepted.

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. Removing the final Lean gate prevents the same trace from being accepted.

Declaration kind. def.

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

Lean code for Definition11.2.14●1 definition

defdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

def QuantumBlockEncoding.threeLayerFailedGateTrace :
  QuantumBlockEncoding.ThreeLayerTrace

def QuantumBlockEncoding.threeLayerFailedGateTrace :
  QuantumBlockEncoding.ThreeLayerTrace

Removing the final Lean gate prevents the same trace from being accepted.

Theorem11.2.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “three layer failed gate trace not accepted”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Technical source note. The 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. theorem.

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

Lean code for Theorem11.2.15●1 theorem

theoremdefined in QuantumBlockEncoding/AutomationTrace.lean

complete

theorem QuantumBlockEncoding.threeLayerFailedGateTrace_notAccepted :
  QuantumBlockEncoding.threeLayerFailedGateTrace.finalPhase ≠
    some QuantumBlockEncoding.ThreeLayerPhase.accepted

theorem QuantumBlockEncoding.threeLayerFailedGateTrace_notAccepted :
  QuantumBlockEncoding.threeLayerFailedGateTrace.finalPhase ≠
    some
      QuantumBlockEncoding.ThreeLayerPhase.accepted