Theory /Cortex /Wire /SelectRecovery

Cortex.Wire.SelectRecovery

proofs

On this page

Overview
Context
Theorem Split
Durable Selected-Branch Records
Safe-Run Forwarding for Recovery Records

Imports

import Cortex.Wire.PhantomAdapter
import Cortex.Wire.PulseSafety

Overview

Recovery-facing proof surface for selected Wire branches.

Context

Cortex.Wire.Select proves that a selected latent branch lowers to the ordinary retained-owner appendAfter rewrite. Cortex.Wire.PulseSafety proves that constructed admitted rewrites preserve the combined Wire/Pulse safe-run envelope once runtime materialization supplies the next Pulse state.

This module connects those two surfaces to the durable recovery story. A selected branch recovery record is not a new graph operator. It records the already-selected SelectActualize witness together with the constructed planning step for its lowered append rewrite. A separate provenance predicate connects a recovered record to the persisted admission it claims to replay. Recovery does not re-run selector logic and it does not materialize unselected alternatives.

Theorem Split

The page proves:

a recovered record replays the same append rewrite as the persisted admission it is proven to come from;
equal selected-arm choices produce equal lowered append rewrites;
unselected branch nodes remain outside the replayed selected raw fragment;
a recovered phantom-adapter artifact can be tied to a concrete PhantomAdapterWitness inside the selected branch;
selected-branch recovery feeds the existing safe-run preservation theorem.

              namespace Cortex.Wireopen Cortex.Graphopen Cortex.Pulse

Durable Selected-Branch Records

section SelectedBranchRecoveryvariable {node arm : Type}variable [DecidableEq node]

Proof-side record for replaying one selected latent branch.

The record carries the selected arm and the constructed planner step for the lowered append rewrite. It intentionally does not contain selector code: after admission, recovery is replaying a selected rewrite, not re-evaluating the selector. Durable provenance is represented separately by SelectedBranchRecoveryRecord.Provenance.

structure SelectedBranchRecoveryRecord
    (family : LatentBranchFamily node arm)
    (policy : RuntimeNamespacePolicy node)
    (contractOk : Graph node → Prop)
    (context : PlanningContext node)
    (budget : RewriteBudget) : Type where

Selected branch chosen before recovery replay.

actualize : SelectActualize family

Runtime inserted-depth witness used by constructed planning.

insertedDepth : Nat

Remaining budget after admitting the selected rewrite.

remaining : RewriteBudget

Constructed planner step for the lowered selected append rewrite.

  step :
    ConstructedPlanningStep
      policy
      contractOk
      context
      budget
      actualize.toGraphRewrite
      insertedDepth
      remaining

Proof-side shape of a persisted selected-branch admission row.

This mirrors the durable lineage data that runtime correspondence must recover: the selected arm, inserted-depth witness, remaining budget, and constructed planner step for the selected append rewrite. The runtime proof obligation is to decode durable rewrite lineage into this shape and then into a recovery record.

structure PersistedSelectedBranchAdmission
    (family : LatentBranchFamily node arm)
    (policy : RuntimeNamespacePolicy node)
    (contractOk : Graph node → Prop)
    (context : PlanningContext node)
    (budget : RewriteBudget) : Type where

Selected branch persisted at admission time.

actualize : SelectActualize family

Persisted inserted-depth witness used by constructed planning.

insertedDepth : Nat

Persisted remaining budget after admitting the selected rewrite.

remaining : RewriteBudget

Persisted constructed planner step for the selected append rewrite.

  step :
    ConstructedPlanningStep
      policy
      contractOk
      context
      budget
      actualize.toGraphRewrite
      insertedDepth
      remaining

namespace SelectedBranchRecoveryRecordvariable {family : LatentBranchFamily node arm}variable {policy : RuntimeNamespacePolicy node}variable {contractOk : Graph node → Prop}variable {context : PlanningContext node}variable {budget : RewriteBudget}

The graph rewrite replayed from a selected-branch recovery record.

def replayedRewrite
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget) :
    GraphRewrite node :=
  record.actualize.toGraphRewrite

The selected raw fragment replayed by the recovery record before runtime namespacing.

def replayedSelectedFragment
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget) :
    SubgraphSpec node :=
  record.actualize.selectedFragment

Raw nodes in the selected fragment replayed by the recovery record.

def replayedSelectedNodes
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget) :
    Finset node :=
  record.actualize.selectedFragmentNodes

Runtime correspondence target for a phantom adapter persisted inside a recovered branch.

