QuantumBlockEncoding/AutomationTrace.lean

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

inductive ThreeLayerPhase where
  | upperPlanning
  | middleRefinement
  | lowerAttempt
  | reviewerAudit
  | accepted
  | rejected
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

structure ThreeLayerHandoff where
  source : ThreeLayerPhase
  target : ThreeLayerPhase
  role : AgentRole
  trialLogged : Bool
  artifactCount : Nat
  leanGatePassed : Bool
  reviewerApproved : Bool
deriving Repr, DecidableEq

/-- Executable transition guard.  Acceptance is possible only from review. -/

commit-pinned source · Verso Blueprint panel

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

def ThreeLayerHandoff.validFlag (handoff : ThreeLayerHandoff) : Bool :=
  handoff.trialLogged &&
    decide (handoff.artifactCount > 0) &&
      match handoff.source, handoff.target, handoff.role with
      | .upperPlanning, .middleRefinement, .upper => true
      | .middleRefinement, .lowerAttempt, .middle => true
      | .lowerAttempt, .reviewerAudit, .lower => true
      | .reviewerAudit, .accepted, .reviewer =>
          handoff.leanGatePassed && handoff.reviewerApproved
      | .reviewerAudit, .rejected, .reviewer => true
      | _, _, _ => false

commit-pinned source · Verso Blueprint panel

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

def ThreeLayerHandoff.valid (handoff : ThreeLayerHandoff) : Prop :=
  handoff.validFlag = true

instance (handoff : ThreeLayerHandoff) : Decidable handoff.valid := by

commit-pinned source · Verso Blueprint panel

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.

structure ThreeLayerTrace where
  start : ThreeLayerPhase
  handoffs : List ThreeLayerHandoff
deriving Repr, DecidableEq

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

commit-pinned source · Verso Blueprint panel

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.

def ThreeLayerTrace.advance :
    ThreeLayerPhase → ThreeLayerHandoff → Option ThreeLayerPhase
  | current, handoff =>
      if current = handoff.source ∧ handoff.valid then some handoff.target else none

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

commit-pinned source · Verso Blueprint panel

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

def ThreeLayerTrace.finalPhase (trace : ThreeLayerTrace) : Option ThreeLayerPhase :=
  trace.handoffs.foldlM ThreeLayerTrace.advance trace.start

/-- Every handoff in a trace is locally valid. -/

commit-pinned source · Verso Blueprint panel

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

def ThreeLayerTrace.allValid (trace : ThreeLayerTrace) : Prop :=
  ∀ handoff ∈ trace.handoffs, handoff.valid

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

commit-pinned source · Verso Blueprint panel

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.

def threeLayerCanonicalTrace : ThreeLayerTrace where
  start := .upperPlanning
  handoffs :=
    [ { source := .upperPlanning
        target := .middleRefinement
        role := .upper
        trialLogged := true
        artifactCount := 2
        leanGatePassed := false
        reviewerApproved := false }
    , { source := .middleRefinement

commit-pinned source · Verso Blueprint panel

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

theorem threeLayerCanonicalTrace_allValid :
    threeLayerCanonicalTrace.allValid := by

commit-pinned source · Verso Blueprint panel

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.

theorem threeLayerCanonicalTrace_reachesAccepted :
    threeLayerCanonicalTrace.finalPhase = some .accepted := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

def threeLayerFailedGateTrace : ThreeLayerTrace where
  start := .upperPlanning
  handoffs :=
    threeLayerCanonicalTrace.handoffs.dropLast ++
      [ { source := .reviewerAudit
          target := .accepted
          role := .reviewer
          trialLogged := true
          artifactCount := 2
          leanGatePassed := false
          reviewerApproved := true } ]

commit-pinned source · Verso Blueprint panel

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.

theorem threeLayerFailedGateTrace_notAccepted :
    threeLayerFailedGateTrace.finalPhase ≠ some .accepted := by

commit-pinned source · Verso Blueprint panel