Theory /Cortex /Wire /AdmissionArtifact /PhantomReconstruction

Cortex.Wire.AdmissionArtifact.PhantomReconstruction

proofs

On this page

Overview
Boundary-Row Source Instances
Phantom Reconstruction Contract
Reconstruction Theorems

Imports

import Cortex.Wire.AdmissionArtifact.PrimitiveReconstruction

Overview

Phantom-adapter reconstruction from validator-sound admission artifacts.

The phantom artifact rows record the generated adapter node, product shape, source-visible multi/singular endpoints, and the two primitive bulk ledgers emitted for *. They do not serialize the left and right operand graphs or the Lean BulkContract traces required by PhantomAdapterWitness.

This module therefore reconstructs the strongest honest artifact-boundary witness:

the generated phantom node is backed by a primitive node row;
that primitive row builds an open source-linear phantom-node object;
left/right phantom bulk ledgers are replayed by primitive matched connections;
record and bounded-indexed product-shape facts are available in case form;
source-visible multi/singular endpoints are covered by direction-specific replay facts; and
phantom-node frontier keys are accounted for by primitive replay.

The later full-graph reconstruction step must add the operand graphs and certified BulkContract traces before constructing PhantomAdapterWitness.

              namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace AdmissionBoundaryPort

Boundary-Row Source Instances

Direction-erased port signature projected from an artifact boundary row.

def sourcePortSignature (boundary : AdmissionBoundaryPort) : PortSignature :=
  { label := boundary.port
    contract := boundary.contract }

Output-direction source instance projected from an artifact boundary row.

def sourceOutputInstance
    (boundary : AdmissionBoundaryPort) :
    SourcePortInstance NodeId OutputPortSignature :=
  { node := boundary.node
    port := { signature := boundary.sourcePortSignature } }

Input-direction source instance projected from an artifact boundary row.

def sourceInputInstance
    (boundary : AdmissionBoundaryPort) :
    SourcePortInstance NodeId InputPortSignature :=
  { node := boundary.node
    port := { signature := boundary.sourcePortSignature } }

Open source-linear object for one primitive node row.

def openBoundaryNodeObject
    (node : NodeId)
    (entries exits : List AdmissionBoundaryPort)
    (hEntryNodes : ∀ entry, entry ∈ entries → entry.node = node)
    (hExitNodes : ∀ exit, exit ∈ exits → exit.node = node) :
    LinearPortGraph.LinearPortObject NodeId OutputPortSignature InputPortSignature :=
  LinearPortGraph.LinearPortObject.nodePorts
    ({node} : Finset NodeId)
    ((exits.map AdmissionBoundaryPort.sourceOutputInstance).toFinset)
    ((entries.map AdmissionBoundaryPort.sourceInputInstance).toFinset)
    (bynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = node⊢ ∀ output ∈ (List.map sourceOutputInstance exits).toFinset, output.node ∈ {node}
      intro output hOutputnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeoutput:SourcePortInstance NodeId OutputPortSignaturehOutput:output ∈ (List.map sourceOutputInstance exits).toFinset⊢ output.node ∈ {node}
      simp only [List.mem_toFinset] at hOutputnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeoutput:SourcePortInstance NodeId OutputPortSignaturehOutput:output ∈ List.map sourceOutputInstance exits⊢ output.node ∈ {node}
      rcases List.mem_map.mp hOutput with ⟨exit, hExit, hEq⟩node:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeoutput:SourcePortInstance NodeId OutputPortSignaturehOutput:output ∈ List.map sourceOutputInstance exitsexit:AdmissionBoundaryPorthExit:exit ∈ exitshEq:exit.sourceOutputInstance = output⊢ output.node ∈ {node}
      subst hEqnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeexit:AdmissionBoundaryPorthExit:exit ∈ exitshOutput:exit.sourceOutputInstance ∈ List.map sourceOutputInstance exits⊢ exit.sourceOutputInstance.node ∈ {node}
      exact Finset.mem_singleton.mpr (hExitNodes exit hExit)All goals completed! 🐙)
    (bynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = node⊢ ∀ input ∈ (List.map sourceInputInstance entries).toFinset, input.node ∈ {node}
      intro input hInputnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeinput:SourcePortInstance NodeId InputPortSignaturehInput:input ∈ (List.map sourceInputInstance entries).toFinset⊢ input.node ∈ {node}
      simp only [List.mem_toFinset] at hInputnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeinput:SourcePortInstance NodeId InputPortSignaturehInput:input ∈ List.map sourceInputInstance entries⊢ input.node ∈ {node}
      rcases List.mem_map.mp hInput with ⟨entry, hEntry, hEq⟩node:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeinput:SourcePortInstance NodeId InputPortSignaturehInput:input ∈ List.map sourceInputInstance entriesentry:AdmissionBoundaryPorthEntry:entry ∈ entrieshEq:entry.sourceInputInstance = input⊢ input.node ∈ {node}
      subst hEqnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthEntryNodes:∀ entry ∈ entries, entry.node = nodehExitNodes:∀ exit ∈ exits, exit.node = nodeentry:AdmissionBoundaryPorthEntry:entry ∈ entrieshInput:entry.sourceInputInstance ∈ List.map sourceInputInstance entries⊢ entry.sourceInputInstance.node ∈ {node}
      exact Finset.mem_singleton.mpr (hEntryNodes entry hEntry)All goals completed! 🐙)

