Cortex.Wire.AdmissionArtifact.ReadyPhantom

proofs

On this page

Overview

Imports

import Cortex.Wire.AdmissionArtifact.ReadyPrimitive

Overview

Validator-ready phantom adapter accessors.

This page exposes product, boundary, bulk-replay, indexed-product, and record-product consequences for phantom adapter rows in a validator-ready artifact.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Validator readiness exposes phantom-adapter row validity.

theorem validatorReady_phantomAdapter_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.Valid :=
  hReady.phantomAdaptersValid phantom hPhantom

Validator readiness exposes phantom-adapter domain closure.

theorem validatorReady_phantomAdapter_domainClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    PhantomAdapterArtifact.DomainClosed artifact.nodes phantom :=
  hReady.componentDomainsClosed.phantomAdaptersClosed phantom hPhantom

Validator-ready phantom adapter nodes belong to the top-level node summary.

theorem validatorReady_phantomAdapter_nodeClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.node ∈ artifact.nodes :=
  (validatorReady_phantomAdapter_domainClosed hReady hPhantom).nodeClosed

Validator-ready phantom singular endpoints belong to the top-level node summary.

theorem validatorReady_phantomAdapter_singularNodeClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.singular.node ∈ artifact.nodes :=
  (validatorReady_phantomAdapter_domainClosed hReady hPhantom).singularNodeClosed

Validator-ready phantom multi-side endpoints are closed over the node summary.

theorem validatorReady_phantomAdapter_multiBoundaryClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    AdmissionBoundaryPort.ClosedOver artifact.nodes boundary :=
  (validatorReady_phantomAdapter_domainClosed hReady hPhantom).multiClosed
    boundary hBoundary

Validator-ready phantom left-bulk rows are closed over the node summary.

theorem validatorReady_phantomAdapter_leftBulk_closed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    AdmissionBoundaryPort.ClosedOver artifact.nodes pair.fromPort ∧
      AdmissionBoundaryPort.ClosedOver artifact.nodes pair.toPort :=
  (validatorReady_phantomAdapter_domainClosed hReady hPhantom).leftBulkClosed
    pair hPair

Validator-ready phantom right-bulk rows are closed over the node summary.

theorem validatorReady_phantomAdapter_rightBulk_closed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    AdmissionBoundaryPort.ClosedOver artifact.nodes pair.fromPort ∧
      AdmissionBoundaryPort.ClosedOver artifact.nodes pair.toPort :=
  (validatorReady_phantomAdapter_domainClosed hReady hPhantom).rightBulkClosed
    pair hPair

Validator-ready phantom adapter nodes appear in the component-role ledger.

theorem validatorReady_phantomAdapter_node_mem_componentRoleNodes
    {artifact : WireAdmissionArtifact}
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.node ∈ artifact.componentRoleNodes := byartifact:WireAdmissionArtifactphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ phantom.node ∈ artifact.componentRoleNodes
  simp [componentRoleNodes]artifact:WireAdmissionArtifactphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ phantom.node ∈ artifact.generatedUsedChildNodes ∨
  (∃ a ∈ artifact.phantomAdapters, a.node = phantom.node) ∨ ∃ a ∈ artifact.selects, a.conditionNode = phantom.node
  exact Or.inr (Or.inl ⟨phantom, hPhantom, rfl⟩)All goals completed! 🐙

Validator-ready phantom adapter nodes appear in the phantom-role ledger.

theorem validatorReady_phantomAdapter_node_mem_phantomAdapterNodes
    {artifact : WireAdmissionArtifact}
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.node ∈ artifact.phantomAdapters.map PhantomAdapterArtifact.node :=
  List.mem_map.mpr ⟨phantom, hPhantom, rfl⟩

Validator-ready phantom-adapter rows expose product arity matching.

theorem validatorReady_phantomAdapter_productArityMatches
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.ProductArityMatches :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).productArityMatches

Validator-ready phantom-adapter rows expose product-shape/multi-frontier matching.

theorem validatorReady_phantomAdapter_productShapeMatchesMulti
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.ProductShapeMatchesMulti :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).productShapeMatchesMulti

Validator-ready phantom-adapter rows expose singular/product contract matching.

theorem validatorReady_phantomAdapter_productContractMatchesSingular
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.ProductContractMatchesSingular :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).productContractMatchesSingular

Validator-ready phantom-adapter rows expose product-shape validity.

theorem validatorReady_phantomAdapter_productShape_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.productShape.Valid :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).productShapeValid

Validator-ready phantom-adapter rows expose validity of the aggregate product contract.

theorem validatorReady_phantomAdapter_product_contractValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.productShape.contract.Valid :=
  ProductShapeArtifact.valid_contractValid
    (validatorReady_phantomAdapter_productShape_valid hReady hPhantom)

Validator-ready phantom-adapter rows expose multi-side endpoint uniqueness.

