Molecular Quarantine Settlement: Per-Job Dispute Freezes over Globally Linear Typed Resources

Research corpus codename: NOOSPHERE.

Date: 2026-07-10 Provenance: Compiled from international-lab/invention-final.md (§S02, §4.2, §4.3) and the lab nel-quarantine-lab/ (README.md, nel_adapter.py, engine molecular_quarantine_test.py); every number below is copied from those artifacts — nothing here exists without an on-disk artifact behind it.

Abstract

A settlement layer that fail-stops globally on the first contradiction settles nothing. Molecular Quarantine Settlement (mechanism S02, [SURVIVOR-EXPERIMENT] grade N3 from the international-lab program) replaces global failure with two composed rules: per-job contradiction quarantine — conflicting evidence freezes only the membrane of the affected job — and globally linear typed resources — every settlement atomically consumes a set of globally unique typed IDs, so no resource can ever be paid twice, even across jobs. We wired the unmodified survivor engine onto MindChain's Neural Execution Lane (NEL) settlement vocabulary: jobs become PromptJobs, the consumed reactant triple becomes {EscrowNote, ExecutionRight, DisputeProof}, contradiction becomes conflicting ChunkClaims, and quarantine becomes the per-job DIVERGED dispute freeze of noosphere/05-neural-lane.md §3 rule 5. In the 4-job fixture, the monolithic baseline settles 0/4 jobs after one conflicting ChunkClaim; the mechanism settles the 1/4 independent valid job, quarantines the 1/4 contested job, refuses both cross-job resource-reuse attacks (2/2), rejects the one wrong-phase submission without consuming its proof (1/1), and produces one identical terminal projection across all 4,324,320/4,324,320 enumerated causal interleavings of the 14-event dependency graph — double_payouts=0 MEASURED 2026-07-10. The first implementation failed exactly where it should: job-scoped resource identity allowed 2 double payouts; the preserved failing run and the global-typed-ID revision are part of the record. This is a finite executable model, not a production settlement proof.

Claims

1. MEASURED 2026-07-10 Per-job quarantine preserves independent progress: in the 4-job NEL fixture, a conflicting-ChunkClaim dispute on job-atlas freezes only that job (quarantined_jobs=1 of 4), while job-borealis settles (mechanism_settled=1 of 4). The rejected monolithic baseline — one conflicting ChunkClaim fail-stops the batch — settles baseline_settled=0 of 4. Source: nel-quarantine-lab/README.md.
2. MEASURED 2026-07-10 Global linearity holds across membranes: double_payouts=0 over the entire explored state space. Both cross-job reuse adversaries — job-cinder replaying borealis's consumed ExecutionRight, job-dryad replaying its consumed DisputeProof — are refused (2/2 consumed_resource rejections), and exactly borealis's {EscrowNote, ExecutionRight, DisputeProof} triple is consumed (3/3 typed IDs, once each). Source: lab README gate table.
3. MEASURED 2026-07-10 Session fidelity: a settlement submission delivered while job-borealis is still in its claim phase is rejected as wrong_phase:evidence without consuming the dispute proof (1/1), and the legal retry after session open still settles. Source: lab README gates early_settle_rejected_wrong_phase, mechanism_settled.
4. MEASURED 2026-07-10 Bounded confluence: all 4,324,320/4,324,320 causal linear extensions of the 14-event fixture graph converge — one terminal projection, with equality asserted at every reachable causal prefix (invariant_gate=1). All 5/5 invalid local orders are classified as monitor rejections ({consumed_resource: 2, quarantined: 2, wrong_phase: 1}). Source: interleavings_enumerated=4324320, invalid_order_permutations=5 in the lab README.
5. MEASURED 2026-07-10 The NEL adaptation is structure-preserving, not cosmetic: the adapter's event dependency graph is isomorphic to the engine's own fixture, proven by matching linear-extension counts — engine_fixture_interleavings=4324320 = interleavings_enumerated=4324320 (causal_structure_preserved=1). Source: nel_adapter.py + lab README.
6. THEORY The protocol-scale claim — that per-job quarantine plus a globally-keyed typed-ID consumption ledger is the right settlement object for production NEL disputes (registered as M-QUARANTINE-SETTLE THEORY; fixture MEASURED 2026-07-10) — remains theory. Only the fixture is measured.

Non-claims. This is a finite executable model at 4-job fixture scale. It does not establish BFT consensus, cryptographic authorization, fair exchange, full MPST projection, Maude model checking, production P-system performance, or unbounded confluence (invention-final.md §S02 claims-not-made, §4.4). It makes no claim about real NEL wire objects, byte layouts, network timing, or committee incentives. It is not a production settlement proof.

Construction

State objects and rules

The engine (molecular_quarantine_test.py, an unmodified copy of the S02 survivor test) models settlement as chemistry under guard:

• JobMembrane — a local compartment per job holding its evidence set and session phase (EVIDENCE → OPEN → SETTLED, or QUARANTINED).
• ReactantID(kind, serial) — a globally unique typed resource: BUDGET, RIGHT, or PROOF. The linearity boundary is the global ConsumedSet, not the job.
• Evidence — FAVORABLE and CONTRARY coexist inside a membrane; contradiction is represented, never exploded into arbitrary inference (da Costa-style local non-explosion).
• GuardedReaction — a canonical predicate over membrane phase, evidence, and the exact typed reactants. A valid submission consumes all three reactants atomically and emits exactly one payout; a failed guard consumes nothing and emits a typed MonitorRejection (wrong_phase, quarantined, or consumed_resource).
• Quarantine rule — the moment favorable and contrary evidence coexist, that membrane (only) transitions to QUARANTINED; other membranes are untouched.
• Schedule exploration — the conformance oracle enumerates every causal linear extension of the fixture's event graph and compares canonical terminal projections at every reachable causal prefix (Maude-style executable discipline, implemented in stdlib Python).

stateDiagram-v2
    [*] --> EVIDENCE
    EVIDENCE --> EVIDENCE: early settle rejected wrong_phase, consumes nothing
    EVIDENCE --> OPEN: session opens
    OPEN --> SETTLED: guarded reaction consumes EscrowNote + ExecutionRight + DisputeProof
    OPEN --> QUARANTINED: conflicting ChunkClaims coexist
    QUARANTINED --> QUARANTINED: absorbing while unrelated membranes settle
    SETTLED --> [*]

Figure 1 — Job-membrane state machine: a valid guarded reaction atomically consumes the job's typed triple {EscrowNote, ExecutionRight, DisputeProof} and settles; coexisting conflicting ChunkClaims quarantine only that membrane, which is absorbing while unrelated jobs settle; a wrong-phase submission is rejected without consuming state. MEASURED 2026-07-10.

NEL settlement mapping

nel_adapter.py re-expresses the fixture in the vocabulary of noosphere/05-neural-lane.md (N-TOKEN-STATE section map) and runs the engine's own enumeration and decision logic on it, unchanged:

Fixture (14 events, 4 jobs): job-atlas receives one matching and one conflicting ChunkClaim → per-job DIVERGED freeze; job-borealis settles cleanly after a wrong-phase early submission is rejected without consumption; job-cinder and job-dryad attempt to settle by reusing borealis's already-consumed ExecutionRight and DisputeProof respectively.

flowchart TD
    ATLAS["job-atlas: matching + conflicting ChunkClaim"]
    BOR["job-borealis: valid submission"]
    CIN["job-cinder: replays borealis ExecutionRight"]
    DRY["job-dryad: replays borealis DisputeProof"]
    ATLAS --> QF["frozen DIVERGED<br/>quarantined_jobs = 1"]
    BOR --> TR["consumes its unique typed triple<br/>EscrowNote + ExecutionRight + DisputeProof"]
    TR --> ST["SETTLED<br/>mechanism_settled = 1"]
    CIN --> RC["refused: consumed_resource"]
    DRY --> RD["refused: consumed_resource"]
    RC --> DP["double_payouts = 0"]
    RD --> DP

Figure 2 — The four-job fixture: job-atlas is frozen by its contradiction, job-borealis settles by consuming its unique typed triple, and job-cinder/job-dryad are refused as consumed_resource when replaying borealis's already-consumed ExecutionRight and DisputeProof — double_payouts=0. MEASURED 2026-07-10.

The preserved first-run failure

The first implementation scoped consumed-resource identity by job. Adversarial jobs C and D reused job B's right and proof and received additional payouts — mechanism_settled=3, double_payouts=2, exit 1 (survivors/molecular_quarantine_first_run.log MEASURED, preserved run):

AssertionError: linearity invariant failed: right:right-b consumed by B and C; proof:proof-b consumed by B and D
EXIT_CODE=1

Revision: replace job-scoped consumption keys with one global set of typed, globally unique ReactantID values; a failed guard consumes nothing. Cross-job reuse now produces consumed_resource monitor rejections. The failure is evidence, not theater: it demonstrates that per-job quarantine without global resource identity is an exploitable design, which is precisely why the two rules ship as one mechanism.

Results

All values MEASURED 2026-07-10 by python nel_adapter.py, exit 0, gate_failures=0. Source: nel-quarantine-lab/README.md.

METRIC baseline_settled=0
METRIC mechanism_settled=1
METRIC quarantined_jobs=1
METRIC double_payouts=0
METRIC monitor_rejections=5
METRIC interleavings_enumerated=4324320
METRIC engine_fixture_interleavings=4324320
METRIC causal_structure_preserved=1
METRIC invalid_order_permutations=5
METRIC gate_failures=0
METRIC invariant_gate=1

Gate-by-gate (expected vs measured):

Confluence is asserted at every reachable causal prefix of every one of the 4,324,320 linear extensions of the 14-event causal graph (engine logic, untouched by the adapter).

flowchart LR
    CC["conflicting ChunkClaim on job-atlas"]
    CC --> BL["baseline: global fail-stop"]
    CC --> MQ["mechanism: per-job quarantine"]
    BL --> BH["all 4 jobs halt<br/>baseline_settled = 0"]
    MQ --> MF["only job-atlas frozen"]
    MF --> MS["job-borealis settles<br/>mechanism_settled = 1"]

Figure 3 — Global fail-stop vs per-job quarantine on the same contradiction: the baseline halts all 4 jobs (baseline_settled=0); the mechanism freezes only job-atlas and lets job-borealis settle (mechanism_settled=1) — invariant across all 4,324,320/4,324,320 enumerated causal interleavings. MEASURED 2026-07-10.

For contrast, the preserved first run of the engine — before the global-typed-ID revision (molecular_quarantine_first_run.log MEASURED, preserved failing run):

Falsifiers & kill thresholds

S02 / M-QUARANTINE-SETTLE is killed if any of the following is ever observed (invention-final.md §S02 falsifier; lab README kill threshold):

• Any ReactantID consumed twice — any double payout, in or across membranes.
• The contested (quarantined) job pays or settles.
• The unrelated valid job cannot settle while the baseline globally halts (loss of independent progress).
• Any wrong-phase input consumes state.
• Any two causally valid explored schedules produce different terminal projections — including any divergent projection at a shared causal prefix.
• Any invalid local order that executes instead of being classified as a monitor rejection.

A production proposal is additionally killed if it substitutes the words "membrane," "molecule," or "paraconsistent" for an executable rule and explicit global resource identity — the words are not the mechanism.

Current status: 0 kill conditions triggered across 4,324,320/4,324,320 interleavings and 5/5 invalid orders MEASURED 2026-07-10.

Reproduction

cd nel-quarantine-lab
python nel_adapter.py

Exit 0 ⇔ all gates pass. Stdlib-only Python, deterministic (no seeds, no network). The engine it drives, molecular_quarantine_test.py, is an unmodified copy of international-lab/survivors/molecular_quarantine_test.py; the original survivor gate reproduces with python survivors/molecular_quarantine_test.py from international-lab. The preserved failing first run is international-lab/survivors/molecular_quarantine_first_run.log.

Related work

Program-internal.

• international-lab/invention-final.md — S02 specification, grading (N3, SURVIVE, bounded), first-run failure (§4.2), final gate (§4.3), and limits table (§4.4). S02 survived an 18-kill program; its grade explicitly notes that metaphor-only "membranes" would be N0.
• noosphere/05-neural-lane.md — the NEL settlement vocabulary this mechanism is wired onto: PromptJob (§2.3), ChunkClaim (§2.5), the DIVERGED per-job freeze (§3 rule 5), escrow tranches (§9.1).
• noosphere/papers/04-genealogical-quorum.md — companion paper on S01, the other survivor of the same program, adapted to Chorus testimony aggregation.

Competitor dossiers (settlement and dispute posture surveyed in):

• nockchain-octra-ai-research-handoff/L1-plans/OCTRA/OCTRA-architecture-from-code.md and .../OCTRA/OCTRA-claims-vs-reality.md
• nockchain-octra-ai-research-handoff/L1-plans/NOCKCHAIN/NOCKCHAIN-architecture.md and .../NOCKCHAIN/NOCKCHAIN-claims-vs-reality.md
• research/08-pearl-matmul-pow.md
• noosphere/research/01-octra-hfhe-consensus-digest.md

External anchors (named in the S02 genealogy, invention-final.md §S02; the mechanism is their composition, and removing them reduces S02 to a workflow engine — prior art at N1/N2):

• Gh. Păun, "Computing with membranes," JCSS 2000 — compartment topology and local quarantine as computation structure. https://doi.org/10.1006/jcss.2000.1693
• G. Berry, G. Boudol, "The chemical abstract machine," TCS 1992 — settlement as an atomic consumed multiset. https://doi.org/10.1016/0304-3975(92)90185-I
• C. Fournet, G. Gonthier, "The reflexive CHAM and the join-calculus," POPL 1996. https://doi.org/10.1145/237721.237805
• N. C. A. da Costa, "On the theory of inconsistent formal systems," NDJFL 1974 — local non-explosion: A and ¬A coexist without trivializing the system. https://doi.org/10.1305/ndjfl/1093891487
• K. Ueda, Guarded Horn Clauses / KL1 (TR-103 lineage) — guard/body commitment and suspension. https://www.ueda.info.waseda.ac.jp/~ueda/publications.html
• K. Honda, N. Yoshida, M. Carbone, "Multiparty asynchronous session types," JACM 2016 — role/phase-local legality; wrong-order actions as typed rejections. https://doi.org/10.1145/2827695
• M. Clavel et al., All About Maude, Springer 2007 — the executable-across-adversarial-schedules discipline the Python oracle emulates (it is not Maude). https://doi.org/10.1007/978-3-540-71999-1