The executable artifact carries a concrete phantom-adapter node. Lean does not consume the JSON artifact directly here; instead, the correspondence layer must decode that row into this embedding: the artifact node is one node of the PhantomAdapterWitness.starInsertion graph, and every node in that star-insertion graph belongs to the selected raw fragment replayed by recovery.

structure PhantomAdapterEmbedding
    {outputPort inputPort productContract label : Type}
    [DecidableEq outputPort]
    [DecidableEq inputPort]
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    (witness :
      LinearPortGraph.PhantomAdapterWitness
        node
        outputPort
        inputPort
        productContract
        label)
    (artifactNode : node) :
    Prop where

The persisted artifact node is represented inside the phantom-adapter witness.

  artifactNode_mem_starInsertion :
    artifactNode ∈ (witness.starInsertion).graph.nodes

The complete star-insertion graph is part of the selected branch replayed by recovery.

  starInsertion_nodes_replayed :
    ∀ {nodeId},
      nodeId ∈ (witness.starInsertion).graph.nodes →
        nodeId ∈ record.replayedSelectedNodes

namespace PhantomAdapterEmbedding

A persisted phantom-adapter artifact node is replayed by the selected branch.

theorem artifactNode_replayed
    {outputPort inputPort productContract label : Type}
    [DecidableEq outputPort]
    [DecidableEq inputPort]
    {record :
      SelectedBranchRecoveryRecord family policy contractOk context budget}
    {witness :
      LinearPortGraph.PhantomAdapterWitness
        node
        outputPort
        inputPort
        productContract
        label}
    {artifactNode : node}
    (hEmbedding : PhantomAdapterEmbedding record witness artifactNode) :
    artifactNode ∈ record.replayedSelectedNodes :=
  hEmbedding.starInsertion_nodes_replayed hEmbedding.artifactNode_mem_starInsertion

end PhantomAdapterEmbedding

The replayed rewrite is the retained-owner append rewrite for the selected fragment.

theorem replayedRewrite_eq_appendAfter
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget) :
    record.replayedRewrite =
      GraphRewrite.appendAfter family.owner record.replayedSelectedFragment :=
  rfl

The recovery record exposes admissibility of its constructed proof-carrying step rewrite.

theorem step_toRewrite_admissible
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget) :
    admissible record.step.toRewrite context.topology budget :=
  ConstructedPlanningStep.toAdmissible record.step

Provenance relation between a persisted selected-branch admission and a recovered record.

The runtime correspondence layer must justify this relation from durable rewrite lineage. Lean then consumes it as the formal link that the recovered record is replaying the same selected admission, rather than merely naming a fresh selected branch.

structure Provenance
    (persisted recovered :
      SelectedBranchRecoveryRecord family policy contractOk context budget) :
    Prop where

Recovery preserves the persisted selected arm.

selected_eq : recovered.actualize.selected = persisted.actualize.selected

Recovery replays the persisted raw selected append rewrite.

replayedRewrite_eq : recovered.replayedRewrite = persisted.replayedRewrite

Recovery uses the same constructed rewrite delta.

delta_eq : recovered.step.delta = persisted.step.delta

Recovery carries the same remaining budget as the persisted admission.

remaining_eq : recovered.remaining = persisted.remainingnamespace Provenance

Provenance exposes equality of the raw replayed rewrite.

theorem replayedRewrite_eq_of_provenance
    {persisted recovered :
      SelectedBranchRecoveryRecord family policy contractOk context budget}
    (hProvenance : Provenance persisted recovered) :
    recovered.replayedRewrite = persisted.replayedRewrite :=
  hProvenance.replayedRewrite_eq

Provenance exposes equality of the constructed rewrite delta.

theorem delta_eq_of_provenance
    {persisted recovered :
      SelectedBranchRecoveryRecord family policy contractOk context budget}
    (hProvenance : Provenance persisted recovered) :
    recovered.step.delta = persisted.step.delta :=
  hProvenance.delta_eq

Provenance exposes equality of the remaining budget.

theorem remaining_eq_of_provenance
    {persisted recovered :
      SelectedBranchRecoveryRecord family policy contractOk context budget}
    (hProvenance : Provenance persisted recovered) :
    recovered.remaining = persisted.remaining :=
  hProvenance.remaining_eq

end Provenanceend SelectedBranchRecoveryRecordnamespace PersistedSelectedBranchAdmissionvariable {family : LatentBranchFamily node arm}variable {policy : RuntimeNamespacePolicy node}variable {contractOk : Graph node → Prop}variable {context : PlanningContext node}variable {budget : RewriteBudget}