theorem validatorReady_phantomAdapter_multiEndpointKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.MultiEndpointKeysUnique :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).multiEndpointKeysUnique

Validator-ready phantom-adapter rows expose direction-aware bulk endpoint matching.

theorem validatorReady_phantomAdapter_bulkEndpointsMatch
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.BulkEndpointsMatch :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).bulkEndpointsMatch

Validator-ready phantom-adapter rows expose exact bulk endpoint partitioning.

theorem validatorReady_phantomAdapter_bulkEndpointPartition
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.BulkEndpointPartition :=
  (validatorReady_phantomAdapter_valid hReady hPhantom).bulkEndpointPartition

Validator-ready phantom-adapter rows expose indexed multi-side compatibility-key uniqueness.

theorem validatorReady_phantomAdapter_indexedMultiCompatibilityKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.IndexedMultiCompatibilityKeysUnique :=
  (validatorReady_phantomAdapter_valid
    hReady hPhantom).indexedMultiCompatibilityKeysUnique

Validator-ready gather artifacts expose the left-bulk multi-to-phantom endpoint shape.

theorem validatorReady_phantomAdapter_gather_leftBulkEndpoints
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulk⊢ pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node
  have hMatch := validatorReady_phantomAdapter_bulkEndpointsMatch hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhMatch:phantom.BulkEndpointsMatch⊢ pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node
  unfold PhantomAdapterArtifact.BulkEndpointsMatch at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhMatch:match phantom.direction with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node
  rw [hDirection] at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhMatch:match PhantomAdapterDirection.gather with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node
  exact hMatch.left pair hPairAll goals completed! 🐙

Validator-ready gather artifacts expose the right-bulk phantom-to-singular endpoint shape.

theorem validatorReady_phantomAdapter_gather_rightBulkEndpoints
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulk⊢ pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
  have hMatch := validatorReady_phantomAdapter_bulkEndpointsMatch hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhMatch:phantom.BulkEndpointsMatch⊢ pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
  unfold PhantomAdapterArtifact.BulkEndpointsMatch at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhMatch:match phantom.direction with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
  rw [hDirection] at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhMatch:match PhantomAdapterDirection.gather with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
  exact hMatch.right pair hPairAll goals completed! 🐙

Validator-ready scatter artifacts expose the left-bulk singular-to-phantom endpoint shape.

theorem validatorReady_phantomAdapter_scatter_leftBulkEndpoints
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulk⊢ pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node
  have hMatch := validatorReady_phantomAdapter_bulkEndpointsMatch hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhMatch:phantom.BulkEndpointsMatch⊢ pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node
  unfold PhantomAdapterArtifact.BulkEndpointsMatch at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhMatch:match phantom.direction with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node
  rw [hDirection] at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhMatch:match PhantomAdapterDirection.scatter with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node
  exact hMatch.left pair hPairAll goals completed! 🐙

Validator-ready scatter artifacts expose the right-bulk phantom-to-multi endpoint shape.

theorem validatorReady_phantomAdapter_scatter_rightBulkEndpoints
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulk⊢ pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi
  have hMatch := validatorReady_phantomAdapter_bulkEndpointsMatch hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhMatch:phantom.BulkEndpointsMatch⊢ pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi
  unfold PhantomAdapterArtifact.BulkEndpointsMatch at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhMatch:match phantom.direction with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi
  rw [hDirection] at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhMatch:match PhantomAdapterDirection.scatter with
| PhantomAdapterDirection.gather =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort ∈ phantom.multi ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort = phantom.singular
| PhantomAdapterDirection.scatter =>
  (∀ pair ∈ phantom.leftBulk, pair.fromPort = phantom.singular ∧ pair.toPort.node = phantom.node) ∧
    ∀ pair ∈ phantom.rightBulk, pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi⊢ pair.fromPort.node = phantom.node ∧ pair.toPort ∈ phantom.multi
  exact hMatch.right pair hPairAll goals completed! 🐙

Validator-ready gather artifacts expose exact left-bulk coverage of multi-side keys.

theorem validatorReady_phantomAdapter_gather_leftBulkSourceKeys_perm_multi
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather) :
    phantom.leftBulkSourceKeys.Perm
      (phantom.multi.map AdmissionBoundaryPort.key) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gather⊢ phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  have hPartition := validatorReady_phantomAdapter_bulkEndpointPartition hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPartition:phantom.BulkEndpointPartition⊢ phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPartition:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  rw [hDirection] at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPartition:match PhantomAdapterDirection.gather with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  exact hPartition.leftAll goals completed! 🐙

Validator-ready gather artifacts expose exact right-bulk coverage of the singular key.

theorem validatorReady_phantomAdapter_gather_rightBulkTargetKeys_perm_singular
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather) :
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key] := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gather⊢ phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
  have hPartition := validatorReady_phantomAdapter_bulkEndpointPartition hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPartition:phantom.BulkEndpointPartition⊢ phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
  unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPartition:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
  rw [hDirection] at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPartition:match PhantomAdapterDirection.gather with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
  exact hPartition.rightAll goals completed! 🐙

