feat(uc): coherence shapes for interleaving; the process model's laws as instances

[dtumad]

Five commits, each validated on its own and best reviewed one at a time. Together they replace the one-off proofs of the process model's activation-level laws by three generic coherence shapes, add the traced laws that had no proof before, and name the strict target a process model can honestly reach.

1. HasPlugFactorization (OpenTheory/PlugFactorization.lean). The UC composition theorems only ever consume five equalities: plug_comm and the residual-context factorizations close_par_left, close_par_right, close_wire_left, close_wire_right. They become a class on top of IsLawful, strictly weaker than HasPlugWireFactor: every HasPlugWireFactor theory is an instance (hasPlugFactorization_of_hasPlugWireFactor, priority 100) and OpenTheory.pi lifts it pointwise. Emulates derives every observation's RespectsFactorization from the class alone. The residual-context formers parContextLeft, parContextRight, wireContextLeft, wireContextRight move to the new module and are exposed.
2. Routed interleaving and re-decoration (Concurrent/RoutedInterleave.lean, UC/OpenProcessInterleave.lean). ProcessOver.interleaveRouted keeps the shape of interleave and adds a routing hook: after the scheduled side completes a step path, a route may update the other side's state from that path; with trivial routes it is interleave on the nose. OpenProcess.mapHom re-decorates an open process along an arbitrary node-context hom (mapBoundary is the boundary-morphism case), OpenNodeContext.PreservesActivation names the homs that silence cannot see (instances for every structural hom), and OpenProcess.interleaveRouted lifts routing to open processes with samplers.
3. Coherence shapes and congruence (UC/OpenProcessCoherence.lean). Silence of a composite step; the three shapes every activation-level law is an instance of (reassociation, commutation, re-homing) with left and right absorption of a silent unit; congruence of OpenProcessActivationEquiv under interleave and mapHom, lifting delay bisimulations through silent prefixes. OpenProcessInterleave gains the normalization equalities (mapHom_interleave, mapBoundary_interleave, interleave_mapHom_left, interleave_mapHom_right) that push outer re-decoration into the injections.
4. Process-model laws as instances (UC/OpenProcessModel.lean). Every law of openTheory up to activation equivalence is now simp only [openTheory], normalization, one shape, and the congruence. Proofs are at most twenty lines and the implicit_reducible workaround is gone. The traced laws wire_assoc, wire_par_superpose, and wire_comm, which had no up-to-equivalence version before, are added the same way.
5. Plug factorization laws as instances (UC/OpenProcessFactorization.lean). The four openTheory_plug_{par,wire}_{left,right}_activation_equiv laws become chains of the shapes, about twenty lines each instead of two hundred.

Every existing law keeps its name and statement.

Public API delta

• New modules Interaction/Concurrent/RoutedInterleave, Interaction/UC/OpenProcessInterleave, Interaction/UC/OpenProcessCoherence, Interaction/UC/OpenTheory/PlugFactorization (DAG entries in docs/wiki/repo-map.md; OpenProcessModel now imports OpenProcessCoherence).
• New class OpenTheory.HasPlugFactorization. The instance respectsFactorization_of_hasPlugWireFactor in Emulates is replaced by respectsFactorization_of_hasPlugFactorization with the weaker hypothesis. The five laws and the four residual-context formers keep their names and namespace but now live in OpenTheory/PlugFactorization with [HasPlugFactorization T] hypotheses.
• Moved and made public: OpenProcess.ext_of_step_eq, OpenProcess.heq_step_of_processOver_eq (from OpenProcessModel to OpenProcessInterleave).
• New: ProcessOver.interleaveRouted, OpenProcess.mapHom, OpenProcess.interleaveRouted, OpenNodeContext.PreservesActivation, isSilentStep_interleave{Routed}_{left,right}_iff, interleave_{assoc,comm,rehome}_activationEquiv, interleave_unit_{left,right}_activationEquiv, OpenProcess.interleave_congr_{left,right}, OpenProcess.mapHom_congr, mapBoundary_eq_mapHom, openTheory_{wire_assoc,wire_par_superpose,wire_comm}_activation_equiv, schedulerNode_isActivated, map_schedulerNode_isActivated, openTheoryUnit_isSilentStep, openTheoryIdWire_isSilentStep.
• Nothing else is removed.

