Cortex.Wire.AdmissionArtifact.ReadySelect

proofs

On this page

Overview

Imports

import Cortex.Wire.AdmissionArtifact.ReadyPhantom

Overview

Validator-ready select admission accessors.

This page exposes component-domain, branch-shape, resolution, and latent body consequences for select admission rows in a validator-ready artifact.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Validator readiness exposes select row validity.

theorem validatorReady_select_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.Valid :=
  hReady.selectsValid selectAdmission hSelect

Validator readiness exposes select-artifact domain closure.

theorem validatorReady_select_domainClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    SelectAdmissionArtifact.DomainClosed artifact.nodes selectAdmission :=
  hReady.componentDomainsClosed.selectsClosed selectAdmission hSelect

Validator-ready select condition nodes belong to the top-level node summary.

theorem validatorReady_select_conditionNodeClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.conditionNode ∈ artifact.nodes :=
  (validatorReady_select_domainClosed hReady hSelect).conditionNodeClosed

Validator-ready select condition nodes appear in the component-role ledger.

theorem validatorReady_select_conditionNode_mem_componentRoleNodes
    {artifact : WireAdmissionArtifact}
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.conditionNode ∈ artifact.componentRoleNodes := byartifact:WireAdmissionArtifactselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ selectAdmission.conditionNode ∈ artifact.componentRoleNodes
  simp [componentRoleNodes]artifact:WireAdmissionArtifactselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ selectAdmission.conditionNode ∈ artifact.generatedUsedChildNodes ∨
  (∃ a ∈ artifact.phantomAdapters, a.node = selectAdmission.conditionNode) ∨
    ∃ a ∈ artifact.selects, a.conditionNode = selectAdmission.conditionNode
  exact Or.inr (Or.inr ⟨selectAdmission, hSelect, rfl⟩)All goals completed! 🐙

Validator-ready select condition nodes appear in the select-condition role ledger.

theorem validatorReady_select_conditionNode_mem_selectConditionNodes
    {artifact : WireAdmissionArtifact}
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.conditionNode ∈
      artifact.selects.map SelectAdmissionArtifact.conditionNode :=
  List.mem_map.mpr ⟨selectAdmission, hSelect, rfl⟩

Validator-ready generated child and phantom adapter component nodes cannot collide.

theorem validatorReady_generated_childNode_ne_phantomAdapter_node
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    child.node ≠ phantom.node := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ child.node ≠ phantom.node
  have hDisjoint :=
    validatorReady_generatedChildNodes_disjoint_phantomAdapterNodes hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)⊢ child.node ≠ phantom.node
  have hGeneratedNode :=
    validatorReady_generated_childNode_mem_generatedUsedChildNodes hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodes⊢ child.node ≠ phantom.node
  have hPhantomNode :=
    validatorReady_phantomAdapter_node_mem_phantomAdapterNodes hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodeshPhantomNode:phantom.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdapters⊢ child.node ≠ phantom.node
  intro hEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodeshPhantomNode:phantom.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdaptershEq:child.node = phantom.node⊢ False
  rw [← hEq] at hPhantomNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodeshPhantomNode:child.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdaptershEq:child.node = phantom.node⊢ False
  exact hDisjoint hGeneratedNode hPhantomNodeAll goals completed! 🐙

Validator-ready generated child and select condition component nodes cannot collide.

theorem validatorReady_generated_childNode_ne_select_conditionNode
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    child.node ≠ selectAdmission.conditionNode := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ child.node ≠ selectAdmission.conditionNode
  have hDisjoint :=
    validatorReady_generatedChildNodes_disjoint_selectConditionNodes hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)⊢ child.node ≠ selectAdmission.conditionNode
  have hGeneratedNode :=
    validatorReady_generated_childNode_mem_generatedUsedChildNodes hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodes⊢ child.node ≠ selectAdmission.conditionNode
  have hSelectNode :=
    validatorReady_select_conditionNode_mem_selectConditionNodes hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodeshSelectNode:selectAdmission.conditionNode ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selects⊢ child.node ≠ selectAdmission.conditionNode
  intro hEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodeshSelectNode:selectAdmission.conditionNode ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selectshEq:child.node = selectAdmission.conditionNode⊢ False
  rw [← hEq] at hSelectNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hGeneratedNode:child.node ∈ artifact.generatedUsedChildNodeshSelectNode:child.node ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selectshEq:child.node = selectAdmission.conditionNode⊢ False
  exact hDisjoint hGeneratedNode hSelectNodeAll goals completed! 🐙

Validator-ready phantom adapter and select condition component nodes cannot collide.