end AdmissionBoundaryPortnamespace WireAdmissionArtifact

Phantom Reconstruction Contract

Primitive-backed open phantom-node object reconstructed for one adapter row.

structure PhantomBridgeObjectReconstruction
    (artifact : WireAdmissionArtifact)
    (phantom : PhantomAdapterArtifact)
    (entries exits : List AdmissionBoundaryPort) : Prop where
  primitiveNode :
    PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveSteps
  entriesOwned : ∀ entry, entry ∈ entries → entry.node = phantom.node
  exitsOwned : ∀ exit, exit ∈ exits → exit.node = phantom.node

No two entries share a boundary key. Load-bearing against silent collapse in openBoundaryNodeObject's .toFinset dedup, which projects on the (node, port, contract) key only (see AdmissionBoundaryPort.key).

entriesUnique : (entries.map AdmissionBoundaryPort.key).Nodup

No two exits share a boundary key. Same role as entriesUnique.

  exitsUnique : (exits.map AdmissionBoundaryPort.key).Nodup
  leftBulkTargetsMatchPrimitive :
    phantom.leftBulkTargetKeys.Perm (entries.map AdmissionBoundaryPort.key)
  rightBulkSourcesMatchPrimitive :
    phantom.rightBulkSourceKeys.Perm (exits.map AdmissionBoundaryPort.key)

The open phantom-node object is source-linear. The proof is the smart constructor's built-in openNodePorts_portLinear invariant; it does not depend on artifact-specific data. The no-silent-collapse fields downstream consumers should read are entriesUnique / exitsUnique.

  openObjectLinear :
    (AdmissionBoundaryPort.openBoundaryNodeObject
      phantom.node entries exits entriesOwned exitsOwned).graph.PortLinear
  inputKeysAccounted :
    ∀ {key : NodeId × FieldLabel × ContractId},
      key ∈ entries.map AdmissionBoundaryPort.key →
        PrimitiveInputKeyAccounted artifact key
  outputKeysAccounted :
    ∀ {key : NodeId × FieldLabel × ContractId},
      key ∈ exits.map AdmissionBoundaryPort.key →
        PrimitiveOutputKeyAccounted artifact key

Product-shape reconstruction for a phantom artifact row.

