Delta Type Concept

1 Changes and Incremental Strategies

Setting. Let $f:\X \to T$ , where $\X =\prod _{i=1}^n S_i$ , $n\ge 1$ , is a total product of nonempty sets. No algebraic structure is assumed. Write $x[i\leftarrow t]$ for replacement of $x_i$ by $t$ , and $x_J$ for a context subtuple. The empty product is a singleton. An incremental computation starts with a current input $x$ and its already computed output $v=f(x)$ . It receives a description of an input change and must produce the corresponding new output.

Why identify context? The central form is $\begin {equation} \label {eq:preview} \text {new output}=H(q,c)=A(q,P(c)). \end {equation}$ All inputs may already be accessible when a delta is consumed. A context declares which other input coordinates the selected consumer may consult. It therefore identifies work that can be separated from the changing query. Here $q$ contains the current output and the dynamic change data, including a baseline when required; $c$ is that context. Preparation $P(c)$ performs work depending only on that context. Application $A$ combines its result with the query at consumption. If the context stays fixed, the same preparation can serve changing queries. In an ordered batch, a preparation can also be used once and discarded before a later edit disturbs its context. These are the two reuse patterns proved below.

Definition 1 (Delta function and delta value). A delta function on a set $S$ is a map $\Phi :S\times P_\Phi \longrightarrow S.$ Each $p\in P_\Phi$ names the endomorphism $\delta _p=\Phi (\,\cdot \,,p):S\to S$ . A delta value $d=\langle \Phi ,p\rangle$ identifies the family and its member; write $d\ast s=\Phi (s,p)$ . At coordinate $i$ its input edit is $E_i^d(x)=x[i\leftarrow d\ast x_i].$ A bound packet $d_s$ retains a baseline $s$ , thereby determining the endpoints $(s,d\ast s)$ . An unbound reading supplies the transform without the baseline.

An endomorphism here is a self-map of a set. The family $\Delta ^\Phi =\{\delta _p:p\in P_\Phi \}$ need not be closed under composition. Different parameters may name the same map. Conversely, every family of self-maps is parameterized by its evaluation map.

Example 2 (Replacement and shift). On any set, $\Replace (s,t)=t$ . Its bound packet presents the substitution $s\to t$ ; its unbound reading is the constant self-map with value $t$ . On an abelian group, $\Shift (s,h)=s+h$ names a shift without supplying its baseline. The same delta function can be read bound or unbound when the appropriate consumer exists.

What the delta carries. A delta value is an abstract carrier for an incremental strategy: its family and member describe the input edit and may select a specialized evaluator. The consumer’s coordinate, reading, and context specify its consumption contract. The endpoint need not be materialized before consumption. A delta need not be an additive difference or a small object. Exactness comes from the consumer equation, and reusable work from its factorization as in (1).

Relation to the prerequisites. We use Transition Context, Transform Context, and Contextual Order from Prerequisite Mathematical Definitions, restating the needed conditions. This document develops their mathematical application to incremental computation; concrete Delta Type Classes form the subsequent implementation layer.

2 Exact Consumption at a Context

Jointly reachable data. Fix a coordinate $i$ , delta function $\Phi$ , and context $J\subseteq \{1,\ldots ,n\}\setminus \{i\}$ . Put $C_J=\prod _{j\in J}S_j$ . For a state $x$ and a delta $d=\langle \Phi ,p\rangle$ , the dynamic queries are $q^b(x,d)=(f(x),x_i,d\ast x_i),\qquad q^u(x,d)=(f(x),d).$ For either reading, let $\D =\{(q(x,d),x_J):x\in \X ,\ p\in P_\Phi \}.$ Thus the current output, baseline when present, and context come from one state. The bound query records the endpoints presented by the packet.

