Plasmoid-Merger Petri Net

MIF-012 implements a one-safe stochastic Petri net for the local FRC plasmoid-merger control contract:

approach -> contact -> reconnection -> coalescence -> phase_locked

Unsafe tilt growth or density asymmetry routes the net to the terminal abort sink. Every normal transition consumes the single active token and produces one token in the next place, so the marking remains one-safe. The matching Lean proof surface records the finite one-token marking invariant, transition preservation, terminal stability, and nominal reachability to phase_locked.

Delay fields are discrete sampled tick counts, not continuous dwell times. Python rejects fractional or boolean delay values before coercion; Rust/PyO3 accepts only integer tick-count arguments. This keeps the Python reference, Rust runtime, and CONTROL topology export aligned on the same sampled Petri-net semantics.

Guards

From	To	Guard
approach	contact	axial separation at or below contact_separation_m and closing speed above threshold
contact	reconnection	normalised reconnection flux reaches reconnection_flux_min for the configured delay
reconnection	coalescence	density asymmetry is inside the coalescence window for the configured delay
coalescence	phase_locked	phase-lock error and axial separation are inside their tolerances for the configured delay
any non-terminal place	abort	tilt growth or density asymmetry exceeds the abort envelope

The SCPN-CONTROL export mirrors terminal stability by attaching both terminal places, phase_locked and abort, as inhibitor arcs to every transition. This keeps the CONTROL topology absorbing after either terminal sink is marked.

Python API

plasmoid_merger_petri_net

One-safe stochastic Petri net for FRC plasmoid merger dynamics.

MIF-012 models the control-state progression for a two-plasmoid FRC merge: approach, contact, reconnection, coalescence, and phase lock. The local carrier keeps the MIF-specific guard thresholds here while preserving a constructor shim for the pinned SCPN-CONTROL StochasticPetriNet surface.

MergerPlace

Bases: StrEnum

Places in the MIF FRC plasmoid-merger Petri net.

MergerTransition

Bases: StrEnum

Transitions in the MIF FRC plasmoid-merger Petri net.

PlasmoidMergerSpec(contact_separation_m=0.002, min_closing_speed_m_s=300000.0, reconnection_flux_min=0.72, coalescence_density_asymmetry_max=0.12, phase_lock_tolerance_rad=0.01, max_tilt_growth_rate_s=50000.0, contact_delay_ticks=1, reconnection_delay_ticks=2, coalescence_delay_ticks=2, phase_lock_delay_ticks=3, firing_probability=1.0, abort_density_asymmetry_max=0.35) dataclass

Guard thresholds and stochastic firing policy for MIF-012.

__post_init__()

Validate Petri-net thresholds and abort limits.

MergerObservation(separation_m, relative_velocity_m_s, phase_lock_error_rad, reconnection_flux_norm, density_asymmetry, tilt_growth_rate_s) dataclass

Single sampled observation driving the merger Petri-net guards.

__post_init__()

Validate observed plasmoid-merger state scalars.

MergerMarking(tokens, total_tokens) dataclass

Token marking for the one-safe merger net.

max_tokens_per_place property

Return the maximum token count held by any place.

MergerTransitionRecord(tick, transition, from_place, to_place, reason) dataclass

Audit record for a fired merger transition.

MergerStep(tick, place, transition, fired, reason, dwell_ticks, marking) dataclass

Result of evaluating one sampled observation.

MergerVerificationReport(passed, trials, steps_per_trial, failures, terminal_counts, max_tokens_per_place) dataclass

Boundedness or liveness verification summary.

PlasmoidMergerPetriNet(spec, seed=None)

Stateful one-safe stochastic Petri net for MIF FRC merger control.

audit_log property

Return immutable fired-transition audit entries.

reset(seed=None)

Reset to the initial approach marking.

copy()

Return a copy with identical state and an independently seeded RNG.

marking()

Return the current one-safe marking.

enabled_transition(observation)

Return the transition currently enabled by observation.

step(observation)

Evaluate one sampled observation and fire at most one transition.

build_control_petri_net(spec, net_factory=None)