inductive PhantomProductReconstruction
    (artifact : WireAdmissionArtifact)
    (phantom : PhantomAdapterArtifact) : Prop where
  | record
      {contract : ContractId}
      {fields : List (FieldLabel × ContractId)}
      (shape_eq : phantom.productShape =
        ProductShapeArtifact.record contract fields)
      (contractValid : contract.Valid)
      (fieldRowsValid :
        ∀ field, field ∈ fields → field.fst.Valid ∧ field.snd.Valid)
      (fieldsUnique : (fields.map Prod.fst).Nodup)
      (multiLengthEq : phantom.multi.length = fields.length)
      (multiFieldsPerm :
        (phantom.multi.filterMap AdmissionBoundaryPort.recordField).Perm fields)
      (singularContractEq : phantom.singular.contract = contract) :
        PhantomProductReconstruction artifact phantom
  | indexed
      {element : ContractId}
      {count : Nat}
      (shape_eq : phantom.productShape =
        ProductShapeArtifact.indexed element count)
      (elementValid : element.Valid)
      (elementNominal : element.name.startsWith "[" = false)
      (multiLengthEq : phantom.multi.length = count)
      (multiContractEq :
        ∀ boundary, boundary ∈ phantom.multi → boundary.contract = element)
      (multiCompatibilityKeysUnique :
        (phantom.multi.map AdmissionBoundaryPort.compatibilityShape).Nodup)
      (singularContractEq :
        phantom.singular.contract = ContractId.boundedIndexed element count) :
        PhantomProductReconstruction artifact phantom

Direction-specific replay evidence for the source-visible * endpoints.

inductive PhantomDirectionReconstruction
    (artifact : WireAdmissionArtifact)
    (phantom : PhantomAdapterArtifact) : Prop where
  | gather
      (direction_eq : phantom.direction = PhantomAdapterDirection.gather)
      (leftBulkSourcesPermMulti :
        phantom.leftBulkSourceKeys.Perm
          (phantom.multi.map AdmissionBoundaryPort.key))
      (rightBulkTargetsPermSingular :
        phantom.rightBulkTargetKeys.Perm [phantom.singular.key])
      (multiEndpointsReplayed :
        ∀ {boundary : AdmissionBoundaryPort},
          boundary ∈ phantom.multi →
            ∃ pair, pair ∈ phantom.leftBulk ∧
              pair.fromKey = boundary.key ∧
                pair ∈ PrimitiveGraphStep.matchedConnectionsList
                  artifact.primitiveSteps)
      (singularEndpointReplayed :
        ∃ pair, pair ∈ phantom.rightBulk ∧
          pair.toKey = phantom.singular.key ∧
            pair ∈ PrimitiveGraphStep.matchedConnectionsList
              artifact.primitiveSteps) :
        PhantomDirectionReconstruction artifact phantom
  | scatter
      (direction_eq : phantom.direction = PhantomAdapterDirection.scatter)
      (leftBulkSourcesPermSingular :
        phantom.leftBulkSourceKeys.Perm [phantom.singular.key])
      (rightBulkTargetsPermMulti :
        phantom.rightBulkTargetKeys.Perm
          (phantom.multi.map AdmissionBoundaryPort.key))
      (singularEndpointReplayed :
        ∃ pair, pair ∈ phantom.leftBulk ∧
          pair.fromKey = phantom.singular.key ∧
            pair ∈ PrimitiveGraphStep.matchedConnectionsList
              artifact.primitiveSteps)
      (multiEndpointsReplayed :
        ∀ {boundary : AdmissionBoundaryPort},
          boundary ∈ phantom.multi →
            ∃ pair, pair ∈ phantom.rightBulk ∧
              pair.toKey = boundary.key ∧
                pair ∈ PrimitiveGraphStep.matchedConnectionsList
                  artifact.primitiveSteps) :
        PhantomDirectionReconstruction artifact phantom

Artifact-boundary reconstruction evidence for one phantom adapter row indexed by a shared primitive bridge witness.