Validator-ready scatter artifacts expose exact left-bulk coverage of the singular key.

theorem validatorReady_phantomAdapter_scatter_leftBulkSourceKeys_perm_singular
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter) :
    phantom.leftBulkSourceKeys.Perm [phantom.singular.key] := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ phantom.leftBulkSourceKeys.Perm [phantom.singular.key]
  have hPartition := validatorReady_phantomAdapter_bulkEndpointPartition hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPartition:phantom.BulkEndpointPartition⊢ phantom.leftBulkSourceKeys.Perm [phantom.singular.key]
  unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPartition:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.leftBulkSourceKeys.Perm [phantom.singular.key]
  rw [hDirection] at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPartition:match PhantomAdapterDirection.scatter with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.leftBulkSourceKeys.Perm [phantom.singular.key]
  exact hPartition.leftAll goals completed! 🐙

Validator-ready scatter artifacts expose exact right-bulk coverage of multi-side keys.

theorem validatorReady_phantomAdapter_scatter_rightBulkTargetKeys_perm_multi
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter) :
    phantom.rightBulkTargetKeys.Perm
      (phantom.multi.map AdmissionBoundaryPort.key) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  have hPartition := validatorReady_phantomAdapter_bulkEndpointPartition hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPartition:phantom.BulkEndpointPartition⊢ phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPartition:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  rw [hDirection] at hPartitionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPartition:match PhantomAdapterDirection.scatter with
| PhantomAdapterDirection.gather =>
  phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi) ∧
    phantom.rightBulkTargetKeys.Perm [phantom.singular.key]
| PhantomAdapterDirection.scatter =>
  phantom.leftBulkSourceKeys.Perm [phantom.singular.key] ∧
    phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)
  exact hPartition.rightAll goals completed! 🐙

Validator-ready phantom-adapter rows expose structural row validity.

theorem validatorReady_phantomAdapter_rowsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.RowsValid :=
  (validatorReady_phantomAdapter_valid
    hReady hPhantom).rowsValid

Validator-ready phantom adapter nodes carry valid node identifiers.

theorem validatorReady_phantomAdapter_nodeValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.node.Valid :=
  (validatorReady_phantomAdapter_rowsValid hReady hPhantom).nodeValid

Validator-ready phantom singular endpoints are structurally valid.

theorem validatorReady_phantomAdapter_singularValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.singular.Valid :=
  (validatorReady_phantomAdapter_rowsValid hReady hPhantom).singularValid

Validator-ready phantom multi-side endpoints are structurally valid.

theorem validatorReady_phantomAdapter_multiBoundaryValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    boundary.Valid :=
  (validatorReady_phantomAdapter_rowsValid hReady hPhantom).multiValid
    boundary hBoundary

Validator-ready phantom left-bulk rows are structurally valid.

theorem validatorReady_phantomAdapter_leftBulk_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.Valid :=
  (validatorReady_phantomAdapter_rowsValid hReady hPhantom).leftBulkValid
    pair hPair

Validator-ready phantom right-bulk rows are structurally valid.

theorem validatorReady_phantomAdapter_rightBulk_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.Valid :=
  (validatorReady_phantomAdapter_rowsValid hReady hPhantom).rightBulkValid
    pair hPair

Validator-ready phantom-adapter rows expose compatibility for each left bulk row.

theorem validatorReady_phantomAdapter_leftBulk_boundaryCompatible
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.BoundaryCompatible :=
  let hRows := validatorReady_phantomAdapter_rowsValid hReady hPhantom
  connectionsValid_boundaryCompatible hRows.leftBulkValid hPair

Validator-ready phantom-adapter rows expose compatibility for each right bulk row.

theorem validatorReady_phantomAdapter_rightBulk_boundaryCompatible
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.BoundaryCompatible :=
  let hRows := validatorReady_phantomAdapter_rowsValid hReady hPhantom
  connectionsValid_boundaryCompatible hRows.rightBulkValid hPair

Validator-ready phantom left-bulk rows are replayed by primitive connect rows.

theorem validatorReady_phantomAdapter_leftBulk_replayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps :=
  (validatorReady_phantomBridgeBulkConnectionsReplayed
    hReady phantom hPhantom).left pair hPair

Validator-ready phantom right-bulk rows are replayed by primitive connect rows.

theorem validatorReady_phantomAdapter_rightBulk_replayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps :=
  (validatorReady_phantomBridgeBulkConnectionsReplayed
    hReady phantom hPhantom).right pair hPair

Validator-ready phantom left-bulk source exits are consumed by primitive replay.

