diff --git a/manual/algorithms-and-memory/algorithm-endpoints.md b/manual/algorithms-and-memory/algorithm-endpoints.md
index cd75d4fd37..2e2010a85f 100644
--- a/manual/algorithms-and-memory/algorithm-endpoints.md
+++ b/manual/algorithms-and-memory/algorithm-endpoints.md
@@ -138,7 +138,7 @@ The first fast branch is now at `n = 2^2394`; the old 1296-bit family and its `m
 `g=4^b`, `L=19m` bounds are removed. Inputs between the old and new branch thresholds now use
 the actual exhaustive branch. Recheck finite `timeBound` and geometry/admission premises with
 the current declarations rather than reusing the old finite constants.
-The [parameter client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMExactTriangleDyadicParameters.lean)
+The [parameter client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMExactTriangleDyadicParameters.lean)
 evaluates actual code at zero, just below the new threshold and at the threshold. The headline
 1.9992 exponent, distinct-position meaning and native resource guarantees below are unchanged.
 
@@ -147,7 +147,7 @@ evaluates actual code at zero, just below the new threshold and at the threshold
 To decide whether three signed integer matrices contain a zero-weight triangle, import
 `Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime` and use
 `FixedPrime.runs_input`. The complete
-[initialized client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMExactTriangleBoxFixedPrime.lean)
+[initialized client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMExactTriangleBoxFixedPrime.lean)
 includes imports, admission proofs, successful witness recovery and negative exhaustion.
 Use the client on the canonical pipeline revision before adapting it.
 
@@ -185,7 +185,7 @@ Import `Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime`. For an
 call, use `CallableFixedPrime.runs_input` with the same `PreparationInput.input` layout and
 geometry/prime premises above, and physical width at least
 `CallableFixedPrime.inputWidth n (D m) g p values`. The complete
-[initialized client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMCallableBoxFixedPrime.lean)
+[initialized client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMCallableBoxFixedPrime.lean)
 checks successful original-coordinate recovery, a same-execution finite charge and negative
 exhaustion. Fourteen executed header/pointer instructions precede the actual caller program;
 input placement itself follows the `State.init` convention above.
@@ -201,7 +201,7 @@ Raw verdict, witness and scans return in 632–636.
 The fixed 640-register program preserves the low 160 selector bank, all eight original argument
 registers and memory outside its stated window. It copies and sums only the original arrays,
 computes its own virtual width, and executes the real box controller in reused dirty memory.
-The [dirty caller client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMCallableBoxFixedPrimeCaller.lean)
+The [dirty caller client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMCallableBoxFixedPrimeCaller.lean)
 checks aliased spans, nonzero selector registers and dirty words above the virtual modulus.
 
 At `m=9k`, `CallableFixedPrime.timeBound_le` charges the actual copy/setup/return and final
@@ -222,7 +222,7 @@ geometry and selected prime and calls this actual controller. Its register names
 Import `Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting` and open
 `Cslib.Algorithms.WordRAM.ExactTriangle`. Use `ParameterSelecting.runs_input_uniform` for a
 complete initialized decision. The
-[checked client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMParameterSelectingInput.lean)
+[checked client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMParameterSelectingInput.lean)
 gives full imports, admitted positive/negative signed cases, empty input, and a symbolic fast
 family with the actual selected-prime conclusion. From a checkout containing this endpoint:
 
@@ -268,7 +268,7 @@ enormous interpreter benchmark.
 Import `Complexity.Algorithms.WordRAM.ThreeSum.Decision.Subquadratic`. In namespace
 `Cslib.Algorithms.WordRAM.ThreeSum.Decision`, apply `exists_subquadratic_runs κ` to the actual
 ordinary host with `ParameterSelecting.callee`. The complete
-[checked client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMSubquadraticThreeSum.lean)
+[checked client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMSubquadraticThreeSum.lean)
 includes imports, positive repeated-zero inputs, negative all-one/all-minus-one inputs, and
 rejection of two zeros because the positions must be distinct. From an endpoint checkout:
 
@@ -302,18 +302,40 @@ by the 1.9992 theorem below; there is no separate conservative solver implementa
 ## Ordinary integer 3SUM in time n^1.9992
 
 Import `Complexity.Algorithms.WordRAM.ThreeSum.Decision.One9992`. In namespace
-`Cslib.Algorithms.WordRAM.ThreeSum.Decision`, `boxProgram κ` is computable structured code
-and `boxFlatProgram κ` is its assembled standard Word-RAM program with 848 registers.
-Apply `exists_one9992_runs κ`; no solver, time law, selected prime or layout certificate is
-an argument. The complete
-[checked client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/ThreeSumOne9992.lean)
-shows positive and negative inputs, repeated values at distinct positions, the charged halt,
-and the same-state prehalt prefix. On that source revision, run:
+`Cslib.Algorithms.WordRAM.ThreeSum.Decision`, apply `uniformDecidableInO_one9992 κ` for the
+compact complexity statement in the existing Word-RAM time API. `Admissible κ input W`
+bundles the magnitude and width conditions below; `Admissible.inputFits` proves that every
+admitted pair meets the API's separate input-fit requirement.
+The natural-valued time scale is the ceiling of `n^(2499/1250)`; this ceiling is proof
+metadata and is not evaluated by the machine.
+
+For a particular program, `boxProgram κ` is computable structured code and `boxFlatProgram κ`
+is its assembled standard Word-RAM program with 848 registers.
+`boxFlatProgram_decidesInTime κ` gives its exact `Decision.cost` allowance at every length.
+Use `exists_one9992_runs κ` when you also need the final native state, same-state prehalt
+prefix or polynomial bounds on every prefix. None of these interfaces asks for a solver,
+time law, selected prime or layout certificate. The complete
+[checked client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/ThreeSumOne9992.lean)
+shows the semantic interfaces, positive and negative inputs, repeated values at distinct
+positions, rejection of an inadmissible magnitude, the charged halt and the same-state
+prehalt prefix. On that source revision, run:
 
 ```bash
 scripts/build.sh --wfail --iofail ComplexityTests.ThreeSumOne9992
 ```
 
+The native constructor `Decision.program κ solver` accepts only the finite callee code;
+`Decision.flatProgram` assembles its halt. The canonical solver argument is
+`ParameterSelecting.program`. Correctness and time certificates refer to that same syntax,
+so evaluating it does not require evaluating proof-only resource metadata. There is no
+separate `Decision.Code` import or duplicate `programOfCode` assembly.
+
+For the preprocessing proof, import `Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing`
+for initialized execution, readback, width and resources. Import its `PreprocessingExecute`
+companion to use `Preprocessing.afterFrontend_exec` for the suffix after the frontend, in
+namespace `Cslib.Algorithms.WordRAM.ThreeSum.ChanHe`. The setup and iteration companions
+contain private stage proofs; callers need no snapshot, cursor or individual-stage contracts.
+
 Choose a fixed natural magnitude exponent `κ` and an original `input : List ℤ`. Set
 `n = input.length`, prove every `|z| <= (n+2)^κ`, and supply physical width
 `Decision.width κ 123357 n <= W`. The initial state is
@@ -332,12 +354,24 @@ wider width has the same guarantees. Every reachable prefix has register and mem
 below `(n+2)^(2 * Decision.widthCoefficient κ 123357)` and memory zero at addresses at least
 that envelope; the final data also satisfy the physical word bound.
 
-The [actual automatic callee](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Callee.lean)
-executes parameter computation, prime selection and the real box-backed calls. Its canonical integer family is
-`b = floor(log2(n)/2394)`, `m = 63b`, `g = 4^(2b)`, `D = 4^m` and `L = 21m`.
-The [parameter boundary client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMExactTriangleDyadicParameters.lean)
+The caller places matrix workspace at the final preprocessing heap frontier `H`, copied by an
+executed register instruction. The preprocessing
+[output-layout contract](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/TraversalOutput.lean)
+places the pointer-table endpoint and every live payload endpoint at or below `H`.
+Each solver call preserves memory below `H` on return, so the caller can still read every
+remaining instance. The separately computed polynomial envelope bounds signed values and
+arithmetic width; it no longer determines the workspace address.
+Preprocessing may have touched dead temporary scratch above `H`, which the solver can reuse.
+This layout contract describes live output and a final-state frame, without asserting a ban
+on transient callee writes. The existing polynomial prefix bounds still apply.
+
+The [actual automatic callee](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Callee.lean)
+executes parameter computation, prime selection and the real box-backed calls. Its integer
+parameters and the reason for their constants are explained below; the parameter `n` there
+is the ET dimension, rather than the original 3SUM length.
+The [parameter boundary client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMExactTriangleDyadicParameters.lean)
 checks the actual VM at zero, below `2^2394` and at `2^2394`;
-the [automatic Exact Triangle client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMParameterSelectingInput.lean)
+the [automatic Exact Triangle client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMParameterSelectingInput.lean)
 checks symbolic fast-family executions, including the selected-prime conclusion. These huge
 matrix clients are proof witnesses, not execution benchmarks. Small ordinary-input VM checks
 also reject lengths below three. The complete finite ledger charges preprocessing, selector,
@@ -346,13 +380,39 @@ halt. Polynomial logarithmic factors are absorbed before the ordinary reduction
 
 The intermediate native Exact Triangle bound is `Oκ(n^(3-33/20000)) = Oκ(n^2.99835)`;
 this does not claim the source Exact Triangle exponent 2.9983. The final
-[ordinary theorem and source mapping](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/Complexity/Algorithms/WordRAM/ThreeSum/Decision/One9992.lean)
+[ordinary theorem and source mapping](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/WordRAM/ThreeSum/Decision/One9992.lean)
 adapt the 1.9992 target to this library's standard unsigned Word-RAM with canonical signed
 encoding and polynomially bounded integers. Time counts unit native instructions with
 logarithmic admitted word width. This is not a bit-time or arbitrary-real 3SUM theorem;
 the source's separate signed modular machine and `SolvedInTime` predicate are not imported.
 
-## Reusing the ordinary runtime transfer
+## Following and reusing the runtime bound
+
+The exponent comes from the dimension of each ET call and the number of charged calls.
+For original 3SUM length `n`, write `ell = floor(log2(n+2))+1`,
+`q = Decision.instanceBound κ n` and `s = Host.sideLength (Decision.instanceLength κ n)`.
+The fixed magnitude exponent `κ` may affect constants. The finite account is:
+
+| Quantity | Bound before absorbing logarithms | Checked statement |
+|---|---|---|
+| Native preprocessing `Pκ(n)` | `Kκ*(n+2)*(sqrt(n+2)+1)*ell^13` | `Preprocessing.cost_bound` |
+| Catalogue allowance `q` | `128*(κ+2)^2*ell^7` | `Decision.instanceBound_le_numBound` |
+| ET side `s` | `Oκ(sqrt(n)*ell^2)` | `ChanHe.packed_side_le` |
+| One Convolution call, including outer control | `2*s*T(s,F)+355*s^3` | `Decision.callerTime_add_twelve_le` |
+
+The [runtime module](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/WordRAM/ThreeSum/Decision/Runtime.lean)
+connects these statements to the actual `Decision.cost`:
+`Pκ(n) + 4*E + 32 + q*(Host.callerTime(...)+12)`, where
+`E = Decision.envelopeExponent κ`. The fixed reserve includes setup and halt; the caller
+term includes matrix construction and every ET invocation. The passed magnitude is
+`F = 2*(n+2)^E+1`. `ChanHe.packed_weight_le` bounds it by `(s+2)^(2*E+2)`, so an ET theorem
+for polynomial weights applies at the actual side `s`.
+
+If `T(s,F) = O(s^(3-δ))`, the solver term becomes `O(q*s^(4-δ))`.
+Substitution produces the power `n^(2-δ/2)` with a fixed logarithmic factor.
+Only then does the proof absorb logarithms: it establishes every
+`a > 2-δ/2`, for `0 < δ <= 1`. It does not establish the boundary exponent with those
+factors removed. This also explains why the entire preprocessing cost must be retained.
 
 For a different actual certified ET implementation, import
 `Complexity.Algorithms.WordRAM.ThreeSum.Decision.Runtime`. In the `Decision` namespace,
@@ -372,8 +432,8 @@ input magnitude and physical-width premises described above.
 
 The canonical callee uses `δ = 33/20000`. Both `a = 2499/1250` and the older conservative target
 `a = 2-1/5184` satisfy the strict inequality, so both endpoint proofs reuse this same transfer
-and concrete solver. The [ordinary client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/ThreeSumOne9992.lean)
-and [conservative client](https://github.com/cslib-community/complexitylib/blob/07310e3d595de26f1770123ce2e6c66bff0ab468/ComplexityTests/WordRAMSubquadraticThreeSum.lean)
+and concrete solver. The [ordinary client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/ThreeSumOne9992.lean)
+and [conservative client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMSubquadraticThreeSum.lean)
 check the resulting concrete run/resource contracts. From a checkout containing this revision:
 
 ```bash