The bridgeEntries / bridgeExits parameters name the single primitive node row that backs the adapter node. Sharing them at this layer pins the bridge frontier witness to one concrete primitive row, removing the ambiguity that would otherwise arise from bridge carrying its own existential (entries, exits). The bulk-replay fields don't quantify over any primitive frontier row — they only assert membership in matchedConnectionsList, so they're unaffected by this parameterization.

structure PhantomAdapterReconstructionRecord
    (artifact : WireAdmissionArtifact)
    (phantom : PhantomAdapterArtifact)
    (bridgeEntries bridgeExits : List AdmissionBoundaryPort) : Prop where
  valid : phantom.Valid
  bridge :
    PhantomBridgeObjectReconstruction artifact phantom bridgeEntries bridgeExits
  product : PhantomProductReconstruction artifact phantom
  direction : PhantomDirectionReconstruction artifact phantom
  leftBulkReplayed :
    ∀ {pair : AdmissionConnection},
      pair ∈ phantom.leftBulk →
        pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rightBulkReplayed :
    ∀ {pair : AdmissionConnection},
      pair ∈ phantom.rightBulk →
        pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps

Artifact-boundary reconstruction evidence for one phantom adapter row.

def PhantomAdapterReconstruction
    (artifact : WireAdmissionArtifact)
    (phantom : PhantomAdapterArtifact) : Prop :=
  ∃ bridgeEntries bridgeExits,
    PhantomAdapterReconstructionRecord artifact phantom bridgeEntries bridgeExits

Artifact-boundary phantom reconstruction for every phantom adapter row.

def PhantomReconstruction (artifact : WireAdmissionArtifact) : Prop :=
  ∀ phantom, phantom ∈ artifact.phantomAdapters →
    PhantomAdapterReconstruction artifact phantom

Reconstruction Theorems

Phantom soundness reconstructs the source-linear open object for the adapter node.

theorem Sound.phantomBridgeObjectReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    ∃ entries exits,
      PhantomBridgeObjectReconstruction artifact phantom entries exits := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ ∃ entries exits, artifact.PhantomBridgeObjectReconstruction phantom entries exits
  obtain ⟨entries, exits, hPrimitiveNode, hEntries, hExits⟩ :=
    hSound.phantom.phantomBridgeFrontiersMatchPrimitive phantom hPhantomartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)⊢ ∃ entries exits, artifact.PhantomBridgeObjectReconstruction phantom entries exits
  have hPrimitiveValid :
      (PrimitiveGraphStep.node phantom.node entries exits).Valid :=
    hSound.primitive.primitiveStepsValid
      (PrimitiveGraphStep.node phantom.node entries exits)
      hPrimitiveNodeartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).Valid⊢ ∃ entries exits, artifact.PhantomBridgeObjectReconstruction phantom entries exits
  have hOwned := hPrimitiveValid.frontiersOwnedartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exits⊢ ∃ entries exits, artifact.PhantomBridgeObjectReconstruction phantom entries exits
  have hFrontierLinear := hPrimitiveValid.frontiersLinearartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exits⊢ ∃ entries exits, artifact.PhantomBridgeObjectReconstruction phantom entries exits
  have hAccounted :
      artifact.PrimitiveFrontierKeysAccounted :=
    primitiveFrontierKeysAccounted
      hSound.primitive.summaryFrontiersMatchPrimitiveartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∃ entries exits, artifact.PhantomBridgeObjectReconstruction phantom entries exits
  refine
    ⟨ entries
    , exits
    , { primitiveNode := hPrimitiveNode
        entriesOwned := hOwned.left
        exitsOwned := hOwned.right
        entriesUnique := hFrontierLinear.left
        exitsUnique := hFrontierLinear.right
        leftBulkTargetsMatchPrimitive := hEntries
        rightBulkSourcesMatchPrimitive := hExits
        openObjectLinear :=
          (AdmissionBoundaryPort.openBoundaryNodeObject
            phantom.node entries exits hOwned.left hOwned.right).linear
        inputKeysAccounted := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {key : NodeId × FieldLabel × ContractId},
  key ∈ List.map AdmissionBoundaryPort.key entries → artifact.PrimitiveInputKeyAccounted key
          intro key hKeyartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccountedkey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entries⊢ artifact.PrimitiveInputKeyAccounted key
          have hPrimitiveKey :
              key ∈ PrimitiveGraphStep.nodeEntryKeysList
                artifact.primitiveSteps :=
            PrimitiveGraphStep.nodeEntryKeysList_mem_of_node_mem
              hPrimitiveNode hKeyartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccountedkey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entrieshPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted key
          exact hAccounted.inputs hPrimitiveKeyAll goals completed! 🐙
        outputKeysAccounted := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {key : NodeId × FieldLabel × ContractId},
  key ∈ List.map AdmissionBoundaryPort.key exits → artifact.PrimitiveOutputKeyAccounted key
          intro key hKeyartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccountedkey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exits⊢ artifact.PrimitiveOutputKeyAccounted key
          have hPrimitiveKey :
              key ∈ PrimitiveGraphStep.nodeExitKeysList
                artifact.primitiveSteps :=
            PrimitiveGraphStep.nodeExitKeysList_mem_of_node_mem
              hPrimitiveNode hKeyartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveStepshEntries:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key entries)hExits:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key exits)hPrimitiveValid:(PrimitiveGraphStep.node phantom.node entries exits).ValidhOwned:PrimitiveGraphStep.NodeFrontiersOwned phantom.node entries exitshFrontierLinear:PrimitiveGraphStep.NodeFrontiersLinear entries exitshAccounted:artifact.PrimitiveFrontierKeysAccountedkey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitshPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted key
          exact hAccounted.outputs hPrimitiveKeyAll goals completed! 🐙 }
    ⟩