theorem validatorReady_phantomAdapter_leftBulk_sourceConsumed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.fromKey ∈
      PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps :=
  PrimitiveGraphStep.matchedConnectionsList_fromKey_mem_consumedExitKeysList
    (validatorReady_phantomAdapter_leftBulk_replayed hReady hPhantom hPair)

Validator-ready phantom left-bulk target entries are consumed by primitive replay.

theorem validatorReady_phantomAdapter_leftBulk_targetConsumed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.toKey ∈
      PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps :=
  PrimitiveGraphStep.matchedConnectionsList_toKey_mem_consumedEntryKeysList
    (validatorReady_phantomAdapter_leftBulk_replayed hReady hPhantom hPair)

Validator-ready phantom right-bulk source exits are consumed by primitive replay.

theorem validatorReady_phantomAdapter_rightBulk_sourceConsumed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.fromKey ∈
      PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps :=
  PrimitiveGraphStep.matchedConnectionsList_fromKey_mem_consumedExitKeysList
    (validatorReady_phantomAdapter_rightBulk_replayed hReady hPhantom hPair)

Validator-ready phantom right-bulk target entries are consumed by primitive replay.

theorem validatorReady_phantomAdapter_rightBulk_targetConsumed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.toKey ∈
      PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps :=
  PrimitiveGraphStep.matchedConnectionsList_toKey_mem_consumedEntryKeysList
    (validatorReady_phantomAdapter_rightBulk_replayed hReady hPhantom hPair)

Validator-ready gather adapters consume every multi-side endpoint through a replayed row.

theorem validatorReady_phantomAdapter_gather_multiEndpoint_replayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    ∃ pair,
      pair ∈ phantom.leftBulk ∧
        pair.fromKey = boundary.key ∧
          pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hPerm :=
    validatorReady_phantomAdapter_gather_leftBulkSourceKeys_perm_multi
      hReady hPhantom hDirectionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihPerm:phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hKeyMem :
      boundary.key ∈ phantom.leftBulkSourceKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
    exact hPerm.mem_iff.mpr (List.mem_map.mpr ⟨boundary, hBoundary, rfl⟩)All goals completed! 🐙
  unfold PhantomAdapterArtifact.leftBulkSourceKeys at hKeyMemartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihPerm:phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)hKeyMem:boundary.key ∈ List.map AdmissionConnection.fromKey phantom.leftBulk⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rcases List.mem_map.mp hKeyMem with ⟨pair, hPair, hKey⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihPerm:phantom.leftBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)hKeyMem:boundary.key ∈ List.map AdmissionConnection.fromKey phantom.leftBulkpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhKey:pair.fromKey = boundary.key⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  exact
    ⟨ pair
    , hPair
    , hKey
    , validatorReady_phantomAdapter_leftBulk_replayed hReady hPhantom hPair
    ⟩All goals completed! 🐙

Validator-ready gather adapters consume the singular endpoint through a replayed row.

theorem validatorReady_phantomAdapter_gather_singularEndpoint_replayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather) :
    ∃ pair,
      pair ∈ phantom.rightBulk ∧
        pair.toKey = phantom.singular.key ∧
          pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gather⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hPerm :=
    validatorReady_phantomAdapter_gather_rightBulkTargetKeys_perm_singular
      hReady hPhantom hDirectionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPerm:phantom.rightBulkTargetKeys.Perm [phantom.singular.key]⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hKeyMem :
      phantom.singular.key ∈ phantom.rightBulkTargetKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gather⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
    exact hPerm.mem_iff.mpr (byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPerm:phantom.rightBulkTargetKeys.Perm [phantom.singular.key]⊢ phantom.singular.key ∈ [phantom.singular.key] simpAll goals completed! 🐙)
  unfold PhantomAdapterArtifact.rightBulkTargetKeys at hKeyMemartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPerm:phantom.rightBulkTargetKeys.Perm [phantom.singular.key]hKeyMem:phantom.singular.key ∈ List.map AdmissionConnection.toKey phantom.rightBulk⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rcases List.mem_map.mp hKeyMem with ⟨pair, hPair, hKey⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhPerm:phantom.rightBulkTargetKeys.Perm [phantom.singular.key]hKeyMem:phantom.singular.key ∈ List.map AdmissionConnection.toKey phantom.rightBulkpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhKey:pair.toKey = phantom.singular.key⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  exact
    ⟨ pair
    , hPair
    , hKey
    , validatorReady_phantomAdapter_rightBulk_replayed hReady hPhantom hPair
    ⟩All goals completed! 🐙

Validator-ready scatter adapters consume the singular endpoint through a replayed row.

