refactor(interaction): let the observation carry the UC factorization laws

[dtumad]

Summary

• add Observation.RespectsPlugComm and Observation.RespectsFactorization, stating plug commutation and the four close_* factorizations up to Obs.rel instead of as strict equalities
• add respectsFactorization_of_hasPlugWireFactor, so any observation over a HasPlugWireFactor theory satisfies both classes by reflexivity
• restate Emulates.{par_left, par_right, par_compose, wire_left, wire_right, wire_compose} against RespectsFactorization, and Emulates.{plug_right, plug_compose} against the weaker RespectsPlugComm
• add Interaction/UC/OpenProcessEmulates.lean with Observation.IsSchedulingInsensitive and the RespectsPlugComm instance it yields for openTheory
• add PolyFunTest/Interaction/UC/EmulatesFactorizationExamples.lean

Why

Emulates' composition theorems were gated on OpenTheory.HasPlugWireFactor. The free syntax models instantiate that; the process-backed openTheory cannot, because par/wire/plug each prepend a scheduler node, so reassociating a composite changes the step tree's type and the laws hold only up to OpenProcessActivationEquiv. Emulates.lean said as much in prose — "those theorems do not apply to it directly" — and worked around it for one law with the _of_observes_plug_comm variants.

This generalizes that workaround from one law to all of them. The laws are the same; what changes is who is asked to supply them. A theory with strict coherence supplies them by rfl, so nothing that held before stops holding. A model that can only offer an observation coarse enough not to see scheduler nodes now supplies them too, and Emulates.plug_right / plug_compose reach openTheory for the first time.

Worth noting explicitly: Emulates · · Obs, read as a family indexed by boundary, is already closed under exactly these motions — par_compose and wire_left are the parallel and sequential closure conditions one would assume of an abstract indistinguishability relation. The classes make that closure the interface rather than a consequence of strictness. This is the same split used in the categorical treatment of UC in ePrint 2026/1605, which assumes those two conditions and derives the composition theorems from them.

Deliberately excluded. RespectsFactorization for openTheory — the par/wire half — is not here. It needs activation-equivalence versions of plug_par_left and plug_wire_left, which do not exist yet (nor do any of the three IsTraced laws that would be the categorical route to them). The module docstring records this and it is the subject of a follow-up. The class is also deliberately not an extension of IsCompactClosed: openTheory has neither a HasUnit nor a HasIdWire instance, and requiring them would put the class out of its reach for no gain.

API change. Emulates.plug_right_of_observes_plug_comm and Emulates.plug_compose_of_observes_plug_comm are removed; RespectsPlugComm subsumes them. Callers holding the old bare hypothesis migrate with haveI : Obs.RespectsPlugComm := ⟨hcomm⟩. There are no in-tree callers, and VCVio does not consume Emulates at all — its Interaction/UC/Computational.lean carries its own copy of the suite — so nothing downstream breaks.

Validation

• ./scripts/validate.sh --lint --test
• full library build with warnings as errors
• environment lint, full PolyFunTest build, import and documentation integrity checks
• regression check that Expr.theory still resolves RespectsFactorization by synthesis and still elaborates par_compose, wire_compose, and plug_compose (covered by the new test file)
• docs/wiki/interaction.md UC table and docs/wiki/repo-map.md layering updated for the new module

[dtumad]

Follow-ups filed: #123 supplies the two missing activation-equivalence laws so openTheory can satisfy RespectsFactorization outright, and #122 records the wider design argument this change is a first step in.