Modern entity-component systems (ECS) runtimes expose structural events (\texttt{OnAdd}, \texttt{OnSet}, and \texttt{OnRemove}), change filters,
and continuous queries (CQ) so that systems rerun only where data changed;
yet the correctness of the underlying optimizations—coalescing notifications,
reordering write-disjoint updates within a commit window, caching CQ membership, iterating to quiescence—has lacked
a semantics that states the required \emph{commit-window observation contract}.

We present \emph{RxTCoreECS}, a calculus that formalizes this contract for reactive ECS
by integrating a Core-ECS store-and-scan baseline with a reactive transactional layer. Its key design point is an explicit two-tier notification model:
(i) an \emph{eventful} commit that emits a sequential per-operation trace, and
(ii) a \emph{net-effect} commit that emits a per-cell delta (at most one event per cell per commit window).
The target contract is intentionally windowed: observers are
order-insensitive within a commit window, and \texttt{Changed} is a dirty-by-write post-membership filter rather than a semantic-equality test.
We define a window-local observational equivalence, relative to the incoming queue prefix, that quotients event order only within one commit window, prove schedule independence under write-disjointness,
and connect the two layers by a
coalescing refinement and a forward simulation theorem.
We add a CQ-cache model with correctness lemmas for \texttt{Added/Removed/Changed} deltas, an explicit version/filter alignment theorem exposing the once-per-window bump policy for touched entities and cells, and a fuel-bounded
quiescence loop. We prove a
reusable all-dirty scan-closure schema under explicit round-refinement and stability obligations.
All formal definitions and named results in the paper are mechanized and checked in Rocq.