Definition 3 (Exact consumer and admission). An exact consumer is a map $H:\D \to T$ satisfying $\begin {equation} \label {eq:exact} H(q(x,d),x_J)=f(E_i^d x) \qquad (x\in \X ,\ p\in P_\Phi ). \end {equation}$ The family is admitted at $i$ on $J$ in the chosen reading when such a map exists. Admission covers every member of the family.

The associated output maps. Define $\F _i(s,c)=\{f(x):x_i=s,\ x_J=c\},\qquad \R _J(c)=\{f(x):x_J=c\}.$ For a presented pair $(s,t)$ , a bound consumer determines $U^b_{i,J}[s,t;c]:\F _i(s,c)\longrightarrow \F _i(t,c), \qquad v\longmapsto H((v,s,t),c).$ An unbound consumer determines $U^u_{i,J}[d;c]:\R _J(c)\longrightarrow \R _J(c), \qquad v\longmapsto H((v,d),c).$ The target sets follow from (2). A bound map is generally partial on $T$ ; the unbound map is an endomorphism of its slice range. These are their declared domains throughout.

Proposition 4 (Determinacy and exact consumption). Bound admission is equivalent to the implication $\begin {equation} \label {eq:determinacy} \left . \begin {gathered} f(x)=f(y),\quad x_i=y_i,\quad x_J=y_J \end {gathered}\right \} \Longrightarrow f(E_i^d x)=f(E_i^d y) \end {equation}$ for all $x, y$ and all $d=\langle \Phi ,p\rangle$ . Unbound admission is equivalent to the same condition with $x_i=y_i$ omitted. Every admitted consumer is unique on its declared domain.

Proof. An admitted consumer receives equal queries and contexts under the stated hypotheses, so (2) gives equal edited outputs. Conversely, in the bound case, take a realizable $(v,s,t,c)$ and choose $x$ with $f(x)=v$ , $x_i=s$ , and $x_J=c$ . A parameter presenting $(s,t)$ exists by realizability. Assign the answer $f(x[i\leftarrow t])$ . Condition (3), applied to that parameter, makes the answer independent of the chosen $x$ . It depends only on the endpoints, so a second parameter presenting them gives the same answer. This defines $H$ and proves exactness. In the unbound case, for realizable $(v,d,c)$ choose $x$ with $f(x)=v$ and $x_J=c$ , and assign $f(E_i^d x)$ . The criterion without the baseline hypothesis makes this independent of the witness. In either reading every domain point has a realization, and (2) forces the assigned answer, proving uniqueness. □

Endpoints and family. A bound family’s parameters may select a particular evaluation strategy, but the exact map on each source fibre is forced by the presented endpoints. For $\Replace$ , all endpoints are presented: bound admission says exactly that $J$ is a sufficient transition context for $i$ . Unbound admission is the prerequisite’s transform-context condition for $\Delta ^\Phi$ . Empty context specializes each statement to independence. Enlarging the context preserves either condition, because agreement on a larger context implies agreement on the smaller one in Proposition 4.

3 Preparing and Reusing Context

Separating preparation from application. Suppress the fixed coordinate, family, and reading, and write the exact consumer as $H:\D \to T$ with $\D \subseteq Q\times C$ . A preparation $P:C\to M$ is sufficient for $H$ if an evaluator $A:\D _P\longrightarrow T,\qquad \D _P=\{(q,P(c)):(q,c)\in \D \}$ satisfies $\begin {equation} \label {eq:factor} A(q,P(c))=H(q,c)\qquad ((q,c)\in \D ). \end {equation}$ The prepared value can be retained while later invocations supply their current queries.