theorem validatorReady_phantomAdapter_node_ne_select_conditionNode
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    phantom.node ≠ selectAdmission.conditionNode := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ phantom.node ≠ selectAdmission.conditionNode
  have hDisjoint :=
    validatorReady_phantomAdapterNodes_disjoint_selectConditionNodes hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:(List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)⊢ phantom.node ≠ selectAdmission.conditionNode
  have hPhantomNode :=
    validatorReady_phantomAdapter_node_mem_phantomAdapterNodes hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:(List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hPhantomNode:phantom.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdapters⊢ phantom.node ≠ selectAdmission.conditionNode
  have hSelectNode :=
    validatorReady_select_conditionNode_mem_selectConditionNodes hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:(List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hPhantomNode:phantom.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdaptershSelectNode:selectAdmission.conditionNode ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selects⊢ phantom.node ≠ selectAdmission.conditionNode
  intro hEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:(List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hPhantomNode:phantom.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdaptershSelectNode:selectAdmission.conditionNode ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selectshEq:phantom.node = selectAdmission.conditionNode⊢ False
  rw [← hEq] at hSelectNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshDisjoint:(List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)hPhantomNode:phantom.node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdaptershSelectNode:phantom.node ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selectshEq:phantom.node = selectAdmission.conditionNode⊢ False
  exact hDisjoint hPhantomNode hSelectNodeAll goals completed! 🐙

Validator-ready latent select body nodes cannot reuse generated child component nodes.

theorem validatorReady_select_armBodyNode_ne_generated_childNode
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    {bodyNode : NodeId}
    (hBodyNode : bodyNode ∈ arm.bodyNodes)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    bodyNode ≠ child.node := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ bodyNode ≠ child.node
  have hFresh :=
    validatorReady_select_armBodyNodeFresh hReady hSelect hArm hBodyNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhFresh:bodyNode ∉ artifact.nodes⊢ bodyNode ≠ child.node
  have hClosed :=
    validatorReady_generated_childNodeClosed hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhFresh:bodyNode ∉ artifact.nodeshClosed:child.node ∈ artifact.nodes⊢ bodyNode ≠ child.node
  intro hEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhFresh:bodyNode ∉ artifact.nodeshClosed:child.node ∈ artifact.nodeshEq:bodyNode = child.node⊢ False
  rw [hEq] at hFreshartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhFresh:child.node ∉ artifact.nodeshClosed:child.node ∈ artifact.nodeshEq:bodyNode = child.node⊢ False
  exact hFresh hClosedAll goals completed! 🐙

Validator-ready latent select body nodes cannot reuse phantom-adapter component nodes.

theorem validatorReady_select_armBodyNode_ne_phantomAdapter_node
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    {bodyNode : NodeId}
    (hBodyNode : bodyNode ∈ arm.bodyNodes)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    bodyNode ≠ phantom.node := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ bodyNode ≠ phantom.node
  have hFresh :=
    validatorReady_select_armBodyNodeFresh hReady hSelect hArm hBodyNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershFresh:bodyNode ∉ artifact.nodes⊢ bodyNode ≠ phantom.node
  have hClosed :=
    validatorReady_phantomAdapter_nodeClosed hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershFresh:bodyNode ∉ artifact.nodeshClosed:phantom.node ∈ artifact.nodes⊢ bodyNode ≠ phantom.node
  intro hEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershFresh:bodyNode ∉ artifact.nodeshClosed:phantom.node ∈ artifact.nodeshEq:bodyNode = phantom.node⊢ False
  rw [hEq] at hFreshartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershFresh:phantom.node ∉ artifact.nodeshClosed:phantom.node ∈ artifact.nodeshEq:bodyNode = phantom.node⊢ False
  exact hFresh hClosedAll goals completed! 🐙

Validator-ready latent select body nodes cannot reuse select condition component nodes.

theorem validatorReady_select_armBodyNode_ne_select_conditionNode
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    {bodyNode : NodeId}
    (hBodyNode : bodyNode ∈ arm.bodyNodes)
    {otherSelect : SelectAdmissionArtifact}
    (hOtherSelect : otherSelect ∈ artifact.selects) :
    bodyNode ≠ otherSelect.conditionNode := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesotherSelect:SelectAdmissionArtifacthOtherSelect:otherSelect ∈ artifact.selects⊢ bodyNode ≠ otherSelect.conditionNode
  have hFresh :=
    validatorReady_select_armBodyNodeFresh hReady hSelect hArm hBodyNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesotherSelect:SelectAdmissionArtifacthOtherSelect:otherSelect ∈ artifact.selectshFresh:bodyNode ∉ artifact.nodes⊢ bodyNode ≠ otherSelect.conditionNode
  have hClosed :=
    validatorReady_select_conditionNodeClosed hReady hOtherSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesotherSelect:SelectAdmissionArtifacthOtherSelect:otherSelect ∈ artifact.selectshFresh:bodyNode ∉ artifact.nodeshClosed:otherSelect.conditionNode ∈ artifact.nodes⊢ bodyNode ≠ otherSelect.conditionNode
  intro hEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesotherSelect:SelectAdmissionArtifacthOtherSelect:otherSelect ∈ artifact.selectshFresh:bodyNode ∉ artifact.nodeshClosed:otherSelect.conditionNode ∈ artifact.nodeshEq:bodyNode = otherSelect.conditionNode⊢ False
  rw [hEq] at hFreshartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsbodyNode:NodeIdhBodyNode:bodyNode ∈ arm.bodyNodesotherSelect:SelectAdmissionArtifacthOtherSelect:otherSelect ∈ artifact.selectshFresh:otherSelect.conditionNode ∉ artifact.nodeshClosed:otherSelect.conditionNode ∈ artifact.nodeshEq:bodyNode = otherSelect.conditionNode⊢ False
  exact hFresh hClosedAll goals completed! 🐙

Validator-ready select variant ports belong to the top-level node summary.

theorem validatorReady_select_variantNodeClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {variant : SelectVariantArtifact}
    (hVariant : variant ∈ selectAdmission.variants) :
    variant.port.node ∈ artifact.nodes :=
  (validatorReady_select_domainClosed hReady hSelect).variantPortsClosed variant hVariant

Validator-ready select rows expose owner/condition equality.

theorem validatorReady_select_ownerMatchesCondition
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.OwnerMatchesCondition :=
  (validatorReady_select_valid hReady hSelect).ownerMatchesCondition

Validator-ready select rows expose permutation-level key coverage.

theorem validatorReady_select_keysCovered
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.KeysCovered :=
  (validatorReady_select_valid hReady hSelect).keysCovered

Validator-ready select rows expose unique base variant keys.

theorem validatorReady_select_variantKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.VariantKeysUnique :=
  (validatorReady_select_valid hReady hSelect).variantKeysUnique

Validator-ready select rows expose the exclusive-sum arity floor.

theorem validatorReady_select_variantsAtLeastTwo
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.VariantsAtLeastTwo :=
  (validatorReady_select_valid hReady hSelect).variantsAtLeastTwo

Validator-ready select rows expose the source exclusive group shared by every base variant.

theorem validatorReady_select_variantsShareExclusiveGroup
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.VariantsShareExclusiveGroup :=
  (validatorReady_select_valid hReady hSelect).variantsShareExclusiveGroup

Shared select variant groups force all variant rows to come from one source node.

theorem validatorReady_select_variants_sameSourceNode
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {left right : SelectVariantArtifact}
    (hLeft : left ∈ selectAdmission.variants)
    (hRight : right ∈ selectAdmission.variants) :
    left.port.node = right.port.node := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variants⊢ left.port.node = right.port.node
  obtain ⟨owner, index, hGroup⟩ :=
    validatorReady_select_variantsShareExclusiveGroup hReady hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)⊢ left.port.node = right.port.node
  have hRows : selectAdmission.RowsValid :=
    (validatorReady_select_valid hReady hSelect).rowsValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValid⊢ left.port.node = right.port.node
  have hLeftValid : left.Valid :=
    hRows.variantsValid left hLeftartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.Valid⊢ left.port.node = right.port.node
  have hRightValid : right.Valid :=
    hRows.variantsValid right hRightartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.ValidhRightValid:right.Valid⊢ left.port.node = right.port.node
  have hLeftLocal :
      left.port.ExclusiveGroupOwnerLocal :=
    AdmissionBoundaryPort.valid_exclusiveGroupOwnerLocal hLeftValid.portValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.ValidhRightValid:right.ValidhLeftLocal:left.port.ExclusiveGroupOwnerLocal⊢ left.port.node = right.port.node
  have hRightLocal :
      right.port.ExclusiveGroupOwnerLocal :=
    AdmissionBoundaryPort.valid_exclusiveGroupOwnerLocal hRightValid.portValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.ValidhRightValid:right.ValidhLeftLocal:left.port.ExclusiveGroupOwnerLocalhRightLocal:right.port.ExclusiveGroupOwnerLocal⊢ left.port.node = right.port.node
  unfold AdmissionBoundaryPort.ExclusiveGroupOwnerLocal at hLeftLocal hRightLocalartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.ValidhRightValid:right.ValidhLeftLocal:match left.port.exclusiveGroup with
| none => True
| some (owner, _index) => owner = left.port.nodehRightLocal:match right.port.exclusiveGroup with
| none => True
| some (owner, _index) => owner = right.port.node⊢ left.port.node = right.port.node
  rw [hGroup left hLeft] at hLeftLocalartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.ValidhRightValid:right.ValidhLeftLocal:match some (owner, index) with
| none => True
| some (owner, _index) => owner = left.port.nodehRightLocal:match right.port.exclusiveGroup with
| none => True
| some (owner, _index) => owner = right.port.node⊢ left.port.node = right.port.node
  rw [hGroup right hRight] at hRightLocalartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleft:SelectVariantArtifactright:SelectVariantArtifacthLeft:left ∈ selectAdmission.variantshRight:right ∈ selectAdmission.variantsowner:NodeIdindex:ℕhGroup:∀ variant ∈ selectAdmission.variants, variant.port.exclusiveGroup = some (owner, index)hRows:selectAdmission.RowsValidhLeftValid:left.ValidhRightValid:right.ValidhLeftLocal:match some (owner, index) with
| none => True
| some (owner, _index) => owner = left.port.nodehRightLocal:match some (owner, index) with
| none => True
| some (owner, _index) => owner = right.port.node⊢ left.port.node = right.port.node
  exact hLeftLocal.symm.trans hRightLocalAll goals completed! 🐙

Validator-ready select rows expose unique canonical arm keys.

theorem validatorReady_select_armCanonicalKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.ArmCanonicalKeysUnique :=
  (validatorReady_select_valid hReady hSelect).armCanonicalKeysUnique

Validator-ready select rows expose unique source-arm indexes.

theorem validatorReady_select_armSourceIndexesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.ArmSourceIndexesUnique :=
  (validatorReady_select_valid hReady hSelect).armSourceIndexesUnique

Validator-ready select rows expose source-order arm indexes.

theorem validatorReady_select_armSourceIndexesCanonical
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.ArmSourceIndexesCanonical :=
  (validatorReady_select_valid hReady hSelect).armSourceIndexesCanonical

Validator-ready select rows expose structural row validity.

theorem validatorReady_select_rowsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.RowsValid :=
  (validatorReady_select_valid hReady hSelect).rowsValid

Validator-ready select rows expose owner-node identifier validity.

theorem validatorReady_select_ownerValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.owner.Valid :=
  (validatorReady_select_rowsValid hReady hSelect).ownerValid

Validator-ready select rows expose condition-node identifier validity.

theorem validatorReady_select_conditionNodeValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.conditionNode.Valid :=
  (validatorReady_select_rowsValid hReady hSelect).conditionNodeValid

Validator-ready select rows expose structural validity of each base variant row.

theorem validatorReady_select_variant_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {variant : SelectVariantArtifact}
    (hVariant : variant ∈ selectAdmission.variants) :
    variant.Valid :=
  (validatorReady_select_rowsValid hReady hSelect).variantsValid
    variant hVariant

Validator-ready select variants expose valid canonical keys.

theorem validatorReady_select_variant_keyValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {variant : SelectVariantArtifact}
    (hVariant : variant ∈ selectAdmission.variants) :
    variant.key.Valid :=
  (validatorReady_select_variant_valid hReady hSelect hVariant).keyValid

Validator-ready select variants expose valid boundary ports.

theorem validatorReady_select_variant_portValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {variant : SelectVariantArtifact}
    (hVariant : variant ∈ selectAdmission.variants) :
    variant.port.Valid :=
  (validatorReady_select_variant_valid hReady hSelect hVariant).portValid

Validator-ready select rows expose structural validity of each serialized arm row.

theorem validatorReady_select_arm_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.Valid :=
  (validatorReady_select_rowsValid hReady hSelect).armsValid arm hArm

Validator-ready select arms expose valid source keys.

theorem validatorReady_select_arm_sourceKeyValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.sourceKey.Valid :=
  (validatorReady_select_arm_valid hReady hSelect hArm).sourceKeyValid

Validator-ready select arms expose valid canonical keys.

theorem validatorReady_select_arm_canonicalKeyValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.canonicalKey.Valid :=
  (validatorReady_select_arm_valid hReady hSelect hArm).canonicalKeyValid

Validator-ready select arm rows expose body-boundary closure over the latent body nodes.

theorem validatorReady_select_arm_bodyBoundariesClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.BodyBoundariesClosed :=
  (validatorReady_select_arm_valid hReady hSelect hArm).bodyBoundariesClosed

Validator-ready select arm body entries are closed over the latent body nodes.

theorem validatorReady_select_arm_bodyEntriesClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    BoundaryPortsClosed arm.bodyNodes arm.bodyEntries :=
  (validatorReady_select_arm_bodyBoundariesClosed hReady hSelect hArm).left

Validator-ready select arm body exits are closed over the latent body nodes.

theorem validatorReady_select_arm_bodyExitsClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    BoundaryPortsClosed arm.bodyNodes arm.bodyExits :=
  (validatorReady_select_arm_bodyBoundariesClosed hReady hSelect hArm).right

Validator-ready select arm rows expose duplicate-free latent body rows.

theorem validatorReady_select_arm_bodyRowsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.BodyRowsUnique :=
  (validatorReady_select_arm_valid hReady hSelect hArm).bodyRowsUnique

Validator-ready select arm body nodes are duplicate-free.

theorem validatorReady_select_arm_bodyNodesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.bodyNodes.Nodup :=
  (validatorReady_select_arm_bodyRowsUnique hReady hSelect hArm).left

Validator-ready select arm body entry rows are duplicate-free by endpoint key.

theorem validatorReady_select_arm_bodyEntryKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.bodyEntryKeys.Nodup :=
  (validatorReady_select_arm_bodyRowsUnique hReady hSelect hArm).right.left

Validator-ready select arm body exit rows are duplicate-free by endpoint key.

theorem validatorReady_select_arm_bodyExitKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.bodyExitKeys.Nodup :=
  (validatorReady_select_arm_bodyRowsUnique hReady hSelect hArm).right.right

Validator-ready select arm body nodes carry valid node identifiers.

theorem validatorReady_select_arm_bodyNodeValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    {node : NodeId}
    (hNode : node ∈ arm.bodyNodes) :
    node.Valid :=
  (validatorReady_select_arm_valid hReady hSelect hArm).bodyNodesValid
    node hNode

Validator-ready select arms expose valid latent body entry rows.

theorem validatorReady_select_arm_bodyEntriesValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    BoundaryPortsValid arm.bodyEntries :=
  (validatorReady_select_arm_valid hReady hSelect hArm).bodyEntriesValid

Validator-ready select arms expose valid latent body exit rows.

theorem validatorReady_select_arm_bodyExitsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    BoundaryPortsValid arm.bodyExits :=
  (validatorReady_select_arm_valid hReady hSelect hArm).bodyExitsValid

Validator-ready select arms expose validity of each latent body entry row.

theorem validatorReady_select_arm_bodyEntryValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    {entry : AdmissionBoundaryPort}
    (hEntry : entry ∈ arm.bodyEntries) :
    entry.Valid :=
  validatorReady_select_arm_bodyEntriesValid hReady hSelect hArm entry hEntry

Validator-ready select arms expose validity of each latent body exit row.

theorem validatorReady_select_arm_bodyExitValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    {exit : AdmissionBoundaryPort}
    (hExit : exit ∈ arm.bodyExits) :
    exit.Valid :=
  validatorReady_select_arm_bodyExitsValid hReady hSelect hArm exit hExit

Validator-ready select rows expose canonicalized label-first keys for base variants.

theorem validatorReady_select_variant_keyCanonical
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {variant : SelectVariantArtifact}
    (hVariant : variant ∈ selectAdmission.variants) :
    variant.KeyCanonical :=
  let hRows := validatorReady_select_rowsValid hReady hSelect
  SelectVariantArtifact.valid_keyCanonical (hRows.variantsValid variant hVariant)

Validator-ready select rows expose label-first resolution-mode soundness.

theorem validatorReady_select_armResolutionSound
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.ArmResolutionSound :=
  (validatorReady_select_valid hReady hSelect).armResolutionSound

Validator-ready select arms expose their label-first resolution evidence.

theorem validatorReady_select_armResolution
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    match arm.mode with
    | SelectResolutionMode.resolvedByLabel =>
        arm.sourceKey = arm.canonicalKey ∧
          ∃ variant, variant ∈ selectAdmission.variants ∧
            variant.key = arm.canonicalKey ∧
            variant.port.label = AdmissionPortLabel.label arm.sourceKey
    | SelectResolutionMode.resolvedByContract =>
        (∀ variant, variant ∈ selectAdmission.variants →
          variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
          (∀ variant, variant ∈ selectAdmission.variants →
            (variant.port.contract.name = arm.sourceKey.name ↔
              variant.key = arm.canonicalKey)) :=
  validatorReady_select_armResolutionSound hReady hSelect arm hArm

Validator-ready label-resolved select arms expose their resolved variant directly.

theorem validatorReady_select_labelResolved_variant
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    (hMode : arm.mode = SelectResolutionMode.resolvedByLabel) :
    arm.sourceKey = arm.canonicalKey ∧
      ∃ variant, variant ∈ selectAdmission.variants ∧
        variant.key = arm.canonicalKey ∧
        variant.port.label = AdmissionPortLabel.label arm.sourceKey := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabel⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
  have hResolution :=
    validatorReady_select_armResolution hReady hSelect hArmartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhResolution:match arm.mode with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKey⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
  rw [hMode] at hResolutionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhResolution:match SelectResolutionMode.resolvedByLabel with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKey⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
  exact hResolutionAll goals completed! 🐙

Validator-ready label-resolved arms identify a unique labeled variant.

The executable resolver takes the label branch before contract fallback. Once a label branch is serialized, variant-key uniqueness plus canonical variant keys make the labeled target unique.

theorem validatorReady_select_labelResolved_uniqueVariant
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    (hMode : arm.mode = SelectResolutionMode.resolvedByLabel) :
    arm.sourceKey = arm.canonicalKey ∧
      ∃ variant, variant ∈ selectAdmission.variants ∧
        variant.key = arm.canonicalKey ∧
          variant.port.label = AdmissionPortLabel.label arm.sourceKey ∧
          ∀ other, other ∈ selectAdmission.variants →
            other.port.label = AdmissionPortLabel.label arm.sourceKey →
              other = variant := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabel⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.label = AdmissionPortLabel.label arm.sourceKey ∧
        ∀ other ∈ selectAdmission.variants, other.port.label = AdmissionPortLabel.label arm.sourceKey → other = variant
  obtain ⟨hSourceKey, variant, hVariant, hVariantKey, hVariantLabel⟩ :=
    validatorReady_select_labelResolved_variant hReady hSelect hArm hModeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKey⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.label = AdmissionPortLabel.label arm.sourceKey ∧
        ∀ other ∈ selectAdmission.variants, other.port.label = AdmissionPortLabel.label arm.sourceKey → other = variant
  have hKeysUnique :=
    validatorReady_select_variantKeysUnique hReady hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKeyhKeysUnique:selectAdmission.VariantKeysUnique⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.label = AdmissionPortLabel.label arm.sourceKey ∧
        ∀ other ∈ selectAdmission.variants, other.port.label = AdmissionPortLabel.label arm.sourceKey → other = variant
  have hUnique :
      ∀ other, other ∈ selectAdmission.variants →
        other.port.label = AdmissionPortLabel.label arm.sourceKey →
          other = variant := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabel⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.label = AdmissionPortLabel.label arm.sourceKey ∧
        ∀ other ∈ selectAdmission.variants, other.port.label = AdmissionPortLabel.label arm.sourceKey → other = variant
    intro other hOtherartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKeyhKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variants⊢ other.port.label = AdmissionPortLabel.label arm.sourceKey → other = variant hOtherLabelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKeyhKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variantshOtherLabel:other.port.label = AdmissionPortLabel.label arm.sourceKey⊢ other = variant
    have hOtherCanonical :=
      validatorReady_select_variant_keyCanonical hReady hSelect hOtherartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKeyhKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variantshOtherLabel:other.port.label = AdmissionPortLabel.label arm.sourceKeyhOtherCanonical:other.KeyCanonical⊢ other = variant
    have hOtherKeySource : other.key = arm.sourceKey := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabel⊢ arm.sourceKey = arm.canonicalKey ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.label = AdmissionPortLabel.label arm.sourceKey ∧
        ∀ other ∈ selectAdmission.variants, other.port.label = AdmissionPortLabel.label arm.sourceKey → other = variant
      unfold SelectVariantArtifact.KeyCanonical at hOtherCanonicalartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKeyhKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variantshOtherLabel:other.port.label = AdmissionPortLabel.label arm.sourceKeyhOtherCanonical:other.key = other.port.selectKey⊢ other.key = arm.sourceKey
      simpa [AdmissionBoundaryPort.selectKey, hOtherLabel] using hOtherCanonicalAll goals completed! 🐙
    have hOtherKey : other.key = arm.canonicalKey :=
      hOtherKeySource.trans hSourceKeyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByLabelhSourceKey:arm.sourceKey = arm.canonicalKeyvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhVariantLabel:variant.port.label = AdmissionPortLabel.label arm.sourceKeyhKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variantshOtherLabel:other.port.label = AdmissionPortLabel.label arm.sourceKeyhOtherCanonical:other.KeyCanonicalhOtherKeySource:other.key = arm.sourceKeyhOtherKey:other.key = arm.canonicalKey⊢ other = variant
    exact
      List.inj_on_of_nodup_map hKeysUnique
        hOther
        hVariant
        (hOtherKey.trans hVariantKey.symm)All goals completed! 🐙
  exact
    ⟨ hSourceKey
    , ⟨ variant, hVariant, hVariantKey, hVariantLabel, hUnique ⟩
    ⟩All goals completed! 🐙

Validator-ready select arm keys are covered by base variants.

theorem validatorReady_select_armCanonicalKey_mem_variantKeys
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    arm.canonicalKey ∈ selectAdmission.variantKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.arms⊢ arm.canonicalKey ∈ selectAdmission.variantKeys
  have hCovered := validatorReady_select_keysCovered hReady hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshCovered:selectAdmission.KeysCovered⊢ arm.canonicalKey ∈ selectAdmission.variantKeys
  have hArmKey : arm.canonicalKey ∈ selectAdmission.armCanonicalKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.arms⊢ arm.canonicalKey ∈ selectAdmission.variantKeys
    exact List.mem_map.mpr ⟨arm, hArm, rfl⟩All goals completed! 🐙
  exact hCovered.mem_iff.mp hArmKeyAll goals completed! 🐙

Validator-ready contract-fallback arms identify a unique unshadowed variant.

The executable resolver tries labels first and then admits a contract-name fallback only when exactly one base variant has that contract.

theorem validatorReady_select_contractResolved_uniqueVariant
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms)
    (hMode : arm.mode = SelectResolutionMode.resolvedByContract) :
    (∀ variant, variant ∈ selectAdmission.variants →
      variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
      ∃ variant, variant ∈ selectAdmission.variants ∧
        variant.key = arm.canonicalKey ∧
          variant.port.contract.name = arm.sourceKey.name ∧
          ∀ other, other ∈ selectAdmission.variants →
            other.port.contract.name = arm.sourceKey.name → other = variant := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContract⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  have hResolution :=
    validatorReady_select_armResolution hReady hSelect hArmartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthResolution:match arm.mode with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKey⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  rw [hMode] at hResolutionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthResolution:match SelectResolutionMode.resolvedByContract with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKey⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  rcases hResolution with ⟨hNoLabel, hContractIff⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKey⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  have hKeyMem :=
    validatorReady_select_armCanonicalKey_mem_variantKeys hReady hSelect hArmartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeys⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  rcases List.mem_map.mp hKeyMem with ⟨variant, hVariant, hVariantKey⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeysvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKey⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  have hContract :
      variant.port.contract.name = arm.sourceKey.name :=
    (hContractIff variant hVariant).mpr hVariantKeyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeysvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhContract:variant.port.contract.name = arm.sourceKey.name⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  have hKeysUnique :=
    validatorReady_select_variantKeysUnique hReady hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeysvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhContract:variant.port.contract.name = arm.sourceKey.namehKeysUnique:selectAdmission.VariantKeysUnique⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
  have hUnique :
      ∀ other, other ∈ selectAdmission.variants →
        other.port.contract.name = arm.sourceKey.name → other = variant := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContract⊢ (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      variant.port.contract.name = arm.sourceKey.name ∧
        ∀ other ∈ selectAdmission.variants, other.port.contract.name = arm.sourceKey.name → other = variant
    intro other hOtherartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeysvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhContract:variant.port.contract.name = arm.sourceKey.namehKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variants⊢ other.port.contract.name = arm.sourceKey.name → other = variant hOtherContractartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeysvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhContract:variant.port.contract.name = arm.sourceKey.namehKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variantshOtherContract:other.port.contract.name = arm.sourceKey.name⊢ other = variant
    have hOtherKey :
        other.key = arm.canonicalKey :=
      (hContractIff other hOther).mp hOtherContractartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshMode:arm.mode = SelectResolutionMode.resolvedByContracthNoLabel:∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKeyhContractIff:∀ variant ∈ selectAdmission.variants, variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhKeyMem:arm.canonicalKey ∈ selectAdmission.variantKeysvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhContract:variant.port.contract.name = arm.sourceKey.namehKeysUnique:selectAdmission.VariantKeysUniqueother:SelectVariantArtifacthOther:other ∈ selectAdmission.variantshOtherContract:other.port.contract.name = arm.sourceKey.namehOtherKey:other.key = arm.canonicalKey⊢ other = variant
    exact
      List.inj_on_of_nodup_map hKeysUnique
        hOther
        hVariant
        (hOtherKey.trans hVariantKey.symm)All goals completed! 🐙
  exact
    ⟨ hNoLabel
    , ⟨ variant, hVariant, hVariantKey, hContract, hUnique ⟩
    ⟩All goals completed! 🐙

Validator-ready select variant keys are covered by source arms.

theorem validatorReady_select_variantKey_mem_armCanonicalKeys
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {variant : SelectVariantArtifact}
    (hVariant : variant ∈ selectAdmission.variants) :
    variant.key ∈ selectAdmission.armCanonicalKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variants⊢ variant.key ∈ selectAdmission.armCanonicalKeys
  have hCovered := validatorReady_select_keysCovered hReady hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshCovered:selectAdmission.KeysCovered⊢ variant.key ∈ selectAdmission.armCanonicalKeys
  have hVariantKey : variant.key ∈ selectAdmission.variantKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variants⊢ variant.key ∈ selectAdmission.armCanonicalKeys
    exact List.mem_map.mpr ⟨variant, hVariant, rfl⟩All goals completed! 🐙
  exact hCovered.mem_iff.mpr hVariantKeyAll goals completed! 🐙

Validator readiness exposes select key-cardinality for every select row.

theorem validatorReady_select_arms_length_eq
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    selectAdmission.arms.length = selectAdmission.variants.length :=
  SelectAdmissionArtifact.keysCovered_length_eq
    (validatorReady_select_keysCovered hReady hSelect)

Validator readiness exposes that a select row carries at least two admitted arms.

theorem validatorReady_select_armsAtLeastTwo
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects) :
    2 ≤ selectAdmission.arms.length := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ 2 ≤ selectAdmission.arms.length
  rw [validatorReady_select_arms_length_eq hReady hSelect]artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ 2 ≤ selectAdmission.variants.length
  exact validatorReady_select_variantsAtLeastTwo hReady hSelectAll goals completed! 🐙

Validator-ready select latent entries come from decoded source arm rows.

theorem validatorReady_select_latentEntry_sourceArm
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {entry : SelectArmKey × SelectArmAdmissionArtifact}
    (hEntry :
      entry ∈
        (selectAdmission.toLatentSelectAdmission
          (validatorReady_select_valid hReady hSelect)).entries) :
    ∃ arm, arm ∈ selectAdmission.arms ∧
      entry = (arm.canonicalSelectArmKey, arm) :=
  SelectAdmissionArtifact.toLatentSelectAdmission_entry_sourceArm hEntry

Validator-ready latent entry keys match their decoded source arm canonical keys.

theorem validatorReady_select_latentEntry_key_eq_bodyCanonical
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {entry : SelectArmKey × SelectArmAdmissionArtifact}
    (hEntry :
      entry ∈
        (selectAdmission.toLatentSelectAdmission
          (validatorReady_select_valid hReady hSelect)).entries) :
    entry.fst = entry.snd.canonicalSelectArmKey :=
  SelectAdmissionArtifact.toLatentSelectAdmission_entry_key_eq_bodyCanonical hEntry

Validator-ready select latent body rows retain their row-level validity.

theorem validatorReady_select_latentEntry_body_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {entry : SelectArmKey × SelectArmAdmissionArtifact}
    (hEntry :
      entry ∈
        (selectAdmission.toLatentSelectAdmission
          (validatorReady_select_valid hReady hSelect)).entries) :
    entry.snd.Valid :=
  SelectAdmissionArtifact.toLatentSelectAdmission_entry_body_valid hEntry

Validator-ready latent select body nodes are fresh from the top-level summary.

theorem validatorReady_select_latentEntry_bodyNodeFresh
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {entry : SelectArmKey × SelectArmAdmissionArtifact}
    (hEntry :
      entry ∈
        (selectAdmission.toLatentSelectAdmission
          (validatorReady_select_valid hReady hSelect)).entries)
    {node : NodeId}
    (hNode : node ∈ entry.snd.bodyNodes) :
    node ∉ artifact.nodes := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entriesnode:NodeIdhNode:node ∈ entry.2.bodyNodes⊢ node ∉ artifact.nodes
  obtain ⟨arm, hArm, hEq⟩ :=
    validatorReady_select_latentEntry_sourceArm hReady hSelect hEntryartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entriesnode:NodeIdhNode:node ∈ entry.2.bodyNodesarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshEq:entry = (arm.canonicalSelectArmKey, arm)⊢ node ∉ artifact.nodes
  cases hEqreflartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsnode:NodeIdarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshEntry:(arm.canonicalSelectArmKey, arm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshNode:node ∈ (arm.canonicalSelectArmKey, arm).2.bodyNodes⊢ node ∉ artifact.nodes
  exact validatorReady_select_armBodyNodeFresh hReady hSelect hArm hNodeAll goals completed! 🐙

Validator-ready latent select entries with distinct keys have disjoint body node domains.

theorem validatorReady_select_latentEntries_bodyNodesDisjoint
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {leftEntry rightEntry : SelectArmKey × SelectArmAdmissionArtifact}
    (hLeftEntry :
      leftEntry ∈
        (selectAdmission.toLatentSelectAdmission
          (validatorReady_select_valid hReady hSelect)).entries)
    (hRightEntry :
      rightEntry ∈
        (selectAdmission.toLatentSelectAdmission
          (validatorReady_select_valid hReady hSelect)).entries)
    (hKeys : leftEntry.fst ≠ rightEntry.fst)
    {node : NodeId}
    (hNode : node ∈ leftEntry.snd.bodyNodes) :
    node ∉ rightEntry.snd.bodyNodes := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleftEntry:SelectArmKey × SelectArmAdmissionArtifactrightEntry:SelectArmKey × SelectArmAdmissionArtifacthLeftEntry:leftEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshRightEntry:rightEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:leftEntry.1 ≠ rightEntry.1node:NodeIdhNode:node ∈ leftEntry.2.bodyNodes⊢ node ∉ rightEntry.2.bodyNodes
  obtain ⟨leftArm, hLeftArm, hLeftEq⟩ :=
    validatorReady_select_latentEntry_sourceArm hReady hSelect hLeftEntryartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleftEntry:SelectArmKey × SelectArmAdmissionArtifactrightEntry:SelectArmKey × SelectArmAdmissionArtifacthLeftEntry:leftEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshRightEntry:rightEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:leftEntry.1 ≠ rightEntry.1node:NodeIdhNode:node ∈ leftEntry.2.bodyNodesleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armshLeftEq:leftEntry = (leftArm.canonicalSelectArmKey, leftArm)⊢ node ∉ rightEntry.2.bodyNodes
  obtain ⟨rightArm, hRightArm, hRightEq⟩ :=
    validatorReady_select_latentEntry_sourceArm hReady hSelect hRightEntryartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleftEntry:SelectArmKey × SelectArmAdmissionArtifactrightEntry:SelectArmKey × SelectArmAdmissionArtifacthLeftEntry:leftEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshRightEntry:rightEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:leftEntry.1 ≠ rightEntry.1node:NodeIdhNode:node ∈ leftEntry.2.bodyNodesleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armshLeftEq:leftEntry = (leftArm.canonicalSelectArmKey, leftArm)rightArm:SelectArmAdmissionArtifacthRightArm:rightArm ∈ selectAdmission.armshRightEq:rightEntry = (rightArm.canonicalSelectArmKey, rightArm)⊢ node ∉ rightEntry.2.bodyNodes
  cases hLeftEqreflartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsrightEntry:SelectArmKey × SelectArmAdmissionArtifacthRightEntry:rightEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entriesnode:NodeIdleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armsrightArm:SelectArmAdmissionArtifacthRightArm:rightArm ∈ selectAdmission.armshRightEq:rightEntry = (rightArm.canonicalSelectArmKey, rightArm)hLeftEntry:(leftArm.canonicalSelectArmKey, leftArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:(leftArm.canonicalSelectArmKey, leftArm).1 ≠ rightEntry.1hNode:node ∈ (leftArm.canonicalSelectArmKey, leftArm).2.bodyNodes⊢ node ∉ rightEntry.2.bodyNodes
  cases hRightEqrefl.reflartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsnode:NodeIdleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armsrightArm:SelectArmAdmissionArtifacthRightArm:rightArm ∈ selectAdmission.armshLeftEntry:(leftArm.canonicalSelectArmKey, leftArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshNode:node ∈ (leftArm.canonicalSelectArmKey, leftArm).2.bodyNodeshRightEntry:(rightArm.canonicalSelectArmKey, rightArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:(leftArm.canonicalSelectArmKey, leftArm).1 ≠ (rightArm.canonicalSelectArmKey, rightArm).1⊢ node ∉ (rightArm.canonicalSelectArmKey, rightArm).2.bodyNodes
  have hCanonicalKeys : leftArm.canonicalKey ≠ rightArm.canonicalKey := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsleftEntry:SelectArmKey × SelectArmAdmissionArtifactrightEntry:SelectArmKey × SelectArmAdmissionArtifacthLeftEntry:leftEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshRightEntry:rightEntry ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:leftEntry.1 ≠ rightEntry.1node:NodeIdhNode:node ∈ leftEntry.2.bodyNodes⊢ node ∉ rightEntry.2.bodyNodes
    intro hCanonicalEqartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsnode:NodeIdleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armsrightArm:SelectArmAdmissionArtifacthRightArm:rightArm ∈ selectAdmission.armshLeftEntry:(leftArm.canonicalSelectArmKey, leftArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshNode:node ∈ (leftArm.canonicalSelectArmKey, leftArm).2.bodyNodeshRightEntry:(rightArm.canonicalSelectArmKey, rightArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:(leftArm.canonicalSelectArmKey, leftArm).1 ≠ (rightArm.canonicalSelectArmKey, rightArm).1hCanonicalEq:leftArm.canonicalKey = rightArm.canonicalKey⊢ False
    apply hKeysartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsnode:NodeIdleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armsrightArm:SelectArmAdmissionArtifacthRightArm:rightArm ∈ selectAdmission.armshLeftEntry:(leftArm.canonicalSelectArmKey, leftArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshNode:node ∈ (leftArm.canonicalSelectArmKey, leftArm).2.bodyNodeshRightEntry:(rightArm.canonicalSelectArmKey, rightArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:(leftArm.canonicalSelectArmKey, leftArm).1 ≠ (rightArm.canonicalSelectArmKey, rightArm).1hCanonicalEq:leftArm.canonicalKey = rightArm.canonicalKey⊢ (leftArm.canonicalSelectArmKey, leftArm).1 = (rightArm.canonicalSelectArmKey, rightArm).1
    unfold SelectArmAdmissionArtifact.canonicalSelectArmKey selectArmKeyOfFieldLabelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsnode:NodeIdleftArm:SelectArmAdmissionArtifacthLeftArm:leftArm ∈ selectAdmission.armsrightArm:SelectArmAdmissionArtifacthRightArm:rightArm ∈ selectAdmission.armshLeftEntry:(leftArm.canonicalSelectArmKey, leftArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshNode:node ∈ (leftArm.canonicalSelectArmKey, leftArm).2.bodyNodeshRightEntry:(rightArm.canonicalSelectArmKey, rightArm) ∈ (selectAdmission.toLatentSelectAdmission ⋯).entrieshKeys:(leftArm.canonicalSelectArmKey, leftArm).1 ≠ (rightArm.canonicalSelectArmKey, rightArm).1hCanonicalEq:leftArm.canonicalKey = rightArm.canonicalKey⊢ ({ name := leftArm.canonicalKey.name }, leftArm).1 = ({ name := rightArm.canonicalKey.name }, rightArm).1
    rw [hCanonicalEq]All goals completed! 🐙
  exact
    validatorReady_select_armBodyNodesDisjoint
      hReady hSelect hLeftArm hRightArm hCanonicalKeys hNodeAll goals completed! 🐙

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire