Cortex.Pulse.Frontier

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. Readiness Predicate
  5. Finite Frontier
  6. Antichain Theorem
Imports
import Cortex.Pulse.State

Overview

The Paper 1 fixed-topology kernel computes a frontier from an extensional state over a finite DAG. A ready node is pending and has every strict ancestor terminal. This reachability-level readiness is the proof-facing normal form; the executable runtime computes from direct predecessors, and later refinement lemmas can relate the two under reachable-state invariants.

The key result in this module is real, not axiomatized: all nodes in the frontier are ready, and any two distinct frontier nodes are incomparable by DAG reachability.

Context

The executable frontier is derived from direct predecessors. This proof module keeps both direct-predecessor readiness and strict-reachability readiness visible, so later validity theorems can bridge the executable frontier to the proof-facing antichain argument.

Theorem Split

The page defines readiness, constructs the finite frontier, proves the frontier membership theorem, and then derives the antichain result.

namespace Cortex.Pulsevariable {ν : Type u} {payload : Type v}

Readiness Predicate

Ready G state node means a topology node is pending and every strict ancestor is terminal.

def Ready (G : DAG ν) (state : GraphState ν payload) (node : ν) : Prop := node ∈ G.nodes ∧ state.status node = NodeStatus.pending ∧ ∀ predecessor : ν, G.reaches predecessor node → NodeStatus.terminal (state.status predecessor)

DirectReady G state node mirrors the executable direct-predecessor frontier check.

def DirectReady (G : DAG ν) (state : GraphState ν payload) (node : ν) : Prop := node ∈ G.nodes ∧ state.status node = NodeStatus.pending ∧ ∀ predecessor : ν, G.predecessor predecessor node → NodeStatus.unblocksSuccessors (state.status predecessor)

CausalHistoryClosed G state says unblocking nodes carry closed ancestor history.

def CausalHistoryClosed (G : DAG ν) (state : GraphState ν payload) : Prop := ∀ node : ν, NodeStatus.unblocksSuccessors (state.status node) → ∀ predecessor : ν, G.reaches predecessor node → NodeStatus.terminal (state.status predecessor)

directReady_ready_of_causalHistoryClosed bridges executable and proof frontiers.

theorem directReady_ready_of_causalHistoryClosed (G : DAG ν) (state : GraphState ν payload) {node : ν} (hCausal : CausalHistoryClosed G state) (hDirect : DirectReady G state node) : Ready G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ Ready G state node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ node ∈ G.nodesν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ state.status node = NodeStatus.pending ∧ ∀ (predecessor : ν), G.reaches predecessor node → (state.status predecessor).terminal ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ node ∈ G.nodes All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ state.status node = NodeStatus.pendingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ ∀ (predecessor : ν), G.reaches predecessor node → (state.status predecessor).terminal ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ state.status node = NodeStatus.pending All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state node⊢ ∀ (predecessor : ν), G.reaches predecessor node → (state.status predecessor).terminal intro predecessor ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state nodepredecessor:νhReach:G.reaches predecessor node⊢ (state.status predecessor).terminal ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state nodepredecessor:νhReach:G.reaches predecessor nodehEdge:G.edge predecessor node = true⊢ (state.status predecessor).terminalν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state nodepredecessor:νhReach:G.reaches predecessor nodedirect:νhPrefix:EdgePath G.edge predecessor directhEdge:G.edge direct node = true⊢ (state.status predecessor).terminal ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state nodepredecessor:νhReach:G.reaches predecessor nodehEdge:G.edge predecessor node = true⊢ (state.status predecessor).terminal All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhCausal:CausalHistoryClosed G statehDirect:DirectReady G state nodepredecessor:νhReach:G.reaches predecessor nodedirect:νhPrefix:EdgePath G.edge predecessor directhEdge:G.edge direct node = true⊢ (state.status predecessor).terminal All goals completed! 🐙

Finite Frontier

readyNodes G state is the finite frontier for a topology and state.

noncomputable def readyNodes (G : DAG ν) (state : GraphState ν payload) : Finset ν := ν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ Finset ν classical All goals completed! 🐙