Interpret a persisted selected-branch admission row as a recovery record.

def toRecoveryRecord
    (persisted :
      PersistedSelectedBranchAdmission family policy contractOk context budget) :
    SelectedBranchRecoveryRecord family policy contractOk context budget :=
  { actualize := persisted.actualize
    insertedDepth := persisted.insertedDepth
    remaining := persisted.remaining
    step := persisted.step }

Loading exactly the persisted admission row produces recovery provenance.

The executable correspondence target is the equality premise: Haskell recovery must show that decoding durable rewrite lineage yields this recovery record.

theorem provenance_of_recovered_eq
    (persisted :
      PersistedSelectedBranchAdmission family policy contractOk context budget)
    (recovered :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    (hRecovered : recovered = persisted.toRecoveryRecord) :
    SelectedBranchRecoveryRecord.Provenance persisted.toRecoveryRecord recovered := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetpersisted:PersistedSelectedBranchAdmission family policy contractOk context budgetrecovered:SelectedBranchRecoveryRecord family policy contractOk context budgethRecovered:recovered = persisted.toRecoveryRecord⊢ persisted.toRecoveryRecord.Provenance recovered
  cases hRecoveredreflnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetpersisted:PersistedSelectedBranchAdmission family policy contractOk context budget⊢ persisted.toRecoveryRecord.Provenance persisted.toRecoveryRecord
  exact
    { selected_eq := rfl
      replayedRewrite_eq := rfl
      delta_eq := rfl
      remaining_eq := rfl }All goals completed! 🐙

end PersistedSelectedBranchAdmission

Equal selected arms replay equal lowered append rewrites.

This is a functional-congruence fact about the selected-arm lowering, not a claim that selector execution is deterministic. Durable recovery determinism is stated separately using SelectedBranchRecoveryRecord.Provenance.

theorem replayedRewrite_eq_of_selected_eq
    {family : LatentBranchFamily node arm}
    {policy : RuntimeNamespacePolicy node}
    {contractOk : Graph node → Prop}
    {context : PlanningContext node}
    {budget : RewriteBudget}
    (left right :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    (hSelected : left.actualize.selected = right.actualize.selected) :
    left.replayedRewrite = right.replayedRewrite := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetleft:SelectedBranchRecoveryRecord family policy contractOk context budgetright:SelectedBranchRecoveryRecord family policy contractOk context budgethSelected:left.actualize.selected = right.actualize.selected⊢ left.replayedRewrite = right.replayedRewrite
  cases left with
  | mk leftActualize _leftDepth _leftRemaining _leftStep =>mknode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetright:SelectedBranchRecoveryRecord family policy contractOk context budgetleftActualize:SelectActualize family_leftDepth:ℕ_leftRemaining:RewriteBudget_leftStep:ConstructedPlanningStep policy contractOk context budget leftActualize.toGraphRewrite _leftDepth _leftRemaininghSelected:{ actualize := leftActualize, insertedDepth := _leftDepth, remaining := _leftRemaining,
        step := _leftStep }.actualize.selected =
  right.actualize.selected⊢ { actualize := leftActualize, insertedDepth := _leftDepth, remaining := _leftRemaining,
      step := _leftStep }.replayedRewrite =
  right.replayedRewrite
      cases right with
      | mk rightActualize _rightDepth _rightRemaining _rightStep =>mk.mknode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetleftActualize:SelectActualize family_leftDepth:ℕ_leftRemaining:RewriteBudget_leftStep:ConstructedPlanningStep policy contractOk context budget leftActualize.toGraphRewrite _leftDepth _leftRemainingrightActualize:SelectActualize family_rightDepth:ℕ_rightRemaining:RewriteBudget_rightStep:ConstructedPlanningStep policy contractOk context budget rightActualize.toGraphRewrite _rightDepth _rightRemaininghSelected:{ actualize := leftActualize, insertedDepth := _leftDepth, remaining := _leftRemaining,
        step := _leftStep }.actualize.selected =
  { actualize := rightActualize, insertedDepth := _rightDepth, remaining := _rightRemaining,
        step := _rightStep }.actualize.selected⊢ { actualize := leftActualize, insertedDepth := _leftDepth, remaining := _leftRemaining,
      step := _leftStep }.replayedRewrite =
  { actualize := rightActualize, insertedDepth := _rightDepth, remaining := _rightRemaining,
      step := _rightStep }.replayedRewrite
          cases leftActualize with
          | mk leftSelected _leftMem =>mk.mk.mknode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudget_leftDepth:ℕ_leftRemaining:RewriteBudgetrightActualize:SelectActualize family_rightDepth:ℕ_rightRemaining:RewriteBudget_rightStep:ConstructedPlanningStep policy contractOk context budget rightActualize.toGraphRewrite _rightDepth _rightRemainingleftSelected:arm_leftMem:leftSelected ∈ family.arms_leftStep:ConstructedPlanningStep policy contractOk context budget
  { selected := leftSelected, selected_mem := _leftMem }.toGraphRewrite _leftDepth _leftRemaininghSelected:{ actualize := { selected := leftSelected, selected_mem := _leftMem }, insertedDepth := _leftDepth,
        remaining := _leftRemaining, step := _leftStep }.actualize.selected =
  { actualize := rightActualize, insertedDepth := _rightDepth, remaining := _rightRemaining,
        step := _rightStep }.actualize.selected⊢ { actualize := { selected := leftSelected, selected_mem := _leftMem }, insertedDepth := _leftDepth,
      remaining := _leftRemaining, step := _leftStep }.replayedRewrite =
  { actualize := rightActualize, insertedDepth := _rightDepth, remaining := _rightRemaining,
      step := _rightStep }.replayedRewrite
              cases rightActualize with
              | mk rightSelected _rightMem =>mk.mk.mk.mknode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudget_leftDepth:ℕ_leftRemaining:RewriteBudget_rightDepth:ℕ_rightRemaining:RewriteBudgetleftSelected:arm_leftMem:leftSelected ∈ family.arms_leftStep:ConstructedPlanningStep policy contractOk context budget
  { selected := leftSelected, selected_mem := _leftMem }.toGraphRewrite _leftDepth _leftRemainingrightSelected:arm_rightMem:rightSelected ∈ family.arms_rightStep:ConstructedPlanningStep policy contractOk context budget
  { selected := rightSelected, selected_mem := _rightMem }.toGraphRewrite _rightDepth _rightRemaininghSelected:{ actualize := { selected := leftSelected, selected_mem := _leftMem }, insertedDepth := _leftDepth,
        remaining := _leftRemaining, step := _leftStep }.actualize.selected =
  { actualize := { selected := rightSelected, selected_mem := _rightMem }, insertedDepth := _rightDepth,
        remaining := _rightRemaining, step := _rightStep }.actualize.selected⊢ { actualize := { selected := leftSelected, selected_mem := _leftMem }, insertedDepth := _leftDepth,
      remaining := _leftRemaining, step := _leftStep }.replayedRewrite =
  { actualize := { selected := rightSelected, selected_mem := _rightMem }, insertedDepth := _rightDepth,
      remaining := _rightRemaining, step := _rightStep }.replayedRewrite
                  simp only
                    [ SelectedBranchRecoveryRecord.replayedRewrite
                    , SelectActualize.toGraphRewrite
                    , SelectActualize.selectedFragment
                    ] at hSelected ⊢mk.mk.mk.mknode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudget_leftDepth:ℕ_leftRemaining:RewriteBudget_rightDepth:ℕ_rightRemaining:RewriteBudgetleftSelected:arm_leftMem:leftSelected ∈ family.arms_leftStep:ConstructedPlanningStep policy contractOk context budget
  { selected := leftSelected, selected_mem := _leftMem }.toGraphRewrite _leftDepth _leftRemainingrightSelected:arm_rightMem:rightSelected ∈ family.arms_rightStep:ConstructedPlanningStep policy contractOk context budget
  { selected := rightSelected, selected_mem := _rightMem }.toGraphRewrite _rightDepth _rightRemaininghSelected:leftSelected = rightSelected⊢ GraphRewrite.appendAfter family.owner (family.fragment leftSelected) =
  GraphRewrite.appendAfter family.owner (family.fragment rightSelected)
                  cases hSelectedmk.mk.mk.mk.reflnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudget_leftDepth:ℕ_leftRemaining:RewriteBudget_rightDepth:ℕ_rightRemaining:RewriteBudgetleftSelected:arm_leftMem:leftSelected ∈ family.arms_leftStep:ConstructedPlanningStep policy contractOk context budget
  { selected := leftSelected, selected_mem := _leftMem }.toGraphRewrite _leftDepth _leftRemaining_rightMem:leftSelected ∈ family.arms_rightStep:ConstructedPlanningStep policy contractOk context budget
  { selected := leftSelected, selected_mem := _rightMem }.toGraphRewrite _rightDepth _rightRemaining⊢ GraphRewrite.appendAfter family.owner (family.fragment leftSelected) =
  GraphRewrite.appendAfter family.owner (family.fragment leftSelected)
                  rflAll goals completed! 🐙

Two recovered records with the same persisted provenance replay the same admission data.

The non-trivial recovery obligation is the provenance witness: it is the runtime correspondence fact that both records were loaded from the same persisted selected-branch admission. Once that witness is supplied, replay is deterministic for the raw selected append rewrite, constructed delta, and remaining budget.

theorem selectedBranch_recovery_deterministic
    {family : LatentBranchFamily node arm}
    {policy : RuntimeNamespacePolicy node}
    {contractOk : Graph node → Prop}
    {context : PlanningContext node}
    {budget : RewriteBudget}
    (persisted left right :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    (hLeft : SelectedBranchRecoveryRecord.Provenance persisted left)
    (hRight : SelectedBranchRecoveryRecord.Provenance persisted right) :
    left.replayedRewrite = right.replayedRewrite ∧
      left.step.delta = right.step.delta ∧
        left.remaining = right.remaining :=
  ⟨ hLeft.replayedRewrite_eq.trans hRight.replayedRewrite_eq.symm
  , ⟨ hLeft.delta_eq.trans hRight.delta_eq.symm
    , hLeft.remaining_eq.trans hRight.remaining_eq.symm
    ⟩
  ⟩

Recovery does not replay nodes from an unselected branch raw fragment.

theorem selectedBranch_unselected_not_replayed
    {family : LatentBranchFamily node arm}
    {policy : RuntimeNamespacePolicy node}
    {contractOk : Graph node → Prop}
    {context : PlanningContext node}
    {budget : RewriteBudget}
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    {unselected : arm}
    (hUnselectedMem : unselected ∈ family.arms)
    (hDifferent : unselected ≠ record.actualize.selected)
    {nodeId : node}
    (hNode : nodeId ∈ family.fragmentNodes unselected) :
    nodeId ∉ record.replayedSelectedNodes :=
  SelectActualize.selectActualize_unselected_not_in_selectedFragment
    record.actualize
    hUnselectedMem
    hDifferent
    hNode

Selected-branch recovery with an embedded phantom adapter stays linear and prunes other arms.

The embedding premise is the non-vacuous handoff: it ties the persisted phantom-adapter artifact and the proof-side PhantomAdapterWitness to the selected branch replayed by recovery. With that bridge, every star-insertion node is replayed as selected, while the same node cannot belong to any unselected branch fragment.

theorem selectedBranch_recovery_embeddedPhantomAdapter_linear_and_prunes
    {outputPort inputPort productContract label : Type}
    [DecidableEq outputPort]
    [DecidableEq inputPort]
    {family : LatentBranchFamily node arm}
    {policy : RuntimeNamespacePolicy node}
    {contractOk : Graph node → Prop}
    {context : PlanningContext node}
    {budget : RewriteBudget}
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    (witness :
      LinearPortGraph.PhantomAdapterWitness
        node
        outputPort
        inputPort
        productContract
        label)
    {artifactNode : node}
    (hEmbedding :
      SelectedBranchRecoveryRecord.PhantomAdapterEmbedding
        record
        witness
        artifactNode)
    {unselected : arm}
    (hUnselectedMem : unselected ∈ family.arms)
    (hDifferent : unselected ≠ record.actualize.selected)
    {adapterNode : node}
    (hAdapterNode : adapterNode ∈ (witness.starInsertion).graph.nodes) :
    (witness.starInsertion).graph.PortLinear ∧
      adapterNode ∈ record.replayedSelectedNodes ∧
        adapterNode ∉ family.fragmentNodes unselected := bynode:Typearm:Typeinst✝²:DecidableEq nodeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortfamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetwitness:LinearPortGraph.PhantomAdapterWitness node outputPort inputPort productContract labelartifactNode:nodehEmbedding:record.PhantomAdapterEmbedding witness artifactNodeunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedadapterNode:nodehAdapterNode:adapterNode ∈ witness.starInsertion.graph.nodes⊢ witness.starInsertion.graph.PortLinear ∧
  adapterNode ∈ record.replayedSelectedNodes ∧ adapterNode ∉ family.fragmentNodes unselected
  have hReplayed :
      adapterNode ∈ record.replayedSelectedNodes :=
    hEmbedding.starInsertion_nodes_replayed hAdapterNodenode:Typearm:Typeinst✝²:DecidableEq nodeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortfamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetwitness:LinearPortGraph.PhantomAdapterWitness node outputPort inputPort productContract labelartifactNode:nodehEmbedding:record.PhantomAdapterEmbedding witness artifactNodeunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedadapterNode:nodehAdapterNode:adapterNode ∈ witness.starInsertion.graph.nodeshReplayed:adapterNode ∈ record.replayedSelectedNodes⊢ witness.starInsertion.graph.PortLinear ∧
  adapterNode ∈ record.replayedSelectedNodes ∧ adapterNode ∉ family.fragmentNodes unselected
  have hPruned :
      adapterNode ∉ family.fragmentNodes unselected := bynode:Typearm:Typeinst✝²:DecidableEq nodeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortfamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetwitness:LinearPortGraph.PhantomAdapterWitness node outputPort inputPort productContract labelartifactNode:nodehEmbedding:record.PhantomAdapterEmbedding witness artifactNodeunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedadapterNode:nodehAdapterNode:adapterNode ∈ witness.starInsertion.graph.nodes⊢ witness.starInsertion.graph.PortLinear ∧
  adapterNode ∈ record.replayedSelectedNodes ∧ adapterNode ∉ family.fragmentNodes unselected
    intro hUnselectedNodenode:Typearm:Typeinst✝²:DecidableEq nodeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortfamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetwitness:LinearPortGraph.PhantomAdapterWitness node outputPort inputPort productContract labelartifactNode:nodehEmbedding:record.PhantomAdapterEmbedding witness artifactNodeunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedadapterNode:nodehAdapterNode:adapterNode ∈ witness.starInsertion.graph.nodeshReplayed:adapterNode ∈ record.replayedSelectedNodeshUnselectedNode:adapterNode ∈ family.fragmentNodes unselected⊢ False
    exact
      (selectedBranch_unselected_not_replayed
        record
        hUnselectedMem
        hDifferent
        hUnselectedNode)
        hReplayedAll goals completed! 🐙
  exact
    ⟨ LinearPortGraph.PhantomAdapterWitness.starInsertion_portLinear witness
    , ⟨ hReplayed, hPruned ⟩
    ⟩All goals completed! 🐙

The persisted phantom-adapter artifact node is replayed by the selected branch and absent from every unselected branch fragment.

theorem selectedBranch_recovery_embeddedPhantomAdapter_artifact_replayed_and_pruned
    {outputPort inputPort productContract label : Type}
    [DecidableEq outputPort]
    [DecidableEq inputPort]
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    (witness :
      LinearPortGraph.PhantomAdapterWitness
        node
        outputPort
        inputPort
        productContract
        label)
    {artifactNode : node}
    (hEmbedding :
      SelectedBranchRecoveryRecord.PhantomAdapterEmbedding
        record
        witness
        artifactNode)
    {unselected : arm}
    (hUnselectedMem : unselected ∈ family.arms)
    (hDifferent : unselected ≠ record.actualize.selected) :
    (witness.starInsertion).graph.PortLinear ∧
      artifactNode ∈ record.replayedSelectedNodes ∧
        artifactNode ∉ family.fragmentNodes unselected :=
  selectedBranch_recovery_embeddedPhantomAdapter_linear_and_prunes
    record
    witness
    hEmbedding
    hUnselectedMem
    hDifferent
    hEmbedding.artifactNode_mem_starInsertion

Namespaced unselected branch nodes are absent from the constructed delta topology.

This theorem needs a freshness premise for the unselected branch namespace: fragment disjointness rules out collisions with the selected inserted subgraph, while freshness rules out the same namespaced node already being present in the pre-rewrite context.

theorem selectedBranch_unselected_not_in_delta_topology
    {family : LatentBranchFamily node arm}
    {policy : RuntimeNamespacePolicy node}
    {contractOk : Graph node → Prop}
    {context : PlanningContext node}
    {budget : RewriteBudget}
    (record :
      SelectedBranchRecoveryRecord family policy contractOk context budget)
    {unselected : arm}
    (hUnselectedMem : unselected ∈ family.arms)
    (hDifferent : unselected ≠ record.actualize.selected)
    (hFresh :
      ∀ {nodeId},
        nodeId ∈ family.fragmentNodes unselected →
          policy.namespaceNode family.owner nodeId ∉ (denote context.topology).vertices)
    {nodeId : node}
    (hNode : nodeId ∈ family.fragmentNodes unselected) :
    policy.namespaceNode family.owner nodeId ∉
      (denote record.step.delta.topology).vertices := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
  intro hFinalnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).vertices⊢ False
  have hRuntimeSpecValid :
      (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.Valid := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
    simp only [runtimePlannerRewrite, namespaceGraphRewrite_spec]node:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).vertices⊢ (namespaceSubgraphSpec (policy.namespaceNode record.actualize.toGraphRewrite.anchor)
    record.actualize.toGraphRewrite.spec).Valid
    exact
      namespaceSubgraphSpec_preserves_valid
        (policy.namespaceNode_injective record.actualize.toGraphRewrite.anchor)
        record.step.inputs.rawSubgraphValidAll goals completed! 🐙
  have hAnchor :
      family.owner ∈ (denote context.topology).vertices := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
    simpa only [SelectActualize.toGraphRewrite, GraphRewrite.anchor] using
      record.step.inputs.anchorInTopologyAll goals completed! 🐙
  have hFinalRelation :
      policy.namespaceNode family.owner nodeId ∈
        (plannedFinalRelation
          context.topology
          (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
    simpa only
      [ ConstructedPlanningStep.delta
      , constructedPlannedRewriteDelta
      , constructedFinalRelation
      , denote_constructedFinalTopology
      ] using hFinalAll goals completed! 🐙
  have hVerticesEq :
      (plannedFinalRelation
        context.topology
        (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
        (denote context.topology).vertices ∪
          (denote
            (runtimePlannerRewrite policy
              record.actualize.toGraphRewrite).spec.topology).vertices := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
    simpa only
      [ SelectActualize.toGraphRewrite
      , runtimePlannerRewrite
      , namespaceGraphRewrite
      , GraphRewrite.anchor
      , GraphRewrite.spec
      , GraphRewrite.anchorDisposition
      ] using
        (plannedFinalRelation_vertices_append
          (context := context.topology)
          (anchor := family.owner)
          (spec := namespaceSubgraphSpec (policy.namespaceNode family.owner)
            record.actualize.selectedFragment)
          hAnchor
          hRuntimeSpecValid.entryNodesInside
          hRuntimeSpecValid.exitNodesInside)All goals completed! 🐙
  have hUnion :
      policy.namespaceNode family.owner nodeId ∈
        (denote context.topology).vertices ∪
          (denote
            (runtimePlannerRewrite policy
              record.actualize.toGraphRewrite).spec.topology).vertices := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
    simpa only [hVerticesEq] using hFinalRelationAll goals completed! 🐙
  rcases Finset.mem_union.mp hUnion with hOld | hInsertedinlnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshOld:policy.namespaceNode family.owner nodeId ∈ (denote context.topology).vertices⊢ Falseinrnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshInserted:policy.namespaceNode family.owner nodeId ∈
  (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).vertices⊢ False
  ·inlnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshOld:policy.namespaceNode family.owner nodeId ∈ (denote context.topology).vertices⊢ False exact hFresh hNode hOldAll goals completed! 🐙
  ·inrnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshInserted:policy.namespaceNode family.owner nodeId ∈
  (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).vertices⊢ False simp only
      [ SelectActualize.toGraphRewrite
      , runtimePlannerRewrite
      , namespaceGraphRewrite
      , GraphRewrite.spec
      , namespaceSubgraphSpec
      , denote_mapGraph
      , mapRelation
      , Finset.mem_image
      ] at hInsertedinrnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshInserted:∃ a ∈ (denote record.actualize.selectedFragment.topology).vertices,
  policy.namespaceNode (GraphRewrite.appendAfter family.owner record.actualize.selectedFragment).anchor a =
    policy.namespaceNode family.owner nodeId⊢ False
    rcases hInserted with ⟨selectedNode, hSelectedNode, hNamespacedEq⟩inrnode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticesselectedNode:nodehSelectedNode:selectedNode ∈ (denote record.actualize.selectedFragment.topology).verticeshNamespacedEq:policy.namespaceNode (GraphRewrite.appendAfter family.owner record.actualize.selectedFragment).anchor selectedNode =
  policy.namespaceNode family.owner nodeId⊢ False
    have hSelectedEq :
        selectedNode = nodeId := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
      apply policy.namespaceNode_injective family.owneranode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticesselectedNode:nodehSelectedNode:selectedNode ∈ (denote record.actualize.selectedFragment.topology).verticeshNamespacedEq:policy.namespaceNode (GraphRewrite.appendAfter family.owner record.actualize.selectedFragment).anchor selectedNode =
  policy.namespaceNode family.owner nodeId⊢ policy.namespaceNode family.owner selectedNode = policy.namespaceNode family.owner nodeId
      simpa only using hNamespacedEqAll goals completed! 🐙
    have hSelectedRaw :
        nodeId ∈ record.replayedSelectedNodes := bynode:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselected⊢ policy.namespaceNode family.owner nodeId ∉ (denote ⋯.delta.topology).vertices
      rw [← hSelectedEq]node:Typearm:Typeinst✝:DecidableEq nodefamily:LatentBranchFamily node armpolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetrecord:SelectedBranchRecoveryRecord family policy contractOk context budgetunselected:armhUnselectedMem:unselected ∈ family.armshDifferent:unselected ≠ record.actualize.selectedhFresh:∀ {nodeId : node},
  nodeId ∈ family.fragmentNodes unselected →
    policy.namespaceNode family.owner nodeId ∉ (denote context.topology).verticesnodeId:nodehNode:nodeId ∈ family.fragmentNodes unselectedhFinal:policy.namespaceNode family.owner nodeId ∈ (denote ⋯.delta.topology).verticeshRuntimeSpecValid:(runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.ValidhAnchor:family.owner ∈ (denote context.topology).verticeshFinalRelation:policy.namespaceNode family.owner nodeId ∈
  (plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).verticeshVerticesEq:(plannedFinalRelation context.topology (runtimePlannerRewrite policy record.actualize.toGraphRewrite)).vertices =
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticeshUnion:policy.namespaceNode family.owner nodeId ∈
  (denote context.topology).vertices ∪
    (denote (runtimePlannerRewrite policy record.actualize.toGraphRewrite).spec.topology).verticesselectedNode:nodehSelectedNode:selectedNode ∈ (denote record.actualize.selectedFragment.topology).verticeshNamespacedEq:policy.namespaceNode (GraphRewrite.appendAfter family.owner record.actualize.selectedFragment).anchor selectedNode =
  policy.namespaceNode family.owner nodeIdhSelectedEq:selectedNode = nodeId⊢ selectedNode ∈ record.replayedSelectedNodes
      simpa only
        [ SelectedBranchRecoveryRecord.replayedSelectedNodes
        , SelectActualize.selectedFragmentNodes
        , LatentBranchFamily.fragmentNodes
        , SelectActualize.selectedFragment
        ] using hSelectedNodeAll goals completed! 🐙
    exact
      (selectedBranch_unselected_not_replayed
        record
        hUnselectedMem
        hDifferent
        hNode)
        hSelectedRawAll goals completed! 🐙

end SelectedBranchRecovery

Safe-Run Forwarding for Recovery Records

section SafeRunStatevariable {executor config contract authority payload : Type}variable [DecidableEq contract]variable [DecidableEq (StagedExecutorNode executor config authority)]variable {registry : ExecutorRegistry executor config contract authority}variable {initialBudget remainingBudget : RewriteBudget}variable {context : PlanningContext (WireNode executor config authority)}variable {G : DAG (WireNode executor config authority)}variable {state : GraphState (WireNode executor config authority) payload}variable {policy : RuntimeNamespacePolicy (WireNode executor config authority)}variable {arm : Type}variable {family : LatentBranchFamily (WireNode executor config authority) arm}variable {nextG : DAG (WireNode executor config authority)}variable {nextState : GraphState (WireNode executor config authority) payload}
                  A selected-branch recovery record forwards to admitted-rewrite safe-run preservation.

                  The theorem consumes the same materialization witness as ordinary admitted
rewrites. Its contribution is connecting the durable selected-branch recovery
record to the existing SelectActualize safe-run theorem; recovery-specific
durable provenance is modeled by SelectedBranchRecoveryRecord.Provenance.
theorem selectedBranch_recovery_preserves_safeRunState
    (hSafe :
      SafeWireRunState registry initialBudget remainingBudget context G state)
    (record :
      SelectedBranchRecoveryRecord
        family
        policy
        (_root_.Cortex.Wire.registryBoundary registry)
        context
        remainingBudget)
    (hDelta : RegistryBoundaryDeltaAdmitted registry record.step.delta)
    (hMaterialized : MaterializedPulseState record.step.nextContext nextG nextState) :
    SafeWireRunState
      registry
      initialBudget
      record.remaining
      record.step.nextContext
      nextG
      nextState :=
  SafeWireRunState.selectActualize_preserves_safeRunState
    hSafe
    record.step
    hDelta
    hMaterializedend SafeRunStateend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.SelectAdmission Next →Packages