Skip to content

Plasmoid-merger Petri-net invariants

MIF-012 now has a Lean 4 proof surface for the finite one-token marking used by the Python and Rust plasmoid-merger Petri net.

The proof surface mirrors the runtime places and transitions:

inductive MergerPlace where
  | approach
  | contact
  | reconnection
  | coalescence
  | phaseLocked
  | abort

inductive MergerTransition where
  | detectContact
  | formReconnectionLayer
  | coalescePlasmoids
  | achievePhaseLock
  | abortUnstable

One-safety is represented by tokenAt active place, where the active place has one token and every other place has zero. Lean proves both per-place and transition-preservation contracts:

theorem one_safe_marking (active place : MergerPlace) :
    tokenAt active place ≤ 1

theorem total_tokens_one (active : MergerPlace) :
    totalTokens active = 1

theorem transition_preserves_one_safe_marking
    (transition : MergerTransition)
    (place : MergerPlace) :
    tokenAt (transitionTarget transition) place ≤ 1

The nominal guard-satisfied liveness path reaches the terminal phase-lock place:

theorem nominal_campaign_reaches_phase_locked :
    iterateNominal 4 MergerPlace.approach = MergerPlace.phaseLocked

theorem terminal_places_stable :
    nominalStep MergerPlace.phaseLocked = MergerPlace.phaseLocked ∧
      nominalStep MergerPlace.abort = MergerPlace.abort

The Python SCPN-CONTROL topology builder carries the same terminal-stability contract by exporting phase_locked and abort as inhibitor arcs on every transition. This prevents downstream CONTROL consumers from advancing the token once either terminal sink is marked.

This proof does not replace the stochastic boundedness and liveness campaigns. It formalises the finite marking invariant and nominal reachability skeleton that those executable campaigns exercise under sampled guard conditions.

Verification

  • lake build
  • pytest tests/unit/test_lean_plasmoid_merger_petri_net.py --no-cov -q