Phantom soundness reconstructs product-shape evidence for one adapter row.

theorem Sound.phantomProductReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    PhantomProductReconstruction artifact phantom := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ artifact.PhantomProductReconstruction phantom
  have hValid := hSound.phantom.phantomAdaptersValid phantom hPhantomartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Valid⊢ artifact.PhantomProductReconstruction phantom
  cases hShape : phantom.productShape with
  | record contract fields =>recordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fields⊢ artifact.PhantomProductReconstruction phantom
      have hProductValid := hValid.productShapeValidrecordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:phantom.productShape.Valid⊢ artifact.PhantomProductReconstruction phantom
      have hArity := hValid.productArityMatchesrecordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:phantom.productShape.ValidhArity:phantom.ProductArityMatches⊢ artifact.PhantomProductReconstruction phantom
      have hSingular := hValid.productContractMatchesSingularrecordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:phantom.productShape.ValidhArity:phantom.ProductArityMatcheshSingular:phantom.ProductContractMatchesSingular⊢ artifact.PhantomProductReconstruction phantom
      unfold PhantomAdapterArtifact.ProductArityMatches at hArityrecordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:phantom.productShape.ValidhArity:phantom.multi.length = phantom.productShape.arityhSingular:phantom.ProductContractMatchesSingular⊢ artifact.PhantomProductReconstruction phantom
      unfold PhantomAdapterArtifact.ProductContractMatchesSingular at hSingularrecordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:phantom.productShape.ValidhArity:phantom.multi.length = phantom.productShape.arityhSingular:phantom.singular.contract = phantom.productShape.contract⊢ artifact.PhantomProductReconstruction phantom
      rw [hShape] at hProductValid hArity hSingularrecordartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:(ProductShapeArtifact.record contract fields).ValidhArity:phantom.multi.length = (ProductShapeArtifact.record contract fields).arityhSingular:phantom.singular.contract = (ProductShapeArtifact.record contract fields).contract⊢ artifact.PhantomProductReconstruction phantom
      exact
        PhantomProductReconstruction.record
          hShape
          (ProductShapeArtifact.valid_record_contractValid hProductValid)
          (fun field hField =>
            ProductShapeArtifact.valid_record_fieldValid hProductValid hField)
          (hSound.phantom.recordFieldsUnique hPhantom hShape)
          (byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:(ProductShapeArtifact.record contract fields).ValidhArity:phantom.multi.length = (ProductShapeArtifact.record contract fields).arityhSingular:phantom.singular.contract = (ProductShapeArtifact.record contract fields).contract⊢ phantom.multi.length = fields.length simpa [ProductShapeArtifact.arity] using hArityAll goals completed! 🐙)
          (hSound.phantom.recordMultiFieldsPerm hPhantom hShape)
          (byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validcontract:ContractIdfields:List (FieldLabel × ContractId)hShape:phantom.productShape = ProductShapeArtifact.record contract fieldshProductValid:(ProductShapeArtifact.record contract fields).ValidhArity:phantom.multi.length = (ProductShapeArtifact.record contract fields).arityhSingular:phantom.singular.contract = (ProductShapeArtifact.record contract fields).contract⊢ phantom.singular.contract = contract simpa [ProductShapeArtifact.contract] using hSingularAll goals completed! 🐙)
  | indexed element count =>indexedartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validelement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element count⊢ artifact.PhantomProductReconstruction phantom
      have hProductValid := hValid.productShapeValidindexedartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validelement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthProductValid:phantom.productShape.Valid⊢ artifact.PhantomProductReconstruction phantom
      have hCompatibility := hValid.indexedMultiCompatibilityKeysUniqueindexedartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validelement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthProductValid:phantom.productShape.ValidhCompatibility:phantom.IndexedMultiCompatibilityKeysUnique⊢ artifact.PhantomProductReconstruction phantom
      unfold PhantomAdapterArtifact.IndexedMultiCompatibilityKeysUnique
        at hCompatibilityindexedartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validelement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthProductValid:phantom.productShape.ValidhCompatibility:match phantom.productShape with
| ProductShapeArtifact.record contract fields => True
| ProductShapeArtifact.indexed elementContract count =>
  (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup⊢ artifact.PhantomProductReconstruction phantom
      rw [hShape] at hProductValid hCompatibilityindexedartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Validelement:ContractIdcount:ℕhShape:phantom.productShape = ProductShapeArtifact.indexed element counthProductValid:(ProductShapeArtifact.indexed element count).ValidhCompatibility:match ProductShapeArtifact.indexed element count with
| ProductShapeArtifact.record contract fields => True
| ProductShapeArtifact.indexed elementContract count =>
  (List.map AdmissionBoundaryPort.compatibilityShape phantom.multi).Nodup⊢ artifact.PhantomProductReconstruction phantom
      exact
        PhantomProductReconstruction.indexed
          hShape
          (hSound.phantom.indexedElementValid hPhantom hShape)
          (hSound.phantom.indexedElementNominal hPhantom hShape)
          (hSound.phantom.indexedMultiLengthEq hPhantom hShape)
          (fun boundary hBoundary =>
            hSound.phantom.indexedMultiContractEq
              hPhantom hShape hBoundary)
          hCompatibility
          (hSound.phantom.indexedSingularContractEq hPhantom hShape)All goals completed! 🐙

Phantom soundness reconstructs replay evidence for a gather singular endpoint.

theorem PhantomSound.gatherSingularEndpointReplayed
    {artifact : WireAdmissionArtifact}
    (hPhantomSound : artifact.PhantomSound)
    {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:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gather⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hValid := hPhantomSound.phantomAdaptersValid phantom hPhantomartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.Valid⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hPartition := hValid.bulkEndpointPartitionartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.ValidhPartition:phantom.BulkEndpointPartition⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.ValidhPartition: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)⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rw [hDirection] at hPartitionartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.ValidhPartition: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)⊢ ∃ pair ∈ phantom.rightBulk,
  pair.toKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hKeyMem :
      phantom.singular.key ∈ phantom.rightBulkTargetKeys :=
    hPartition.right.mem_iff.mpr (byartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.ValidhPartition: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.singular.key ∈ [phantom.singular.key] simpAll goals completed! 🐙)
  unfold PhantomAdapterArtifact.rightBulkTargetKeys at hKeyMemartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.ValidhPartition: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)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:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhValid:phantom.ValidhPartition: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)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
    , (hPhantomSound.phantomBridgeBulkConnectionsReplayed
        phantom hPhantom).right pair hPair
    ⟩All goals completed! 🐙