theorem validatorReady_phantomAdapter_scatter_singularEndpoint_replayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter) :
    ∃ pair,
      pair ∈ phantom.leftBulk ∧
        pair.fromKey = phantom.singular.key ∧
          pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hPerm :=
    validatorReady_phantomAdapter_scatter_leftBulkSourceKeys_perm_singular
      hReady hPhantom hDirectionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPerm:phantom.leftBulkSourceKeys.Perm [phantom.singular.key]⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hKeyMem :
      phantom.singular.key ∈ phantom.leftBulkSourceKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
    exact hPerm.mem_iff.mpr (byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPerm:phantom.leftBulkSourceKeys.Perm [phantom.singular.key]⊢ phantom.singular.key ∈ [phantom.singular.key] simpAll goals completed! 🐙)
  unfold PhantomAdapterArtifact.leftBulkSourceKeys at hKeyMemartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPerm:phantom.leftBulkSourceKeys.Perm [phantom.singular.key]hKeyMem:phantom.singular.key ∈ List.map AdmissionConnection.fromKey phantom.leftBulk⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rcases List.mem_map.mp hKeyMem with ⟨pair, hPair, hKey⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhPerm:phantom.leftBulkSourceKeys.Perm [phantom.singular.key]hKeyMem:phantom.singular.key ∈ List.map AdmissionConnection.fromKey phantom.leftBulkpair:AdmissionConnectionhPair:pair ∈ phantom.leftBulkhKey:pair.fromKey = phantom.singular.key⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  exact
    ⟨ pair
    , hPair
    , hKey
    , validatorReady_phantomAdapter_leftBulk_replayed hReady hPhantom hPair
    ⟩All goals completed! 🐙

Validator-ready scatter adapters consume every multi-side endpoint through a replayed row.

theorem validatorReady_phantomAdapter_scatter_multiEndpoint_replayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    ∃ pair,
      pair ∈ phantom.rightBulk ∧
        pair.toKey = boundary.key ∧
          pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hPerm :=
    validatorReady_phantomAdapter_scatter_rightBulkTargetKeys_perm_multi
      hReady hPhantom hDirectionartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihPerm:phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hKeyMem :
      boundary.key ∈ phantom.rightBulkTargetKeys := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
    exact hPerm.mem_iff.mpr (List.mem_map.mpr ⟨boundary, hBoundary, rfl⟩)All goals completed! 🐙
  unfold PhantomAdapterArtifact.rightBulkTargetKeys at hKeyMemartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihPerm:phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)hKeyMem:boundary.key ∈ List.map AdmissionConnection.toKey phantom.rightBulk⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rcases List.mem_map.mp hKeyMem with ⟨pair, hPair, hKey⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihPerm:phantom.rightBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key phantom.multi)hKeyMem:boundary.key ∈ List.map AdmissionConnection.toKey phantom.rightBulkpair:AdmissionConnectionhPair:pair ∈ phantom.rightBulkhKey:pair.toKey = boundary.key⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = boundary.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  exact
    ⟨ pair
    , hPair
    , hKey
    , validatorReady_phantomAdapter_rightBulk_replayed hReady hPhantom hPair
    ⟩All goals completed! 🐙

Validator-ready indexed phantom artifacts expose the serialized product count.

theorem validatorReady_phantomAdapter_indexed_multi_length_eq
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {element : ContractId}
    {count : Nat}
    (hShape : phantom.productShape = ProductShapeArtifact.indexed element count) :
    phantom.multi.length = count := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element count⊢ phantom.multi.length = count
  have hArity := validatorReady_phantomAdapter_productArityMatches hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthArity:phantom.ProductArityMatches⊢ phantom.multi.length = count
  unfold PhantomAdapterArtifact.ProductArityMatches at hArityartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthArity:phantom.multi.length = phantom.productShape.arity⊢ phantom.multi.length = count
  rw [hShape] at hArityartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthArity:phantom.multi.length = (ProductShapeArtifact.indexed element count).arity⊢ phantom.multi.length = count
  simpa [ProductShapeArtifact.arity] using hArityAll goals completed! 🐙

Validator-ready indexed phantom artifacts expose uniform multi-side element contracts.

theorem validatorReady_phantomAdapter_indexed_multi_contract_eq
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {element : ContractId}
    {count : Nat}
    (hShape : phantom.productShape = ProductShapeArtifact.indexed element count)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    boundary.contract = element := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element countboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ boundary.contract = element
  have hMatch := validatorReady_phantomAdapter_productShapeMatchesMulti hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element countboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihMatch:phantom.ProductShapeMatchesMulti⊢ boundary.contract = element
  unfold PhantomAdapterArtifact.ProductShapeMatchesMulti at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element countboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihMatch:phantom.productShape.BoundariesMatch phantom.multi⊢ boundary.contract = element
  rw [hShape] at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element countboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihMatch:(ProductShapeArtifact.indexed element count).BoundariesMatch phantom.multi⊢ boundary.contract = element
  exact hMatch boundary hBoundaryAll goals completed! 🐙

Validator-ready indexed phantom artifacts expose valid element contracts.