Theorem 5 (Exactly when a preparation suffices). A chosen $P:C\to M$ is sufficient if and only if $\begin {equation} \label {eq:summary} P(c)=P(c')\quad \Longrightarrow \quad H(q,c)=H(q,c') \end {equation}$ for every common realizable query $q$ , meaning $(q,c),(q,c')\in \D$ . The evaluator is then unique on $\D _P$ .

Proof. If (4) holds, the two queries with equal prepared values give identical arguments to $A$ , proving (5). Conversely, given $(q,m)\in \D _P$ , choose $c$ with $(q,c)\in \D$ and $P(c)=m$ , and define $A(q,m)=H(q,c)$ . Every other such witness is covered by (5), so the definition is independent of the choice. It satisfies (4), which also forces its value at every point of $\D _P$ . □

Retaining original context. If application reads $c$ as well as auxiliary work, use $P(c)=(c,\operatorname {aux}(c))$ . This models exactly the available information. The first component guarantees semantic sufficiency; the second may contain work that the selected evaluator reuses. Caching does not require discarding the context.

The packet can select the evaluator. Bound semantic queries record endpoints, but an implementation may evaluate directly from the family and its parameter. On jointly realizable bound packet data, a packet evaluator can satisfy $\begin {equation} \label {eq:packet} \mathcal A_\Phi (v,s,p,P(c)) = A((v,s,\Phi (s,p)),P(c)). \end {equation}$ This is an equality of results. It does not prescribe evaluating $\Phi (s,p)$ first. The family can identify a specialized strategy and work to prepare before the particular parameter arrives.

Exactness and computation. The factorization is a statement about mathematical maps. An executable strategy also supplies representations and algorithms for $P$ and $A$ . The work comparisons below concern those specified algorithms in an additive cost model. Semantic existence alone asserts no running-time improvement.

Example 6 (A prepared dictionary of input changes). Let $\mathbb F$ be a fixed finite field, let $d,m,h\ge 1$ , and fix a dictionary $u_1,\ldots ,u_h\in \mathbb F^d$ . Consider $f(x,B,r)=Bx+r,\qquad (x,B,r)\in \mathbb F^d\times \mathbb F^{m\times d}\times \mathbb F^m,$ with the delta family $\Phi (x,(k,\alpha ))=x+\alpha u_k,\qquad (k,\alpha )\in \{1,\ldots ,h\}\times \mathbb F .$ For changes to $x$ , the matrix $B$ is a sufficient transform context; the current value of $r$ need not be read by this consumer. Put $U=[u_1\ \cdots \ u_h],\qquad P(B)=BU=Z,$ and, writing the fixed family implicitly in its query, define $A((v,k,\alpha ),Z)=v+\alpha Z_{:,k}.$ For every input and parameter, $A((f(x,B,r),k,\alpha ),P(B)) =Bx+r+\alpha Bu_k =B(x+\alpha u_k)+r .$ This proves exactness and the asserted transform context. Preparation depends on the current context $B$ and the fixed family dictionary, but not on $x$ , $r$ , $k$ , or $\alpha$ . It can precede the arrival of the next delta value.

Repeated use. Hold $B$ fixed and start with $v_0=Bx^0+r$ . For any sequence $(k_j,\alpha _j)$ , set $x^j=x^{j-1}+\alpha _j u_{k_j},\qquad v_j=v_{j-1}+\alpha _j Z_{:,k_j}.$ If $v_{j-1}=Bx^{j-1}+r$ , substitution gives $v_j=Bx^j+r$ . The initial equality and induction therefore prove exactness at every step. Every update uses the same prepared matrix $Z$ .

An explicit work comparison. In an arithmetic work model, count one field addition or multiplication as one operation, using ordinary dense dot products and vector operations. Preparing $B U$ costs $p=mh(2d-1)$ operations. Each output application costs $2m$ , and updating the stored input $x$ costs $2d$ . For $\ell \ge 1$ updates, extend this arithmetic count by charging all additional retention and reuse work to $\kappa _\ell$ in the same units. After cancelling other common work, the same factored algorithm has costs $\begin {array}{@{}ll@{}} \text {prepare at every use:}& \ell mh(2d-1)+\ell (2m+2d),\\[2pt] \text {prepare once and retain:}& mh(2d-1)+\ell (2m+2d)+\kappa _\ell . \end {array}$ The saving is $(\ell -1)mh(2d-1)-\kappa _\ell$ . The retained object contains $m h$ field elements. These counts establish the saving for this chosen strategy; they make no optimality claim. The inputs can all remain accessible throughout. The benefit comes from reusing intermediate computation determined by the context.

Lemma 7 (Sequential exactness). Let $x^0,\ldots ,x^m$ be an input run, each step an admitted coordinate edit. Start with $v_0=f(x^0)$ . At step $r$ , apply its exact consumer to $v_{r-1}$ using the actual context and, when bound, the actual baseline and resulting endpoint. Then every invocation is defined and $v_r=f(x^r)$ . An exact factorization may be used at any step whose preparation equals $P(c)$ for that step’s actual context $c$ .

Proof. If $v_{r-1}=f(x^{r-1})$ , the supplied query and labels are jointly realized by the actual state and edit. Equation (2) therefore returns $f(x^r)$ . A factored invocation returns the same value by (4). The assumed equality at step zero and induction prove the assertion. No closure of the admitted families is used. □

Theorem 8 (Reuse while context is fixed). Fix a consumer with context $J$ and factorization (4). Consider any finite admitted input run in which $x^r_J=c$ throughout. Prepare $C=P(c)$ once. At every invocation of this consumer, use $C$ with the current query, including the actual baseline and endpoint when bound. Let any intervening edits use their own exact consumers with actual labels. Starting from $v_0=f(x^0)$ , the maintained output after every step is $f(x^r)$ , and $C=P(x^r_J)$ remains valid for every designated invocation.

Proof. The stored value is initially $P(c)$ . Every state has context $c$ by hypothesis, so this stored value remains $P(x^r_J)$ throughout the run. At a designated invocation, the baseline and endpoint, if required, are those of the actual edit; its current-output query therefore meets the factorization hypothesis of Lemma 7. The intervening invocations meet that lemma’s direct exactness hypothesis. It follows inductively that $v_r=f(x^r)$ after every step. Thus both the current output and the preparation remain correct at each designated use. □

Finite-run work. Suppose there are $m\ge 1$ designated uses. Let preparation cost $p$ , let application at use $r$ cost $b_r$ , and let retaining and obtaining the cache add $\ell _r$ . Assume these costs add, retention leaves the $b_r$ unchanged, and all other work is identical. For the same factored consumer, the costs are $\begin {aligned} \text {repeated preparation:}\quad &mp+\sum _{r=1}^{m}b_r,\\ \text {retained preparation:}\quad &p+\sum _{r=1}^{m}(b_r+\ell _r). \end {aligned}$ Both runs are exact by Theorem 8. Counting their preparations and subtracting gives saved work $(m-1)p-\sum _r\ell _r$ ; retention is cheaper exactly when this quantity is positive.

Corollary 9 (Maintaining preparation under a context edit). For $\gamma :C\to C$ , an exact map $M_\gamma :P(C)\to P(C)$ with $M_\gamma (P(c))=P(\gamma (c))$ exists if and only if $P(c)=P(c')\quad \Longrightarrow \quad P(\gamma (c))=P(\gamma (c'))\qquad (c,c'\in C).$

Proof. An exact map sends equal prepared values to equal new prepared values, proving necessity. Conversely, define $M_\gamma (m)=P(\gamma (c))$ using any $c$ with $P(c)=m$ . The condition makes the answer independent of the witness, with image in $P(C)$ , and proves the required equation. □

4 Temporary Caches and Contextual Order

Preparation before a batch. A cache may be needed only until one designated use. Later edits may then change its context after it has served the batch. We first record why several such preparations can be made together.

Lemma 10 (Independent preparation). Fix context values $c_1,\ldots ,c_m$ and deterministic, terminating algorithms for $P_1,\ldots ,P_m$ . Each algorithm reads only its fixed context value and uses private intermediate and result storage. Every completed interleaving preserving each algorithm’s instruction order produces $(P_1(c_1),\ldots ,P_m(c_m)).$ Thus the preparations may be evaluated independently, including in parallel. Their contexts may involve overlapping input coordinates.

Proof. For each algorithm, its input reads remain fixed and only its own instructions change its intermediate state. Induction on those instructions gives the same local state as in its isolated evaluation. It therefore produces $P_r(c_r)$ after its finite isolated instruction sequence. An interleaving executing all these sequences produces every component of the stated tuple, independently of their relative order. □

The ordered setting. Fix an initial tuple $a$ and a target $b$ . At each coordinate choose a globally sufficient transition context $J_i\subseteq \{i+1,\ldots ,n\}$ and an exact factorization $H_i((v,s,t),c)=A_i((v,s,t),P_i(c))$ for its bound replacement consumer. Prepare $C_i=P_i(a_{J_i})$ . Each cache is needed once in this batch, for the substitution $a_i\to b_i$ , then is no longer required.

Theorem 11 (Consumption before context disturbance). Set $x^k=(b_1,\ldots ,b_k,a_{k+1},\ldots ,a_n),\qquad v_0=f(a),$ and consume the prepared caches in increasing order: $\begin {equation} \label {eq:batch} v_k=A_k((v_{k-1},a_k,b_k),C_k),\qquad k=1,\ldots ,n. \end {equation}$ After step $k$ , the output is $v_k=f(x^k)$ and every pending $i>k$ has $x_i^k=a_i,\qquad x_{J_i}^k=a_{J_i},\qquad C_i=P_i(x_{J_i}^k).$ Every cache is thus consumed before its declared context changes, and $v_n=f(b)$ . Under the algorithmic hypotheses of Lemma 10, all preparations can be evaluated in parallel from the fixed context values at $a$ .

Proof. At $k=0$ , the stated invariant follows from initialization. Assume it holds after $k-1$ steps. Coordinate $k$ is still pending, so its actual baseline is $a_k$ , its actual context is $a_{J_k}$ , and $C_k$ is the preparation for that context. Its query in (7) uses the current output $f(x^{k-1})$ , hence is jointly realizable. Exactness gives $v_k=H_k((f(x^{k-1}),a_k,b_k),a_{J_k}) =f(x^{k-1}[k\leftarrow b_k])=f(x^k).$ For every still-pending $i>k$ , both $i$ and all $j\in J_i$ are larger than $k$ , so none has yet changed. Their values, and the preparation made from them, retain their original values. This proves the full invariant by induction. At $k=n$ , $x^n=b$ . The parallel preparation claim follows from Lemma 10 applied to the fixed subtuples of $a$ . □

The lifetime protected. The proof keeps each pending baseline and context at its original value, even while the earlier inputs and the output change. It imposes no continuing requirement on a cache after its designated use. In particular, the preparation work can precede the sequence of current-output applications even when each cache is used only once.

Example 12 (Three caches, used in order). Consider the scalar mechanism $f(s_1,s_2,s_3)=(s_1+s_2)s_2s_3^2, \qquad (s_1,s_2,s_3)\in \mathbb R\times \mathbb R_{>0}^2 .$ It has sufficient transition contexts $J_1=\{2,3\}$ , $J_2=\{3\}$ , and $J_3=\varnothing$ . The preparations and exact applications are $\begin {align*} P_1(c_2,c_3)&=c_2c_3^2, &A_1((v,s,t),k)&=v+(t-s)k,\\ P_2(c_3)&=c_3^2, &A_2((v,s,t),k)&=\frac {t}{s}v+t(t-s)k,\\ P_3(())&=*, &A_3((v,s,t),*)&=\left (\frac {t}{s}\right )^2v . \end {align*}$

For the first equation, replacing $s_1=s$ by $t$ adds $(t-s)s_2s_3^2$ . For the second, with $s_2=s$ , $\frac {t}{s}(s_1+s)s\,s_3^2+t(t-s)s_3^2 =(s_1+t)t\,s_3^2 .$ For the third, replacing $s_3=s$ by $t$ changes only its square factor. The positive domains make every denominator nonzero. These identities prove the global transition conditions and all three factorizations.

Take $a=(1,1,1),\qquad b=(2,2,3),\qquad C_1=P_1(1,1)=1,\quad C_2=P_2(1)=1,\quad C_3=* .$ The exact trace is $v_0=2$ , $v_1=3$ , $v_2=2\cdot 3+2=8$ , and $v_3=3^2\cdot 8=72$ . Each table row records a complete consume-and-replace step; its context column is measured at consumption.

Step	State after step	Output	Context at use	Pending caches
$0$	$(1,1,1)$	$2$	—	$C_1,C_2,C_3$
$1$	$(2,1,1)$	$3$	$(s_2,s_3)=(1,1)$	$C_2,C_3$
$2$	$(2,2,1)$	$8$	$s_3=1$	$C_3$
$3$	$(2,2,3)$	$72$	$()$	none

Updating $s_1$ consumes $C_1$ while both context coordinates still have their original values. Updating $s_2$ then changes that context: the current value of $P_1$ becomes $2$ , but $C_1$ has finished its job. That step uses $C_2$ while $s_3=1$ is still unchanged. Finally, updating $s_3$ changes the contexts of both earlier caches after both have been used. Its own cache has empty context. Direct evaluation gives $f(2,2,3)=72$ , as required.

Original and final contexts. Increasing order uses preparations from the original later-coordinate values. Decreasing order can instead use $P_i(b_{J_i})$ . Indeed, before step $i$ in decreasing order the tuple is $(a_1,\ldots ,a_i,b_{i+1},\ldots ,b_n)$ . Its active baseline is $a_i$ and its context is $b_{J_i}$ . Given its exact current output, the factored consumer therefore gives the output after replacing $a_i$ by $b_i$ . Starting from $f(a)$ , descending induction proves exactness through the final tuple $b$ . The temporary-cache theorem above uses the increasing order and preparations made at the original tuple.

The Precedence Graph

A fixed batch and chosen contexts. Now allow arbitrary chosen sufficient transition contexts $J_i$ . Fix $a, b$ , prepare at $a$ , and let $I=\{i:a_i\ne b_i\}$ . The batch contains one fixed genuine substitution $a_i\to b_i$ at each $i\in I$ , and no other mutations. A schedule is a permutation of complete steps: consume at the current output and replace that coordinate before the next step begins. Its directed graph has vertex set $I$ and edges $\begin {equation} \label {eq:edge} i\longrightarrow j\quad \Longleftrightarrow \quad j\in J_i\cap I. \end {equation}$ The edge means: consume $i$ before changing the context coordinate $j$ . A schedule is context-preserving if every original declared context remains unchanged until its designated use.

Theorem 13 (Exactly when original contexts can be preserved). The context-preserving schedules are precisely the topological orders of this graph. Such a schedule exists if and only if the graph is acyclic. With exact factorizations, its initial preparations compute $f(b)$ when applied to the current output.

Proof. Suppose the schedule preserves contexts and $i\to j$ . If $j$ preceded $i$ , the $j$ entry of $i$ ’s context would be $b_j\ne a_j$ at use. There is only one substitution at $j$ , so it could not have returned to $a_j$ . Thus $i$ precedes $j$ , and every edge is respected.

Conversely, in a topological order, every $j\in J_i\cap I$ lies after $i$ , so still equals $a_j$ when $i$ is consumed. Every $j\in J_i\setminus I$ remains fixed throughout. The context is therefore $a_{J_i}$ and its initial preparation is valid. Coordinate $i$ also still has baseline $a_i$ . Starting with $f(a)$ , Lemma 7 now gives the exact output at every step; the last tuple is $b$ .

A topological order cannot contain a directed cycle. Conversely, a nonempty finite acyclic graph has a vertex of indegree zero: otherwise following incoming edges would eventually repeat a vertex, giving a cycle. Remove such a vertex first and repeat on the remaining acyclic graph. The resulting list is a topological order. This proves the existence equivalence as well as the schedule characterization. □

Precedence graph with vertices 1, 2, and 3 and edges 1 to 2, 1 to 3, and 2 to 3. An edge i to j means that step i consumes its original-context preparation before step j replaces coordinate j.

The three-cache example has exactly these precedence edges: each arrow places a cache’s use before a later change to its context.

Corollary 14 (Contextual orderability). Call an order contextual when the full suffix after each coordinate is sufficient for its transitions, and the inputs contextually orderable when some permutation is contextual. They are contextually orderable if and only if one can choose a globally sufficient $J_i$ for every coordinate so that the graph $i\to j$ for $j\in J_i$ on all coordinates is acyclic.

Proof. For an acyclic choice, take a topological order. Each $J_i$ is contained in the suffix after $i$ , which is sufficient by upward closure. Thus the order is contextual. Conversely, from a contextual order choose its full suffixes as the $J_i$ . They are sufficient by definition, and every edge points forward, so the graph is acyclic. □

The corollary quantifies over a choice of sufficient contexts. The lifetime guarantee for a particular batch depends on its chosen declared contexts, whose graph must respect that batch’s uses.

5 Composing Exact Consumers

One coordinate at one context. The sequential lemma already proves exactness of arbitrary admitted runs. When a context stays fixed, the corresponding operators also satisfy the following typed laws.

Proposition 15 (Transition and transform composition). If $J$ is a sufficient transition context for $i$ , write $T_c[s,t]:\F _i(s,c)\to \F _i(t,c)$ for its replacement operator. Then $T_c[s,s]=\id _{\F _i(s,c)},\qquad T_c[t,u]\circ T_c[s,t]=T_c[s,u].$ Consequently $T_c[s,t]$ is a bijection with inverse $T_c[t,s]$ .

For an admitted unbound family at fixed $c$ , let $M_i\subseteq S_i^{S_i}$ be the monoid generated by its input transforms and $\id _{S_i}$ . The family’s output maps extend to an action of $M_i$ on $\R _J(c)$ : composition is preserved, and $\id _{S_i}$ induces $\id _{\R _J(c)}$ .

Proof. Take $v=f(x)\in \F _i(s,c)$ . Replacing $s$ by itself leaves $x$ unchanged. Replacing $s$ by $t$ gives $f(x[i\leftarrow t])\in \F _i(t,c)$ , and then replacing $t$ by $u$ gives $f(x[i\leftarrow u])$ . These are exactly the asserted identities at $v$ . Every source value has such a realization. Taking $u=s$ , then reversing $s, t$ , gives both inverse identities on their respective fibres.

For the unbound case, any finite word of admitted transforms, including the empty word, preserves the input context slice. Repeated exactness sends $f(x)$ to the value of $f$ after that word acts at coordinate $i$ . Two words naming the same input transform give the same resulting tuple for every $x$ , so give equal output maps on $\R _J(c)$ . Hence the output map depends only on the generated transform and respects composition. The empty word leaves every realizing tuple unchanged and induces the identity map. □

Distinct coordinates. Fix admitted edits $E_i,E_j$ at distinct coordinates $i\ne j$ , each a fixed member of its family. For a source $x$ , write $U_i^0,U_j^0$ for the consumers labeled at $x$ ; write $U_j^i$ for the $j$ consumer labeled at $E_i x$ , and $U_i^j$ for the $i$ consumer labeled at $E_j x$ . Labels include the actual context and, when bound, the actual endpoints. The edit itself remains fixed.

Proposition 16 (Commutation with refreshed labels). The two input edits commute on $\X$ . Their correctly labeled consumers satisfy $\begin {equation} \label {eq:refreshed} U_j^i U_i^0(f(x))=f(E_jE_i x) =f(E_iE_j x)=U_i^j U_j^0(f(x)). \end {equation}$ Both compositions are defined at $f(x)$ . If neither edit changes the other’s declared context tuple at $x$ , the refreshed labels equal the original labels.

Proof. Each fixed edit determines the new value from its own coordinate alone. Both composite tuples therefore have the same new $i$ and $j$ entries, with all other entries unchanged. Thus $E_jE_i=E_iE_j$ on the total product. Applying Lemma 7 in each order proves the outer equalities and definedness in (9). The other edit does not change a coordinate’s bound baseline, and hence does not change its endpoint under its fixed transform. If its context is also unchanged, every label is the original one. □

Proposition 17 (A common domain for frozen consumers). Suppose $j\notin J_i$ and $i\notin J_j$ . Fix compatible context labels $c_i,c_j$ and a baseline for each bound reading. Let $Z\subseteq \X$ be the joint source stratum defined by those context constraints and those bound baselines. For the originally labeled consumers $U_i,U_j$ , $\begin {equation} \label {eq:frozen} (U_j\circ U_i)|_{f(Z)}=(U_i\circ U_j)|_{f(Z)}, \end {equation}$ with both sides defined on $f(Z)$ . When both readings are unbound, $Z$ is an invariant joint context slice and the restricted consumers are commuting endomorphisms of $f(Z)$ .

Proof. For $v\in f(Z)$ choose a realizing $x\in Z$ . Each edit preserves the other’s context by the exclusions, and its baseline when bound because the coordinates differ. The labels in Proposition 16 therefore remain the original ones. That proposition gives definedness and equality at $v$ , proving (10). If both readings are unbound, $Z$ has only context constraints. Both edits preserve these, so $E_iZ,E_jZ\subseteq Z$ . Exactness gives $U_i(f(Z)),U_j(f(Z))\subseteq f(Z)$ , proving the endomorphism assertion. □

For bound partial maps, the two maximal composition domains in $T$ need not coincide; (10) states the equality on the joint compatible source range.

Example 18 (Commuting maps at stale contexts). Let $f(x,y,z)=xy+z$ on $\mathbb R^3$ . Unbound increments of $x$ and $y$ have respective contexts $y$ and $x$ , with exact consumers $U_x[h;y](v)=v+hy,\qquad U_y[k;x](v)=v+kx.$ Each relevant slice range is all of $\mathbb R$ , since $z$ is free. At $(1,1,0)$ , prepare increments $h=k=1$ from the original contexts. Both maps are $v\mapsto v+1$ , and they commute on $\mathbb R$ . Yet $U_y[1;1]U_x[1;1](1)=3, \qquad f(2,2,0)=4.$ After the $x$ edit, the actual context for the $y$ edit is $x=2$ . Refreshing it gives $1\ \xmapsto {\ U_x[1;1]\ }\ 2 \ \xmapsto {\ U_y[1;2]\ }\ 4.$ The stale consumer accepts the intermediate number $2$ , but describes a different context. Context correspondence is stronger than numerical domain acceptance, exactly as used in the composition proofs.

Example 19 (Composition is not addition of differences). Let $f(x,y)=2^{x+y}$ on $\mathbb Z^2$ . Incrementing either coordinate has empty transform context and induces the exact map $U(v)=2v$ on $\{2^k:k\in \mathbb Z\}$ . The two frozen consumers commute, and from $(0,0)$ their composition gives $U(U(1))=4=f(1,1)$ . Each separately evaluated initial difference is $U(1)-1=1$ , but adding both to the initial output gives $1+1+1=3$ . Thus even valid commuting consumers do not justify merging their initial output differences by addition.

Preparation and application. Independent preparation in Lemma 10 produces values for fixed context tuples. Consumption uses the current output and preparations matching the actual context at each invocation. Frozen labels suffice under Proposition 17; changing labels use Proposition 16. The results justify independent preparation and exact operator composition. Their elapsed-time costs depend on the specified evaluators and execution resources.