Requirements for an Enter-specific theorem

A formal application would require:

1. full configuration and event-occurrence definitions;

2. a residual theorem validating swaps without collapsing occurrences;

3. a precise intervention and observation semantics;

4. a sensitivity–reachability or routing theorem;

5. a compositional probabilistic diamond;

6. an ownership theorem for simultaneously enabled operations;

7. the representation data $\mathsf{Aff}$, including its completion and faithfulness claims;

8. a sound implementation of causal-origin typing and transport;

9. record-preserving symmetry constructions supporting $\mathsf{S}$, its homogeneous strictly convex weakening, or $\mathsf{B}$, together with a proof that the polyhedral embeddings are not equivariant realizations of those symmetries.

For a discrete calculus, the final item may require a completion or limit of families of experiments. It must not impose a transitive continuous event action incompatible with past-finiteness.