Phantom soundness reconstructs replay evidence for a scatter singular endpoint.

theorem PhantomSound.scatterSingularEndpointReplayed
    {artifact : WireAdmissionArtifact}
    (hPhantomSound : artifact.PhantomSound)
    {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:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hValid := hPhantomSound.phantomAdaptersValid phantom hPhantomartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.Valid⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hPartition := hValid.bulkEndpointPartitionartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.ValidhPartition:phantom.BulkEndpointPartition⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.ValidhPartition: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)⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  rw [hDirection] at hPartitionartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.ValidhPartition: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)⊢ ∃ pair ∈ phantom.leftBulk,
  pair.fromKey = phantom.singular.key ∧ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  have hKeyMem :
      phantom.singular.key ∈ phantom.leftBulkSourceKeys :=
    hPartition.left.mem_iff.mpr (byartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.ValidhPartition: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.singular.key ∈ [phantom.singular.key] simpAll goals completed! 🐙)
  unfold PhantomAdapterArtifact.leftBulkSourceKeys at hKeyMemartifact:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.ValidhPartition: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)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:WireAdmissionArtifacthPhantomSound:artifact.PhantomSoundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhValid:phantom.ValidhPartition: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)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
    , (hPhantomSound.phantomBridgeBulkConnectionsReplayed
        phantom hPhantom).left pair hPair
    ⟩All goals completed! 🐙

Phantom soundness reconstructs direction-specific endpoint replay evidence.

theorem Sound.phantomDirectionReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    PhantomDirectionReconstruction artifact phantom := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ artifact.PhantomDirectionReconstruction phantom
  have hValid := hSound.phantom.phantomAdaptersValid phantom hPhantomartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.Valid⊢ artifact.PhantomDirectionReconstruction phantom
  have hPartition := hValid.bulkEndpointPartitionartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition:phantom.BulkEndpointPartition⊢ artifact.PhantomDirectionReconstruction phantom
  cases hDirection : phantom.direction with
  | gather =>gatherartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition:phantom.BulkEndpointPartitionhDirection:phantom.direction = PhantomAdapterDirection.gather⊢ artifact.PhantomDirectionReconstruction phantom
      unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitiongatherartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition: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)hDirection:phantom.direction = PhantomAdapterDirection.gather⊢ artifact.PhantomDirectionReconstruction phantom
      rw [hDirection] at hPartitiongatherartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition: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)hDirection:phantom.direction = PhantomAdapterDirection.gather⊢ artifact.PhantomDirectionReconstruction phantom
      exact
        PhantomDirectionReconstruction.gather
          hDirection
          hPartition.left
          hPartition.right
          (fun hBoundary =>
            hSound.phantom.gatherMultiEndpointReplayed
              hPhantom hDirection hBoundary)
          (hSound.phantom.gatherSingularEndpointReplayed
            hPhantom hDirection)All goals completed! 🐙
  | scatter =>scatterartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition:phantom.BulkEndpointPartitionhDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ artifact.PhantomDirectionReconstruction phantom
      unfold PhantomAdapterArtifact.BulkEndpointPartition at hPartitionscatterartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition: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)hDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ artifact.PhantomDirectionReconstruction phantom
      rw [hDirection] at hPartitionscatterartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershValid:phantom.ValidhPartition: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)hDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ artifact.PhantomDirectionReconstruction phantom
      exact
        PhantomDirectionReconstruction.scatter
          hDirection
          hPartition.left
          hPartition.right
          (hSound.phantom.scatterSingularEndpointReplayed
            hPhantom hDirection)
          (fun hBoundary =>
            hSound.phantom.scatterMultiEndpointReplayed
              hPhantom hDirection hBoundary)All goals completed! 🐙