Semantics

• HasPlugFactorization is exactly what Emulates consumes, and it is the strict target a process model can honestly aim for: at strong sampler equivalence interleave unit p has one more path per step than p, so the unit and snake laws of HasPlugWireFactor admit no path bijection (recorded in the uc.md ledger row).
• In interleaveRouted the scheduled side steps, the route sees the completed path and updates the frozen side. RoutedPlugExamples closes a reactive process against a reactive context by routing every emitted packet across the plug. It runs over the possibilistic SetM monad with no probability: the real and ideal one-time pad are sampler-bisimilar via the key bijection, a fixed distinguisher reaches both verdicts against either, and it never reaches the verdict false against a protocol that leaks its plaintext. The structural plug of openTheory erases packets, so no statement of that shape is available there.
• The activation shapes assume only PreservesActivation injections and silent scheduler nodes; the model's instances supply both by instance search plus schedulerNode_isActivated.

Tests

• Ordinary-import canaries in PolyFunTest/ModuleAPI/Interaction.lean: the five factorization laws, interleave_eq_interleaveRouted, mapBoundary_eq_mapHom, silence under mapHom, interleave_comm_activationEquiv, and wire_assoc and wire_par_superpose on openTheory.
• Worked examples: PolyFunTest/Interaction/UC/PlugFactorizationExamples.lean (the free model reaches the class through its strict instance, a family of theories reaches it pointwise, and the whole Emulates suite elaborates from the class alone with no unit, identity wire, or snake law in scope), RoutedPlugExamples.lean (above), OpenProcessCoherenceExamples.lean (re-derives par_assoc, par_comm, the left unit law, and plug_par_left from the shapes: normalize, one shape, chain through the congruence).

Validation

• Rebased linearly onto main at e4099b4 (feat(tocslib): add polynomial-time single-tape toolkit #178). The Lean sources of every commit are byte-identical to the versions validated during development; only the wiki DAG entries and the canary file were merged (one blank line restored).
• On each of the five commits: git diff --check, scripts/check-imports.sh, scripts/check-modules.sh, and both docs-integrity checks. lake build && lake test on commits 1, 2, 4, and 5 (the tip).
• ./scripts/validate.sh --lint --test --axioms at the tip of the stack (dtumad/uc-quotient-theory, which contains this PR): lint passes for PolyFun and ToCslib; the axiom sweep reports 11255 declarations across 291 modules with zero sorry and zero non-standard axioms.

Audit note

• Attacked: whether three shapes cover every model law (commits 4 and 5 contain no unfolding beyond simp only [openTheory] and the normalization equalities); whether PreservesActivation holds for the composite injections the model uses (instances for the six structural homs and composition); whether routing changes interleave for trivial routes (rfl); whether a fixed distinguisher can be fooled by routing (the leaky-protocol example).
• Hardened: Emulates no longer needs the unit and snake laws; the process model's proofs no longer depend on implicit_reducible; the traced laws now have up-to-equivalence versions.
• Outside the result: the same shapes up to sampler equivalence (next PR in the stack); strict laws for process models (impossible for unit and snake; the quotient PR gives the strict class on the activation quotient); routing inside openTheory itself.
• VCVio uses HasPlugWireFactor, openTheory, and the Emulates names generically (Computational.lean, Standard.lean, Runtime.lean, AsyncSecurity.lean); none of the moved, renamed, or added declarations is referenced there, and VCVio pins PolyFun at c0c9236 (28 commits behind main), so nothing moves downstream until a deliberate bump.

Stack

1 of 3: this PR → dtumad/uc-sampler-coherence → dtumad/uc-quotient-theory. dtumad/uc-drop-machineid is independent. The later PRs are based on this branch; merge bottom-up, after which the next PR is retargeted to main.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EtHsoefgvyzMtfdyqjLVhT