directReadyNodes G state mirrors the runtime direct-predecessor frontier.

noncomputable def directReadyNodes (G : DAG ν) (state : GraphState ν payload) : Finset ν := ν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ Finset ν classical All goals completed! 🐙

mem_readyNodes states that frontier membership is exactly readiness.

theorem mem_readyNodes (G : DAG ν) (state : GraphState ν payload) (node : ν) : node ∈ readyNodes G state ↔ node ∈ G.nodes ∧ Ready G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:ν⊢ node ∈ readyNodes G state ↔ node ∈ G.nodes ∧ Ready G state node classical All goals completed! 🐙

mem_directReadyNodes states runtime frontier membership exactly.

theorem mem_directReadyNodes (G : DAG ν) (state : GraphState ν payload) (node : ν) : node ∈ directReadyNodes G state ↔ node ∈ G.nodes ∧ DirectReady G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:ν⊢ node ∈ directReadyNodes G state ↔ node ∈ G.nodes ∧ DirectReady G state node classical All goals completed! 🐙

frontier_only_ready states that every frontier node is ready.

theorem frontier_only_ready (G : DAG ν) (state : GraphState ν payload) : ∀ node ∈ readyNodes G state, Ready G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ ∀ node ∈ readyNodes G state, Ready G state node intro node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhNode:node ∈ readyNodes G state⊢ Ready G state node All goals completed! 🐙

Antichain Theorem

PairwiseReachabilityIncomparable G nodes means frontier members are mutually unreachable.

def PairwiseReachabilityIncomparable (G : DAG ν) (nodes : Finset ν) : Prop := ∀ a ∈ nodes, ∀ b ∈ nodes, a ≠ b → ¬ G.reaches a b ∧ ¬ G.reaches b a

ready_not_reaches_ready rules out strict reachability between ready nodes.

theorem ready_not_reaches_ready (G : DAG ν) (state : GraphState ν payload) {a b : ν} (hA : Ready G state a) (hB : Ready G state b) : ¬ G.reaches a b := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νb:νhA:Ready G state ahB:Ready G state b⊢ ¬G.reaches a b ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νb:νhA:Ready G state ahB:Ready G state bhReach:G.reaches a b⊢ False have hTerminal : NodeStatus.terminal NodeStatus.pending := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νb:νhA:Ready G state ahB:Ready G state b⊢ ¬G.reaches a b All goals completed! 🐙 All goals completed! 🐙

frontier_antichain proves the fixed-DAG frontier is a reachability antichain.

theorem frontier_antichain (G : DAG ν) (state : GraphState ν payload) : PairwiseReachabilityIncomparable G (readyNodes G state) := ν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ PairwiseReachabilityIncomparable G (readyNodes G state) intro a ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νhA:a ∈ readyNodes G state⊢ ∀ b ∈ readyNodes G state, a ≠ b → ¬G.reaches a b ∧ ¬G.reaches b a ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νhA:a ∈ readyNodes G stateb:ν⊢ b ∈ readyNodes G state → a ≠ b → ¬G.reaches a b ∧ ¬G.reaches b a ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νhA:a ∈ readyNodes G stateb:νhB:b ∈ readyNodes G state⊢ a ≠ b → ¬G.reaches a b ∧ ¬G.reaches b a ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νhA:a ∈ readyNodes G stateb:νhB:b ∈ readyNodes G state_hDistinct:a ≠ b⊢ ¬G.reaches a b ∧ ¬G.reaches b a ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νhA:a ∈ readyNodes G stateb:νhB:b ∈ readyNodes G state_hDistinct:a ≠ bhReadyA:Ready G state a⊢ ¬G.reaches a b ∧ ¬G.reaches b a ν:Type upayload:Type vG:DAG νstate:GraphState ν payloada:νhA:a ∈ readyNodes G stateb:νhB:b ∈ readyNodes G state_hDistinct:a ≠ bhReadyA:Ready G state ahReadyB:Ready G state b⊢ ¬G.reaches a b ∧ ¬G.reaches b a All goals completed! 🐙end Cortex.Pulse