Validator soundness reconstructs phantom-adapter artifact-boundary witnesses.

theorem Sound.toPhantomReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound) :
    artifact.PhantomReconstruction := byartifact:WireAdmissionArtifacthSound:artifact.Sound⊢ artifact.PhantomReconstruction
  intro phantom hPhantomartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ artifact.PhantomAdapterReconstruction phantom
  obtain ⟨bridgeEntries, bridgeExits, hBridge⟩ :=
    hSound.phantomBridgeObjectReconstruction hPhantomartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersbridgeEntries:List AdmissionBoundaryPortbridgeExits:List AdmissionBoundaryPorthBridge:artifact.PhantomBridgeObjectReconstruction phantom bridgeEntries bridgeExits⊢ artifact.PhantomAdapterReconstruction phantom
  refine ⟨bridgeEntries, bridgeExits, ?_⟩artifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersbridgeEntries:List AdmissionBoundaryPortbridgeExits:List AdmissionBoundaryPorthBridge:artifact.PhantomBridgeObjectReconstruction phantom bridgeEntries bridgeExits⊢ artifact.PhantomAdapterReconstructionRecord phantom bridgeEntries bridgeExits
  exact
    { valid := hSound.phantom.phantomAdaptersValid phantom hPhantom
      bridge := hBridge
      product := hSound.phantomProductReconstruction hPhantom
      direction := hSound.phantomDirectionReconstruction hPhantom
      leftBulkReplayed := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersbridgeEntries:List AdmissionBoundaryPortbridgeExits:List AdmissionBoundaryPorthBridge:artifact.PhantomBridgeObjectReconstruction phantom bridgeEntries bridgeExits⊢ ∀ {pair : AdmissionConnection},
  pair ∈ phantom.leftBulk → pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
        intro pair hPairartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersbridgeEntries:List AdmissionBoundaryPortbridgeExits:List AdmissionBoundaryPorthBridge:artifact.PhantomBridgeObjectReconstruction phantom bridgeEntries bridgeExitspair:AdmissionConnectionhPair:pair ∈ phantom.leftBulk⊢ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
        exact
          (hSound.phantom.phantomBridgeBulkConnectionsReplayed
            phantom hPhantom).left pair hPairAll goals completed! 🐙
      rightBulkReplayed := byartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersbridgeEntries:List AdmissionBoundaryPortbridgeExits:List AdmissionBoundaryPorthBridge:artifact.PhantomBridgeObjectReconstruction phantom bridgeEntries bridgeExits⊢ ∀ {pair : AdmissionConnection},
  pair ∈ phantom.rightBulk → pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
        intro pair hPairartifact:WireAdmissionArtifacthSound:artifact.Soundphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptersbridgeEntries:List AdmissionBoundaryPortbridgeExits:List AdmissionBoundaryPorthBridge:artifact.PhantomBridgeObjectReconstruction phantom bridgeEntries bridgeExitspair:AdmissionConnectionhPair:pair ∈ phantom.rightBulk⊢ pair ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
        exact
          (hSound.phantom.phantomBridgeBulkConnectionsReplayed
            phantom hPhantom).right pair hPairAll goals completed! 🐙 }

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.AdmissionArtifact.Phantom Next →Cortex.Wire.AdmissionArtifact.Primitive