ch:dependent-partiality: fuel-bounded observation

Problem and result. Observe return, step, bind, subtraction gcd, and search using finite fuel. The invariant is that one unit of fuel performs at most one machine transition. The accepted cases return gcd two, find the first even number four from three, and report only later for a nonreturning search after twelve units.

Representation. The companion represents a partial computation by a first-order machine state and a one-step transition function. A host-language lazy stream would look closer to $A^{\nu }$, but its forcing behavior would be harder to audit and a strict host could hide multiple steps in one call. The machine makes fuel consumption and the residual state explicit.

First complete version. Implement Done and Continue, then define an observer by structural recursion on fuel. Zero fuel returns later; positive fuel returns a stored result or performs exactly one transition and recurses on the predecessor. This already checks the step-count invariant.

Remaining cases. Add bind by retaining every input step before entering the continuation. Add subtraction gcd next, whose unequal positive branches each expose one step. Add search last: even inputs finish and odd inputs advance once. A separate nonreturning state supplies the finite later fixture without being misclassified as a proof of divergence.

A failing version. At zero fuel return the successor state rather than the unchanged residual machine; the step-count oracle detects the free transition. Dropping a bind continuation and adding an early equality exit to Gcd separately fail the bind result and the chapter’s exact three-delay Gcd trace.

Acceptance test. Require the seven exact pass lines and empty audit recorded in subappendix E.9. Each recorded mutation must fail, and the restored source must preserve the residual machine, bind continuation, and printed Gcd transition count. The executable record in subappendix E.9 alone stores the accepted source identity and mutation replay.

Mathematical boundary. The observer illustrates finite instances of convergence and the guarded definition of bind. Running it does not prove lemma 105.5, theorem 105.8, theorem 105.9; in particular, later is not evidence of divergence.