feat(interaction): plug factorization for the process model up to activation equivalence

[dtumad]

Stacked on #121 — review that first; this PR's base is its branch. Closes #123.

Summary

• add Interaction/UC/OpenProcessFactorization.lean with the four factorization laws for openTheory up to OpenProcessActivationEquiv: openTheory_plug_{par,wire}_{left,right}_activation_equiv
• move openTheory_plug_par_left_activation_equiv and its siblings into that module rather than growing OpenProcessModel.lean past the 1500-line cap (it stays at its current 971 lines)
• add respectsFactorization_of_isSchedulingInsensitive, completing the instance story begun in refactor(interaction): let the observation carry the UC factorization laws #121
• extend EmulatesFactorizationExamples.lean with par_compose and wire_compose on the process model

Why

#121 made the composition theorems depend on the observation rather than on strict compact-closed structure, but openTheory could still only satisfy the weaker RespectsPlugComm. The par and wire half needed activation-equivalence versions of plug_par_left and plug_wire_left, which did not exist — and neither did any of the three IsTraced laws that would be the categorical route to them.

So they are proved directly, as OpenProcessActivationEquiv.of_step_match bisimulations in the established style of openTheory_par_assoc_activation_equiv. In each case the state relation is a regrouping of the nested product of component states, and the four step obligations re-encode a two-bit scheduler path as a one-bit one. What makes this work is that the scheduler nodes being moved are .internal, so isActivated is false and activationLTS labels them silent — the delay bisimulation absorbs exactly the nodes the regrouping introduces or removes.

The _right variants are proved directly rather than derived from the _left ones. The strict proofs of close_par_right / close_wire_right rewrite under plug using par_comm / wire_comm, which needs activation equivalence to be a congruence for plug; no such lemma exists, and wire_comm has no activation-equivalence version either. A plug-congruence lemma would be independently useful and would shorten this file, but it is a separate piece of work.

The payoff is that the concrete, probability-carrying model now meets the same interface as the free syntax models, so Emulates.par_compose and Emulates.wire_compose apply to it — which is the general validation that #121's design actually works, not just on the models that already had strict coherence.

Deliberately excluded. No IsTraced or IsCompactClosed instance for openTheory; those laws remain unproved for this model and are not needed here. No probability — that stays downstream in VCVio, per the scope boundary.

Validation

• ./scripts/validate.sh --lint --test
• full library build with warnings as errors
• environment lint, full PolyFunTest build, import and documentation integrity checks
• Obs.RespectsFactorization resolves by synthesis for openTheory, and par_compose / wire_compose elaborate against it (new examples in the test file)
• all three UC modules stay under the 1500-line cap: OpenProcessFactorization.lean 916, OpenProcessModel.lean 971, OpenProcessEmulates.lean 127
• docs/wiki/interaction.md UC table and docs/wiki/repo-map.md layering updated for the new module

[dtumad]

Note on CI: ci.yml, check-imports.yml, and docs-integrity.yml all trigger only on pull_request: branches: [main], so while this PR is based on #121's branch only Lint Style and the OpenRouter key check run. The full suite ran locally — ./scripts/validate.sh --lint --test passes, covering the same build/lint/test/import/docs jobs. Retargeting to main after #121 merges will run them in CI.