feat(interaction): allowed-systems sub-theories and relativized emulation

[dtumad]

Summary

• PolyFun/Interaction/UC/SubTheory.lean (new). SubTheory T bundles a boundary-indexed mem : ∀ {Δ}, T.Obj Δ → Prop with closure under map, par, and wire. Closure under plug is the IsPlugClosed mixin, free for HasPlugWireFactor theories via plug_eq_wire; containment of the unit and identity wires is the IsStructural mixin. Plus the order ≤ with top, inf, and SubTheory.generated with its induction principle generated_le.
• PolyFun/Interaction/UC/EmulatesWithin.lean (new). EmulatesWithin D real ideal Obs restricts the plug quantifier of Emulates to D. The composition suite is restated against it, along with UCSecureWithin, whose simulator must map allowed contexts to allowed contexts. emulatesWithin_top_iff and ucSecureWithin_top_iff recover the unrelativized judgments.
• PolyFun/Interaction/UC/OpenSyntax/AtomSubTheory.lean (new). atomSubTheory is the sub-theory of Expr.theory generated by an allowed set of atoms plus the identity wires; interpretSubTheory is the pullback along interpretation; mem_interpret_of_atoms transfers allowedness from atoms to whole networks.
• PolyFunTest/Interaction/UC/SubTheoryExamples.lean (new), AGENTS.md, both wiki pages, regenerated PolyFun.lean.

Why

OpenTheory says how open systems compose. It has never said which open systems one is allowed to build, and every UC development needs that second notion — a corruption model restricts the machines a real protocol may use, an efficiency requirement restricts the machines anyone may use. Nothing predicate-on-objects existed anywhere in the repo before this PR.

The reason to make it a first-class object rather than a side condition is the closure fields. Read mem as "implementable within a fixed resource discipline"; then mem_par and mem_wire say a network of implementable systems is implementable. That property is normally assumed about a machine model, because stated globally over networks there is no finite obligation to discharge. Here a network is built from four operations, so the assumption is four fields — and SubTheory.generated_le reduces "everything in this protocol class is implementable" to "each generator is".

Two things fall out that are worth naming:

• The side condition is derived, not imposed. EmulatesWithin.par_left needs D.mem W₂ because the plug it hands to the inductive hypothesis is parContextLeft W₂ K. An abstract account of UC imposes "the map exhibiting the emulation lies in the allowed sub-category" by convention; here there is nowhere else it could come from.
• The simulator acquires an obligation. UCSecureWithin's first conjunct is that simulate s sends allowed contexts to allowed contexts. Under a resource instantiation that reads "the simulator is efficient".

Deliberately excluded: any cost, probability, or machine content. SubTheory is the OpenTheory-level sibling of PFunctor.StepClass — a bundled predicate plus its closure proofs, passed explicitly, with mixins for optional structure and an order along which results transport — and the two are meant to meet later at an instantiation of mem in terms of realizability, not to share code. Nothing here depends on PolyFun/Realizability/.

Two design notes that cost iterations and are recorded in the source:

• SubTheory.generated takes its generator predicate's boundary explicitly. A predicate whose leading argument is implicit has its implicits inserted eagerly when passed as an argument, leaving the boundary as an unsolvable metavariable at every use site. mem escapes this only because it is a projection applied to a known SubTheory.
• atomSubTheory needs no reasoning about the Expr quotient. A predicate defined by recursion on Raw would have to be shown invariant under all of Raw.Equiv; generated is defined by the operations of the theory, which act on the quotient already.

Validation

./scripts/validate.sh --lint --test

green (lake build --wfail, check-modules.sh, check-imports.sh, check-docs-integrity.py, lake lint, lake test). No sorry, no disabled linters.

No-regression evidence:

• git diff --stat against this PR's base touches no existing .lean file — only AGENTS.md, the two wiki pages, the generated PolyFun.lean, and four new files. Emulates.lean is untouched.
• emulatesWithin_top_iff / ucSecureWithin_top_iff are the machine-checked form of "this is a conservative extension", and the test file carries a canary that Emulates.par_compose still reaches Expr.theory by synthesis alone.
• The relativized plug_compose is exercised on the process-backed openTheory, which reaches it through Observation.IsSchedulingInsensitive rather than any strict factorization.

Axiom footprints: SubTheory.generated_le, EmulatesWithin.plug_compose, emulatesWithin_top_iff, and ucSecureWithin_top_iff are axiom-free; EmulatesWithin.par_compose, wire_compose, and mem_interpret_of_atoms are within [propext, Classical.choice, Quot.sound].

Downstream: VCVio imports PolyFun.Interaction.UC.Emulates but never uses Emulates or Observation — it re-derives the suite in Computational.lean — so this cannot break it, despite the import suggesting otherwise.

Stacked on #121; retarget to main once that merges so the full CI matrix runs (PRs not based on main only get 3 checks).

🤖 Generated with Claude Code