@@ -385,6 +445,42 @@ the integer parameter tuning, shared native representation and cost composition
 native adaptations. The generic transfer changes proof reuse, not the computational model or
 the 1.9992 theorem's scope.
 
+### Why these integer parameters work
+
+Here `n` denotes the ET dimension. The parameters put all components on the common scale
+`n^3/g`. Read the feasibility and balance conditions before the chosen values:
+
+| Condition | What it pays for |
+|---|---|
+| `D^18 <= n` | Box-backend geometry |
+| `D*g^2 <= n` | Preparation `n^2*D*g <= n^3/g` |
+| `g^2 <= sqrt(D)` | Query control |
+| `g^2 <= D^(8/125)` | Product work `n^3*g*D^(-8/125) <= n^3/g` |
+
+The [parameter family](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/ExactTriangle/ParameterChoice.lean)
+chooses `g=4^(2b)`, `m=63b`, `D=4^m`, and the existing box tensor depth `L=21m`.
+The product balance is the small integer inequality `4*125 <= 63*8`, or `500 <= 504`;
+`63b` also satisfies the box tradeoff's divisibility by nine.
+The stronger reserve `D^19 <= n` requires `2394*b <= floor(log2(n))`, because
+`2394 = 2*63*19`. This gives `b=floor(log2(n)/2394)`.
+The [cost-geometry lemmas](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/ExactTriangle/ParameterChoice/CostGeometry.lean)
+prove the conditions and `n^3/g <= 16*n^(3-2/1197)`, retaining integer rounding.
+
+The raw saving `2/1197` is not yet a full runtime exponent. The
+[finite coefficient](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/WordRAM/ExactTriangle/DyadicCost/Asymptotics.lean)
+retains the product factor `(21m+1)^2*(m+1)`, a linear logarithmic parameter term and the
+global selected-prime scan term proportional to the weight exponent times `log(n)`.
+It is bounded by a constant times `(floor(log2(n))+1)^3`. Absorbing this full coefficient,
+and charging callable setup and dispatch, gives the ET saving `δ=33/20000`.
+The ordinary transfer then allows any exponent above `2-δ/2`, which is 1.999175;
+the target 1.9992 leaves a further gap of `1/40000` for its logarithmic factors.
+
+`ParameterChoice.blocks_pos_iff` proves the exact ET fast cutoff `n >= 2^2394`.
+The executable selector chooses exhaustive solving below it. This cutoff follows from
+the proved integer family; it is not a measured crossover, an optimized cutoff, or a claim
+about practical performance. The asymptotic threshold can be larger still, and the
+existential false-positive constant in the proof does not supply a numerical benchmark.
+
 ## Tree Evaluation
 
 The [Cook–Mertz endpoint](catalytic-and-tree-evaluation.md) computes the root of an explicitly table-encoded perfect binary tree in native independent workspace `O(log n · log log n)` for positive value length and height. The output is not charged to workspace, and the theorem leaves time existential. The same page distinguishes borrowed-register restoration and fan-in/packed procedure variants.
