ch:temporal-types: bounded reactive trace

Problem, algorithm, invariant, result, and acceptance. Compute a finite running-sum transducer and contrast one retained temporal root per step with a history-retaining countermodel. The causal invariant says output $i$ uses inputs only through $i$; the root invariant says the bounded machine retains one root after every transition. On input $(2,11,5)$, the required trace is $(2,13,18)$, bounded counts are $(1,1,1)$, and the mutant counts are $(1,2,3)$. Acceptance is the four named passes, completion line, and empty audit in appendix E.

Representation choice. A list supplies a finite input prefix. The causal transducer carries one natural accumulator. Separate root-count functions model the bounded and history-retaining machines. Lists make the expected trace readable but erase heap identities. An alternative explicit state-step record with now/later location sets would expose heap rotation, but would require freshness, reachability, and store-typing code that this finite oracle does not verify.

Minimal end-to-end version. Emit $accumulator+input$, recurse with that sum, and record root count one. On inputs $2,11,5$, require outputs $2,13,18$ and confirm that changing the third input cannot change either of the first two outputs.

Remaining cases, in metatheory order. First test the causal prefix property, then the bounded-root invariant, then the history-retaining countermodel. Add the requested two-state transducer last, with a named input and complete expected output trace; it must retain its finite stable state without increasing the temporal-root count.

Incorrect input. Use the retained-history count in the bounded oracle. It exceeds one after the first step while the trace still computes.

Run and theorem boundary. Execute the four commands for this artifact in appendix E and require the exact named transcript and audit []. Activate the history mutation, observe the root oracle fail, restore, and replay. Simply RaTT’s Fundamental Property is a world-indexed proof from which productivity, causality, and the machine garbage-collection result follow. The finite list program is not the abstract machine or logical relation and does not prove any of those theorems.