theorem validatorReady_phantomAdapter_indexed_elementValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {element : ContractId}
    {count : Nat}
    (hShape : phantom.productShape = ProductShapeArtifact.indexed element count) :
    element.Valid := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element count⊢ element.Valid
  have hValid := validatorReady_phantomAdapter_productShape_valid hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthValid:phantom.productShape.Valid⊢ element.Valid
  rw [hShape] at hValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthValid:(ProductShapeArtifact.indexed element count).Valid⊢ element.Valid
  exact ProductShapeArtifact.valid_indexed_elementValid hValidAll goals completed! 🐙

Validator-ready indexed phantom artifacts reject nested indexed product elements.

theorem validatorReady_phantomAdapter_indexed_elementNominal
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {element : ContractId}
    {count : Nat}
    (hShape : phantom.productShape = ProductShapeArtifact.indexed element count) :
    element.name.startsWith "[" = false := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element count⊢ element.name.startsWith "[" = false
  have hValid := validatorReady_phantomAdapter_productShape_valid hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthValid:phantom.productShape.Valid⊢ element.name.startsWith "[" = false
  rw [hShape] at hValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthValid:(ProductShapeArtifact.indexed element count).Valid⊢ element.name.startsWith "[" = false
  exact ProductShapeArtifact.valid_indexed_elementNominal hValidAll goals completed! 🐙

Validator-ready indexed phantom artifacts expose duplicate-free multi compatibility keys.

