Context
The model isolates finite work that can adaptively inspect earlier records. A later query may depend on values returned by earlier queries, so replay support must record the executed dependency trace rather than a static graph alone.
Definitions
- Source cells range independently over a finite product of coordinate domains.
- Derived cells are well-founded and pure: they may query only source cells and earlier derived cells.
- An ordered query transcript records cell identifiers in execution order, with repetitions; its support is the set of queried cells.
- Replay support begins at the observer's actual queries and follows recorded dependencies backward.
Proof or evidence
The public note gives the exact oracle model and least-closure definition. The finite checker enumerates every two-source, two-derived-cell program and observer in its declared adaptive branch model.
Verification notes
The definition was checked for well-foundedness, termination, purity, adaptive query order, source-product scope, and the distinction between trace support and semantic dependence.
Limitations
- The model excludes side effects, cycles, nondeterminism, and nontermination.
- It is an execution-specific model, not a uniform finite-memory bound.
- The definition makes no novelty claim over program slicing, provenance, or trace semantics.