petri-net lemmas

# Petri Net Lemmas

Formal properties of arcnet's Petri net object model.

## Definitions

**Model** = (P, T, A) where:
- P = set of places
- T = set of transitions
- A = set of arcs ⊆ (P × T) ∪ (T × P)

**Marking** M : P → ℕ assigns token counts to places.

**Bindings** β : Var → Value assigns values to transition parameters.

**Guard** g : Bindings → Bool is a predicate on bindings.

---

## Structural Lemmas

### Lemma 1: Bipartite Graph Property

*Arcs connect only places to transitions or transitions to places.*

```
∀ (s, t) ∈ A:
  (s ∈ P ∧ t ∈ T) ∨ (s ∈ T ∧ t ∈ P)
```

This ensures the alternating flow: tokens rest in places, transitions move them.

### Lemma 2: Well-Formed Model

*A valid model has unique identifiers and valid arc references.*

```
∀ p₁, p₂ ∈ P: p₁.id = p₂.id → p₁ = p₂
∀ t₁, t₂ ∈ T: t₁.id = t₂.id → t₁ = t₂
∀ (s, t) ∈ A: s ∈ (P ∪ T) ∧ t ∈ (P ∪ T)
```

---

## Firing Lemmas

### Lemma 3: Enabling Condition

*A transition t is enabled at marking M iff all input places have sufficient tokens.*

```
enabled(t, M) ⟺ ∀ (p, t) ∈ A: M(p) ≥ weight(p, t)
```

### Lemma 4: Firing Rule

*Firing transition t transforms marking M to M' by consuming inputs and producing outputs.*

```
fire(t, M) = M' where:
  ∀ p ∈ P:
    M'(p) = M(p) - weight(p, t) + weight(t, p)
```

where weight(x, y) = 0 if (x, y) ∉ A.

### Lemma 5: Atomicity

*Transition firing is atomic—consumption and production occur as a single step.*

```
¬∃ M_intermediate:
  M →consume M_intermediate →produce M'
```

This prevents observing partial states during a transition.

---

## Conservation Lemmas

### Lemma 6: Token Conservation (Closed Systems)

*For a model with no sources (mint) or sinks (burn), total tokens are conserved.*

```
Let sources(t) = {p | (t, p) ∈ A ∧ ¬∃p': (p', t) ∈ A}
Let sinks(t) = {p | (p, t) ∈ A ∧ ¬∃p': (t, p') ∈ A}

If ∀ t ∈ T: sources(t) = ∅ ∧ sinks(t) = ∅
Then: Σₚ M(p) = Σₚ M'(p) after any firing
```

### Lemma 7: Balance Invariant (ERC-20)

*For fungible tokens, the sum of all balances equals total supply.*

```
Let balances = {p | p.schema = "balance"}
Let supply = {p | p.id = "totalSupply"}

Invariant: Σₚ∈balances M(p) = M(totalSupply)
```

This holds because transfer moves tokens between balances without changing supply.

---

## Guard Lemmas

### Lemma 8: Guard Satisfaction

*A guarded transition fires only when its guard evaluates to true.*

```
fire(t, M, β) is defined ⟺
  enabled(t, M) ∧ guard(t)(β) = true
```

### Lemma 9: Guard Compositionality

*Guards compose via boolean operators.*

```
guard(g₁ ∧ g₂, β) = guard(g₁, β) ∧ guard(g₂, β)
guard(g₁ ∨ g₂, β) = guard(g₁, β) ∨ guard(g₂, β)
guard(¬g, β) = ¬guard(g, β)
```

---

## Reachability Lemmas

### Lemma 10: Reachability Closure

*The reachability relation is the reflexive transitive closure of the firing relation.*

```
M →* M' ⟺ M = M' ∨ ∃M'': M → M'' ∧ M'' →* M'
```

### Lemma 11: Deadlock Condition

*A marking M is a deadlock iff no transition is enabled.*

```
deadlock(M) ⟺ ∀ t ∈ T: ¬enabled(t, M)
```

### Lemma 12: Liveness

*A transition t is live iff from any reachable marking, t can eventually fire.*

```
live(t) ⟺ ∀ M ∈ Reach(M₀): ∃ M' ∈ Reach(M): enabled(t, M')
```

---

## Capacity Lemmas

### Lemma 13: Capacity Constraint

*Places with capacity limits block transitions that would overflow.*

```
enabled(t, M) → ∀ (t, p) ∈ A:
  p.capacity = 0 ∨ M(p) + weight(t, p) ≤ p.capacity
```

### Lemma 14: Capacity Boundedness

*A place with finite capacity has bounded token count in all reachable markings.*

```
p.capacity > 0 → ∀ M ∈ Reach(M₀): M(p) ≤ p.capacity
```

---

## Colored Petri Net Lemmas

### Lemma 15: Binding Independence

*Different bindings define different transition instances.*

```
fire(t, M, β₁) ≠ fire(t, M, β₂) when β₁ ≠ β₂
```

### Lemma 16: Token Identity (NFTs)

*For colored tokens with identity, each token is distinguishable.*

```
Let tokens(p) = {(id, owner) | id ∈ tokenIds(p)}
∀ id: |{(id, _) ∈ tokens(p)}| ≤ 1
```

This captures ERC-721's uniqueness: each tokenId has exactly one owner.

---

## Viewing Objects (Yoneda Perspective)

The Yoneda lemma tells us: *an object is completely determined by its relationships to all other objects*. In Petri net terms:

### Lemma 17: Place Identity (Yoneda)

*A place is defined by the transitions it connects to.*

```
place(p) ≅ (inputs(p), outputs(p))
where:
  inputs(p) = {t | (t, p) ∈ A}   -- transitions that produce here
  outputs(p) = {t | (p, t) ∈ A}  -- transitions that consume here
```

A place with no connections is indistinguishable from absence. A place *is* its role in the flow network.

### Lemma 18: Transition Identity (Yoneda)

*A transition is defined by its input/output signature and guard.*

```
transition(t) ≅ (pre(t), post(t), guard(t))
where:
  pre(t) = {(p, w) | (p, t) ∈ A, weight = w}   -- what it consumes
  post(t) = {(p, w) | (t, p) ∈ A, weight = w}  -- what it produces
```

Two transitions with identical pre/post/guard are *the same operation*, regardless of name.

### Lemma 19: Marking as Functor

*A marking is a functor from places to quantities.*

```
M : P → ℕ
```

The marking "probes" each place to reveal the system state. This is the Yoneda embedding: we understand the net by how markings interact with it.

### Lemma 20: Model as Presheaf

*A Petri net model is a presheaf over the category of flow relationships.*

```
Model : Flow^op → Set
where Flow has:
  - objects: places and transitions
  - morphisms: arcs (with weights)
```

The model is completely determined by:
1. What flows into each node
2. What flows out of each node
3. The conditions (guards) on each flow

---

## Object Summary

| Object | Yoneda View | "Is Defined By" |
|--------|-------------|-----------------|
| Place | Hom(−, p) ∪ Hom(p, −) | Its input/output transitions |
| Transition | pre × post × guard | What it consumes, produces, requires |
| Arc | Morphism in Flow | Connection with weight |
| Marking | Functor P → ℕ | Token count at each place |
| Model | Presheaf over Flow | All relationships, completely |

**Key insight**: You don't need to look "inside" an object. A place *is* its connections. A transition *is* its behavior. The Petri net *is* its flow structure.

This is why CID (content-addressed identity) works: the model's identity emerges from its structure, not from arbitrary naming.