theorem validatorReady_phantomAdapter_indexed_multiCompatibilityShapesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {element : ContractId}
    {count : Nat}
    (hShape : phantom.productShape = ProductShapeArtifact.indexed element count) :
    (phantom.multi.map AdmissionBoundaryPort.compatibilityShape).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element count⊢ (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup
  have hUnique :=
    validatorReady_phantomAdapter_indexedMultiCompatibilityKeysUnique hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthUnique:phantom.IndexedMultiCompatibilityKeysUnique⊢ (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup
  unfold PhantomAdapterArtifact.IndexedMultiCompatibilityKeysUnique at hUniqueartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthUnique:match phantom.productShape with
| ProductShapeArtifact.record contract fields => True
| ProductShapeArtifact.indexed elementContract count =>
  (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup⊢ (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup
  rw [hShape] at hUniqueartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthUnique:match ProductShapeArtifact.indexed element count with
| ProductShapeArtifact.record contract fields => True
| ProductShapeArtifact.indexed elementContract count =>
  (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup⊢ (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup
  exact hUniqueAll goals completed! 🐙

Validator-ready phantom artifacts expose the singular endpoint's aggregate product contract.

theorem validatorReady_phantomAdapter_singular_contract_eq_product
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.singular.contract = phantom.productShape.contract :=
  validatorReady_phantomAdapter_productContractMatchesSingular hReady hPhantom

Validator-ready indexed phantom artifacts expose the singular [T; N] contract.

theorem validatorReady_phantomAdapter_indexed_singular_contract_eq
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {element : ContractId}
    {count : Nat}
    (hShape : phantom.productShape = ProductShapeArtifact.indexed element count) :
    phantom.singular.contract = ContractId.boundedIndexed element count := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element count⊢ phantom.singular.contract = element.boundedIndexed count
  have hContract :=
    validatorReady_phantomAdapter_singular_contract_eq_product hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthContract:phantom.singular.contract = phantom.productShape.contract⊢ phantom.singular.contract = element.boundedIndexed count
  rw [hShape] at hContractartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterselement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthContract:phantom.singular.contract = (ProductShapeArtifact.indexed element count).contract⊢ phantom.singular.contract = element.boundedIndexed count
  simpa [ProductShapeArtifact.contract] using hContractAll goals completed! 🐙

Validator-ready record phantom artifacts expose duplicate-free record field labels.

theorem validatorReady_phantomAdapter_record_fieldsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields) :
    (fields.map Prod.fst).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ (List.map Prod.fst fields).Nodup
  have hValid := validatorReady_phantomAdapter_productShape_valid hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshValid:phantom.productShape.Valid⊢ (List.map Prod.fst fields).Nodup
  rw [hShape] at hValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshValid:(ProductShapeArtifact.record contract fields).Valid⊢ (List.map Prod.fst fields).Nodup
  exact ProductShapeArtifact.valid_record_fieldsUnique hValidAll goals completed! 🐙

Validator-ready record phantom artifacts expose validity of the aggregate contract row.

theorem validatorReady_phantomAdapter_record_contractValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields) :
    contract.Valid := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ contract.Valid
  have hValid := validatorReady_phantomAdapter_productShape_valid hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshValid:phantom.productShape.Valid⊢ contract.Valid
  rw [hShape] at hValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshValid:(ProductShapeArtifact.record contract fields).Valid⊢ contract.Valid
  exact ProductShapeArtifact.valid_record_contractValid hValidAll goals completed! 🐙

Validator-ready record phantom artifacts expose the singular aggregate record contract.

theorem validatorReady_phantomAdapter_record_singular_contract_eq
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields) :
    phantom.singular.contract = contract := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ phantom.singular.contract = contract
  have hContract :=
    validatorReady_phantomAdapter_singular_contract_eq_product hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshContract:phantom.singular.contract = phantom.productShape.contract⊢ phantom.singular.contract = contract
  rw [hShape] at hContractartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshContract:phantom.singular.contract = (ProductShapeArtifact.record contract fields).contract⊢ phantom.singular.contract = contract
  simpa [ProductShapeArtifact.contract] using hContractAll goals completed! 🐙

Validator-ready record phantom artifacts expose validity of every field row.

theorem validatorReady_phantomAdapter_record_fieldValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields)
    {field : FieldLabel × ContractId}
    (hField : field ∈ fields) :
    field.fst.Valid ∧ field.snd.Valid := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsfield:FieldLabel × ContractIdhField:field ∈ fields⊢ field.1.Valid ∧ field.2.Valid
  have hValid := validatorReady_phantomAdapter_productShape_valid hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsfield:FieldLabel × ContractIdhField:field ∈ fieldshValid:phantom.productShape.Valid⊢ field.1.Valid ∧ field.2.Valid
  rw [hShape] at hValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsfield:FieldLabel × ContractIdhField:field ∈ fieldshValid:(ProductShapeArtifact.record contract fields).Valid⊢ field.1.Valid ∧ field.2.Valid
  exact ProductShapeArtifact.valid_record_fieldValid hValid hFieldAll goals completed! 🐙

Validator-ready record phantom artifacts expose serialized record arity.

theorem validatorReady_phantomAdapter_record_multi_length_eq
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields) :
    phantom.multi.length = fields.length := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ phantom.multi.length = fields.length
  have hArity := validatorReady_phantomAdapter_productArityMatches hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshArity:phantom.ProductArityMatches⊢ phantom.multi.length = fields.length
  unfold PhantomAdapterArtifact.ProductArityMatches at hArityartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshArity:phantom.multi.length = phantom.productShape.arity⊢ phantom.multi.length = fields.length
  rw [hShape] at hArityartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshArity:phantom.multi.length = (ProductShapeArtifact.record contract fields).arity⊢ phantom.multi.length = fields.length
  simpa [ProductShapeArtifact.arity] using hArityAll goals completed! 🐙

Validator-ready record phantom artifacts expose the multi-side record-field projection.

theorem validatorReady_phantomAdapter_record_multi_fields_perm
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields) :
    (phantom.multi.filterMap AdmissionBoundaryPort.recordField).Perm fields := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ (List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fields
  have hMatch := validatorReady_phantomAdapter_productShapeMatchesMulti hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshMatch:phantom.ProductShapeMatchesMulti⊢ (List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fields
  unfold PhantomAdapterArtifact.ProductShapeMatchesMulti at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshMatch:phantom.productShape.BoundariesMatch phantom.multi⊢ (List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fields
  rw [hShape] at hMatchartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshMatch:(ProductShapeArtifact.record contract fields).BoundariesMatch phantom.multi⊢ (List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fields
  simpa [ProductShapeArtifact.BoundariesMatch] using hMatchAll goals completed! 🐙

Validator-ready record phantom artifacts expose duplicate-free projected multi labels.

theorem validatorReady_phantomAdapter_record_multi_fieldLabelsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields) :
    ((phantom.multi.filterMap AdmissionBoundaryPort.recordField).map Prod.fst).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ (List.map Prod.fst (List.filterMap AdmissionBoundaryPort.recordField phantom.multi)).Nodup
  have hFieldsUnique :=
    validatorReady_phantomAdapter_record_fieldsUnique hReady hPhantom hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshFieldsUnique:(List.map Prod.fst fields).Nodup⊢ (List.map Prod.fst (List.filterMap AdmissionBoundaryPort.recordField phantom.multi)).Nodup
  have hPerm :=
    validatorReady_phantomAdapter_record_multi_fields_perm hReady hPhantom hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshFieldsUnique:(List.map Prod.fst fields).NoduphPerm:(List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fields⊢ (List.map Prod.fst (List.filterMap AdmissionBoundaryPort.recordField phantom.multi)).Nodup
  exact (hPerm.map Prod.fst).nodup_iff.mpr hFieldsUniqueAll goals completed! 🐙

Validator-ready record phantom artifacts expose a field row for every multi endpoint.

theorem validatorReady_phantomAdapter_record_multi_boundary_field_mem
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    ∃ field,
      boundary.recordField = some field ∧ field ∈ fields := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ field, boundary.recordField = some field ∧ field ∈ fields
  have hLength :=
    validatorReady_phantomAdapter_record_multi_length_eq hReady hPhantom hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihLength:phantom.multi.length = fields.length⊢ ∃ field, boundary.recordField = some field ∧ field ∈ fields
  have hPerm :=
    validatorReady_phantomAdapter_record_multi_fields_perm hReady hPhantom hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihLength:phantom.multi.length = fields.lengthhPerm:(List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fields⊢ ∃ field, boundary.recordField = some field ∧ field ∈ fields
  have hProjectedLength :
      (phantom.multi.filterMap AdmissionBoundaryPort.recordField).length =
        phantom.multi.length := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ field, boundary.recordField = some field ∧ field ∈ fields
    rw [hPerm.length_eq, hLength]All goals completed! 🐙
  obtain ⟨field, hField⟩ :=
    exists_some_of_filterMap_length_eq hProjectedLength hBoundaryartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihLength:phantom.multi.length = fields.lengthhPerm:(List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fieldshProjectedLength:(List.filterMap AdmissionBoundaryPort.recordField phantom.multi).length = phantom.multi.lengthfield:FieldLabel × ContractIdhField:boundary.recordField = some field⊢ ∃ field, boundary.recordField = some field ∧ field ∈ fields
  have hProjected :
      field ∈ phantom.multi.filterMap AdmissionBoundaryPort.recordField :=
    List.mem_filterMap.mpr ⟨boundary, hBoundary, hField⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multihLength:phantom.multi.length = fields.lengthhPerm:(List.filterMap AdmissionBoundaryPort.recordField phantom.multi).Perm fieldshProjectedLength:(List.filterMap AdmissionBoundaryPort.recordField phantom.multi).length = phantom.multi.lengthfield:FieldLabel × ContractIdhField:boundary.recordField = some fieldhProjected:field ∈ List.filterMap AdmissionBoundaryPort.recordField phantom.multi⊢ ∃ field, boundary.recordField = some field ∧ field ∈ fields
  exact ⟨field, hField, hPerm.mem_iff.mp hProjected⟩All goals completed! 🐙

Validator-ready record phantom multi endpoints are labeled by declared record fields.

theorem validatorReady_phantomAdapter_record_multi_boundary_labeled
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {contract : ContractId}
    {fields : List (FieldLabel × ContractId)}
    (hShape : phantom.productShape = ProductShapeArtifact.record contract fields)
    {boundary : AdmissionBoundaryPort}
    (hBoundary : boundary ∈ phantom.multi) :
    ∃ label,
      boundary.label = AdmissionPortLabel.label label ∧
        (label, boundary.contract) ∈ fields := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multi⊢ ∃ label, boundary.label = AdmissionPortLabel.label label ∧ (label, boundary.contract) ∈ fields
  obtain ⟨field, hField, hFieldMem⟩ :=
    validatorReady_phantomAdapter_record_multi_boundary_field_mem
      hReady hPhantom hShape hBoundaryartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multifield:FieldLabel × ContractIdhField:boundary.recordField = some fieldhFieldMem:field ∈ fields⊢ ∃ label, boundary.label = AdmissionPortLabel.label label ∧ (label, boundary.contract) ∈ fields
  cases hLabel : boundary.label with
  | noLabel =>noLabelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multifield:FieldLabel × ContractIdhField:boundary.recordField = some fieldhFieldMem:field ∈ fieldshLabel:boundary.label = AdmissionPortLabel.noLabel⊢ ∃ label, AdmissionPortLabel.noLabel = AdmissionPortLabel.label label ∧ (label, boundary.contract) ∈ fields
      simp [AdmissionBoundaryPort.recordField, hLabel] at hFieldAll goals completed! 🐙
  | label label =>labelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multifield:FieldLabel × ContractIdhField:boundary.recordField = some fieldhFieldMem:field ∈ fieldslabel:FieldLabelhLabel:boundary.label = AdmissionPortLabel.label label⊢ ∃ label_1, AdmissionPortLabel.label label = AdmissionPortLabel.label label_1 ∧ (label_1, boundary.contract) ∈ fields
      simp [AdmissionBoundaryPort.recordField, hLabel] at hFieldlabelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multifield:FieldLabel × ContractIdhFieldMem:field ∈ fieldslabel:FieldLabelhLabel:boundary.label = AdmissionPortLabel.label labelhField:(label, boundary.contract) = field⊢ ∃ label_1, AdmissionPortLabel.label label = AdmissionPortLabel.label label_1 ∧ (label_1, boundary.contract) ∈ fields
      exact ⟨label, rfl, byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapterscontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldsboundary:AdmissionBoundaryPorthBoundary:boundary ∈ phantom.multifield:FieldLabel × ContractIdhFieldMem:field ∈ fieldslabel:FieldLabelhLabel:boundary.label = AdmissionPortLabel.label labelhField:(label, boundary.contract) = field⊢ (label, boundary.contract) ∈ fields simpa [hField] using hFieldMemAll goals completed! 🐙⟩

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire