# Process Contract Lab — autonomous run, 7 September 2026

This increment develops the existing parallel process-to-plan site through two independent constructions: complete producer-count ancestry families for a selected trace, and a typed linear-wire compiler. The [workbench](../apps/process-contract-lab/) brings their results together; the [method note](process-contract-method.md) states the definitions and limits.

The previous causal lab remains available. Its FIFO/LIFO counterexample supplied the starting question: what changes when all compatible ancestries are retained, and what additional structure is needed to construct a process compositionally?

## Actual construction and review loops

1. **Define the harder target.** The family engine was assigned full finite allocation enumeration, order languages and exact single-graph tests. A separate author built typed identities, permutations, tensor and selective sequence composition. An independent reviewer owned a structurally different oracle suite and challenged the definitions before treating implementation as evidence.

2. **Correct the stopping and scope semantics.** Review identified that first-goal input validation differs from the full-occurrence language of a witness. Independent B followed by goal-producing A is a first-goal input trace, while its lawful reordered A,B covers the goal before completing the selected work. The result contract now distinguishes input stopping policy from retained work scope. A further shared-token example distinguishes one input trace’s ancestry family from all count-level reorderings of the same task set.

3. **Expose a failure of the single-graph summary.** The OR-support example has two exact individual trees, but their four-order union cannot be represented by any one dependency DAG on those occurrences. The common relation admits C before either producer; the union relation wrongly demands both producers before C. Actual extra and excluded words support the verdict. A reviewer supplied the converse distinction too: mixed exact/N witnesses can have a fully parallel combined language when initial tokens permit a no-edge witness. Individual classification and family summary remain separate in the interface.

4. **Construct selective wiring.** The typed compiler preserves ordered port identity through identities, permutations and composition. It compiles an N without inventing the missing cross-dependency, and constructs an eight-event refuge with six complete event orders. Explicit event-completion markers handle sink generators; an explicitly declared empty-identity sentinel adapts the zero-event case to the reused positive-goal API. Same-type wires stay distinct, and zero-input generators are rejected rather than given invented resources.

5. **Check with independent oracles.** The family reviewer labelled individual tokens, enumerated consumed subsets and quotiented only completed allocation tables. This differed from production’s producer-count-vector search. For typed terms, the reviewer threaded consumer demands backward from outputs, rather than copying production’s forward wire evaluator. Both results were compared with generated plans and independently enumerated event orders. Identity, associativity, interchange, symmetry and permutation inverses were tested on concrete terms.

6. **Make the concurrency boundary executable.** Review showed why even a correct linear-order language is too weak to certify concurrency: A,B and B,A can both be lawful while one shared token prevents a joint start. A bounded step checker now replays a chosen atomic prefix and compares individual enabling with joint input availability, withholding all outputs until completion. An independent oracle tries disjoint assignments of labelled tokens rather than repeating the production inequality. This addition checks a specific marking; it does not claim full timed or step-language equivalence.

7. **Review the usable handoff.** The interface computes in a replaceable worker, retains completed results while attempting edits and exports definitions plus a selected trace for recomputation. Read-only review identified cancellation-promise settlement, cancelled-control restoration and imported-view restoration as specific recovery checks for the interface author. The interface now settles cancelled work, restores completed controls, and restores the imported view. The completed local browser journey checks all three paths, cancellation during an import, and superseding one worker with another. Wire targets were enlarged after ordinary interaction found a zero-height SVG hit box. Portable exports use compact trace indices when identifiers would otherwise be repeated; their partial derived certificate is explicitly recomputed on opening.

The engine and interface authors also maintain their own tests. These are observed work steps and substantive semantic corrections, not a claim that a multi-agent workflow by itself validates the result.

## Independent evidence checkpoint

At this checkpoint, **17 independent oracle tests pass**:

| Check | Evidence |
|---|---|
| Small pooled producer/consumer grid | 42 valid models; 776 labelled token outcomes reduce to exactly 301 producer-count classes |
| Timing | Each retained small-grid witness independently passes count replay at simultaneous start/finish timestamps |
| Concurrent starts | 807 small resource models, every atomic prefix and selected subset: 12,105 comparisons with disjoint labelled-token assignment, including 3,083 individually enabled but jointly blocked selections |
| Alternative languages | Full permutation comparison verifies Must/May, exact-DAG verdicts and actual extra/excluded words |
| Distinct questions | All exact individual trees with no exact family DAG, and mixed exact/N witnesses with an exact parallel family language |
| Multiplicity | Different producer-count contributions remain distinct even when their event order is the same; repeated occurrences retain IDs |
| Bounds | Ancestry and language cutoffs do not produce false universal classifications or complete certificates |
| Scope | Partial/after-goal input rejection, empty identity, early-goal reordered work and distinct resource-order trace families |
| Typed port identity | 154 permutation/inverse cases on zero through five equal-type wires |
| Typed composition | Backward denotation, identity, sequential/tensor associativity, interchange, symmetry naturality, pass-through wires and fresh occurrence naming |
| Larger typed example | The eight-event refuge matches backward wiring, all 40,320 candidate event permutations filter to exactly six generated traces, and each has earliest finish 15 |
| Model behavior | Selective N, shared-resource threading versus two owned resources, empty/sink completion instrumentation, type/arity/permutation/name errors |

This grid is exhaustive only over its stated small parameter domain. The tests do not establish every finite net, arbitrary category-theoretic coherence, calibrated construction timings or human usefulness. The prior causal lab’s larger finite-order oracle remains a separate inherited test suite.

## Completed local integration checkpoint

The combined suite passes **93 tests**: the 35 retained earlier tests, 15 ancestry-family tests, 17 typed-composition tests, 17 independent oracle tests, four joint-step tests and five portable-result tests. The portable tests cover definitions at the 250,000-character boundary, multibyte Unicode, repeated long identifiers, legacy raw traces and rejected invalid or disagreeing trace indices. Full definitions and selected work survive the roundtrip; derived detail is recomputed.

A fresh Chrome profile passes **39 workbench checks** and **29 retained causal-lab checks**. These cover selection, counterexamples, typed wire inspection, local joint starts, export/reopen, forged-claim rejection, edited definitions, corrected duration/reload, invalid input, empty identity, cancellation, superseded work, keyboard navigation, phone layouts and ordinary entry/return routes. Desktop and 390-pixel screenshots were inspected. These are agent-operated checks; no human-user or engineering validation is claimed.

Reproduce with `node --test tests/*.test.mjs`, `scripts/process-contract-browser.mjs` and `scripts/browser-check.mjs` as described in the [repository README](../README.md). The [GitHub Actions record](https://github.com/lawrencerowland/gimmer-crag-project-mountain-refuge/actions) separately identifies the tested pull-request commit and Pages deployment. Publication and exact served-source verification are separate evidence from this completed local checkpoint.

## What is now possible

The lab can distinguish individual plan representability from representability of a family of alternatives, and can return finite counterexamples when conjunctions of dependency pairs are insufficient. It can also build a process from explicit typed interfaces and generate complete plans whose dependencies retain selective wiring.

The two capabilities preserve their boundary. Typed wire identity resolves ownership by supplying more information. It does not infer that information from pooled token counts. The family language is relative to a selected trace and retains its event scope; it is not the entire project’s behavior. Earliest-finish ranges are allocation calculations, not probabilities or latest-finish guarantees.

## Next research frontier

A useful continuation would compare selected-trace families with all legal count-level reorderings of the same explicitly identified work, and enumerate reachable jointly enabled steps beyond the current single-prefix check. A one-token resource example is already enough to show why this matters: both serial orders can be legal while concurrency is impossible. Matching interleaving languages would therefore be too weak a completion criterion by itself.

The deeper compositional question is how to connect alternative-support families across interfaces while retaining explicit resource ownership, disjunction and occurrence identity. This requires a defined composition contract and replayable counterexamples, rather than simply concatenating graphs or pooling equal type names. The present constructor and family engine are a bounded foundation for that test, not its completed proof.