refactor(uc): drop MachineId and key momentary corruption by an abstract identity

[dtumad]

MachineId (sid, pid), MachineProcess, HasAccessControl, and the session-coherence predicates had no consumer in PolyFun or VCVio, and the categorical UC account keeps identities out of the semantic core: they are a translation surface for Canetti's named ITMs (Theorem IV.6 of FKKKT26), not an ingredient of composition. The module is removed.

MomentaryCorruption keyed its alphabet, bookkeeping state, and canonical process by MachineId Sid Pid; it now takes an arbitrary machine identity type M with decidable equality, so CJSV22's (sid, pid) pairs remain one instantiation among others. MachineProcess.withMomentaryCorruption becomes OpenProcess.withMomentaryCorruption. Docstrings that named MachineId as the canonical identity and the wiki ledger row for Theorem IV.6 now say that no addressing scheme is built in.

Public API delta

• Removed module Interaction/UC/MachineId (MachineId, MachineProcess, HasAccessControl, and the session-coherence predicates); PolyFun.lean regenerated.
• MomentaryCorruption: the alphabet, state, and canonical process are parameterized by an abstract identity type M with decidable equality instead of Sid Pid; MachineProcess.withMomentaryCorruption is renamed to OpenProcess.withMomentaryCorruption.
• Docstring updates in Interface, EnvAction, EnvOpenProcess, CorruptionModel, Leakage; the Theorem IV.6 row of the uc.md ledger and the DAG entries in interaction.md and repo-map.md.

Semantics

• Identities are a translation surface for named ITMs, not part of composition; keeping them out of the semantic core matches the categorical account. Nothing composed through MachineId.
• VCVio has no code use of MachineId, MachineProcess, or withMomentaryCorruption. The docstring of VCVio/Interaction/UC/AsyncRuntime.lean (line 60) mentions MomentaryCorruption.Alphabet Sid Pid; when VCVio bumps its PolyFun pin (currently c0c9236) that wording becomes M := Sid × Pid.

Validation

• Rebased onto main at e4099b4 (feat(tocslib): add polynomial-time single-tape toolkit #178) with no conflicts; the Lean sources are byte-identical to the version validated during development.
• git diff --check, scripts/check-imports.sh, scripts/check-modules.sh, both docs-integrity checks, and ./scripts/validate.sh --lint --test --axioms on this branch: lint passes for PolyFun and ToCslib; the axiom sweep reports 10865 declarations across 281 modules with zero sorry and zero non-standard axioms.

Audit note

• Attacked: consumers of the removed declarations (none in PolyFun, PolyFunTest, or VCVio at origin/main); whether generalizing the key loses the CJSV22 instantiation (it does not: take M := Sid × Pid).
• Outside the result: a named-ITM translation layer, if one is ever wanted, is downstream work.

Stack

Independent of the UC coherence stack (dtumad/uc-activation-coherence → dtumad/uc-sampler-coherence → dtumad/uc-quotient-theory); based on main and mergeable in any order relative to it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EtHsoefgvyzMtfdyqjLVhT