Build the pinned SCPN-CONTROL StochasticPetriNet shape for MIF-012.

verify_merger_boundedness(spec=None, *, trials=100, steps_per_trial=500, seed=0)

Run the requested stochastic boundedness campaign.

verify_merger_liveness(spec=None, *, trials=1000, steps_per_trial=200, seed=0)

Run the requested liveness campaign against nominal merger stimuli.

verify_merger_boundedness_seeded(spec=None, *, trials=100, steps_per_trial=500, seed=0)

Run the boundedness campaign with independent per-trial seeding.

Unlike :func:verify_merger_boundedness, which threads one generator through every trial (so trial k's stimuli depend on how trials 0..k-1 consumed the stream), each trial here draws from its own :func:_trial_seed-derived generator. The result is therefore invariant to trial execution order — the property the Rust parallel campaign lane relies on — and the Rust sequential, Rust parallel, and this reference all produce bit-identical reports.

verify_merger_liveness_seeded(spec=None, *, trials=1000, steps_per_trial=200, seed=0)

Run the liveness campaign with independent per-trial seeding.

The per-trial seeding contract matches :func:verify_merger_boundedness_seeded; see there for how it differs from the shared-stream :func:verify_merger_liveness.

Dispatch

Use scpn_mif_core.lifecycle.dispatched_plasmoid_merger_petri_net(...) for the fastest available measured runtime backend:

"lifecycle.plasmoid_merger_petri_net" = ["rust", "python"]

The Python reference remains available for deterministic debugging and tests.

Verification

The committed MIF-012 tests cover:

• nominal collision-to-phase-lock progression;
• deterministic transition-delay behaviour for reconnection, coalescence, and final phase lock;
• reset semantics with and without stochastic reseeding;
• fail-closed validation of discrete integer delay ticks;
• abort routing for unsafe tilt or density asymmetry;
• CONTROL topology export with both terminal inhibitor arcs and the default pinned import path;
• the required boundedness campaign (100 × 500);
• explicit broken-marking detection in the boundedness verifier;
• the required liveness campaign (1 000 × 200);
• property-based one-safe marking preservation;
• Lean one-token marking and nominal reachability proofs;
• Python/Rust parity and dispatch fallback.

Benchmarks

Measured on the local i5-11600K rig using Python 3.12.3 and Rust 1.85.0. The result is a non-isolated local comparison, not a production latency claim.

Group	Backend	Mean	Result
campaign_8	Rust	3.43 us	fastest
campaign_8	Python	45.51 us	13.3x slower than Rust
boundedness_100x500	Rust	4.18 ms	fastest
boundedness_100x500	Python	421.38 ms	100.8x slower than Rust

Raw summary: bench/results/plasmoid_merger_petri_net.json.

Independently seeded campaigns (rayon lane)

verify_merger_boundedness_seeded / verify_merger_liveness_seeded and the dispatched dispatched_merger_boundedness_campaign / dispatched_merger_liveness_campaign run the same verification trials with an independent generator per trial (the seed ^ ((trial + 1) * mix) SplitMix64 convention shared with the MIF-017 stress injector). Unlike the original shared-stream verifiers — where trial k's stimuli depend on how earlier trials consumed the generator, which is inherently sequential — the seeded campaigns are invariant to trial execution order, so the Rust backend runs them across the rayon pool and still produces a report bit-identical to the Python floor and the Rust sequential lane (asserted whole-report, with failure strings, in tests/unit/lifecycle/test_merger_campaign_rust_parity.py). At the default budgets the measured gap is about two orders of magnitude (boundedness 100x500: 5.7 ms vs 588 ms median; liveness 1000x200: 0.7 ms vs 75.6 ms — see bench/results/merger_campaign.json for honest context). The shared-stream verifiers remain unchanged as the original documented contract.

Ownership

SYNC-STATE: upstream-pending applies to all MIF-012 implementation surfaces. SCPN-MIF-CORE owns the local MIF-specific Petri-net guards until SCPN-CONTROL receives the reusable Petri-net runtime and merger-control surface.