diff --git a/manual/algorithms-and-memory/memory-specifications.md b/manual/algorithms-and-memory/memory-specifications.md
index e7f21ffaeb..ecb71f8607 100644
--- a/manual/algorithms-and-memory/memory-specifications.md
+++ b/manual/algorithms-and-memory/memory-specifications.md
@@ -88,6 +88,60 @@ This client is a header-read demonstration, not a Dijkstra execution or shortest
 
 ## Footprints, traces, and memory windows
 
+### Call fixed code in a disjoint register bank
+
+Import `Complexity.Computability.WordRAM.Call` when the callee already has a native execution
+proof and the caller must prepare arguments and consume the result. `ExecWithin.call` takes
+an injective register embedding, a charged preparation, the callee's execution and
+postcondition, and a charged continuation. The continuation sees the callee postcondition
+on its register bank and equality of every register outside that bank. Memory assertions
+refer to the actual returned memory. The total allowance is `tPrep+tCall+tCont`; register
+renaming emits no instructions.
+
+The complete [fixed-call client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMCall.lean)
+delivers an argument, calls a routine that increments it and writes memory, then retrieves the
+result in five charged instructions. It proves that an unrelated register and other memory
+cells survive, even when unused old words exceed the physical word bound. This rule does not
+add a whole-state boundedness or finite-footprint premise to the supplied callee theorem.
+If a call proof fails, check the embedding's injectivity, the callee's actual preconditions,
+and the registers the continuation needs to preserve. A memory frame belongs in the callee's
+postcondition; register disjointness alone says nothing about its writes.
+
+From a checkout containing this API, check the client with
+`scripts/build.sh --wfail --iofail ComplexityTests.WordRAMCall`.
+The [ordinary 3SUM call proof](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/Complexity/Algorithms/WordRAM/ThreeSum/Decision/Body.lean)
+uses the same rule for its Convolution host and retained controller registers.
+For a renamed execution without a surrounding preparation and continuation, use
+`Exec.rename_post` or `ExecWithin.rename_post`. They return the postcondition on the callee
+bank and the unchanged outside registers; the first retains an exact instruction count.
+
+### Transfer a fixed record through a native stack
+
+Import `Complexity.Algorithms.WordRAM.Stack.Record` and open `Cslib.WordRAM`.
+`Stack.pushRecord` and `Stack.popRecord` use the existing nine-register bounded stack
+dispatcher. Supply its injective embedding, a disjoint record bank and a register for the
+terminal self-copy. Prove `Stack.Rep`, the capacity/address fit and `Fits w 2`; pushing also
+needs room and fitting source values. Popping needs distinct destination registers and the
+record at the live stack top. Repeated source registers are allowed when pushing.
+
+`Stack.pushRecord_exec` puts `List.ofFn` of the source words at the top in forward order
+and costs exactly `9*n+1` instructions. `Stack.popRecord_exec` restores that order in exactly
+`14*n+1` instructions. Both counts include argument delivery and exclude a final program
+halt. A zero-length transfer is one self-copy. Memory outside the reserved stack and registers
+outside the relevant banks are preserved; unused stack cells can be dirty and popped cells
+are not cleared.
+
+The [record client](https://github.com/cslib-community/complexitylib/blob/4b571e0f55c64471a95728d28955f3532ed9329f/ComplexityTests/WordRAMStackRecord.lean)
+pushes two words and pops them into a different bank, checking their order, a live tail and
+outside sentinels. Its interpreter checks include the charged halt and insufficient fuel.
+Run `scripts/build.sh --wfail --iofail ComplexityTests.WordRAMStackRecord` from the API checkout.
+For capacity failures, check `n+vs.length <= capacity`; for register-frame failures, check
+disjointness from the dispatcher and injectivity of the pop destination bank.
+The Chan–He traversal specializes this API to its seven-word record, retaining its exact
+64-instruction push and 99-instruction pop.
+
+### Use an explicit memory frame
+
 [HeapAssertion](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Heap.lean#L62) records a finite support and a predicate on total memory. Separating conjunction uses disjoint supports; `Modifies` records agreement outside an allowed write set. This is an explicit-footprint frame calculus inspired by separation logic, not a replacement semantics in which inaccessible cells disappear [reynolds02][reynolds02].
 
 [Complexity/Computability/WordRAM/Trace.lean](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Trace.lean) decorates actual executions with address/value reads and writes. `TraceExec.exec` erases the trace; `Exec.exists_trace` supplies one for every ordinary execution; trace length is bounded by instructions. These are access costs of a fixed RAM computation. They are not a general cell-probe model allowing arbitrary uncharged local computation.