ch:coinduction: ch:coinduction

Problem and result. Implement finite observation of a stream state machine in Kappa. The result prints the first ten Fibonacci values, confirms that depth nine takes nine state transitions, and rejects a mutated transition whose first two values are $0,0$.

Representation. Represent the infinite stream by a finite pair state and a transition function; represent an observation request by a natural depth. This mirrors the chapter’s corecursor and makes each consumed tail explicit. Storing a long finite list is simpler for one test but cannot express arbitrary finite observation or expose the transition invariant.

First complete version. Implement one Fibonacci transition $(a,b)\mapsto (b,a+b)$ and an observer that recurses structurally on depth, returning $a$ at zero. Check the zero and successor cases before collecting the ten named observations.

Remaining cases. Add a transition counter to verify the depth-nine request. Add the complete ten-value oracle $0,1,1,2,3,5,8,13,21,34$, then isolate the transition as an argument so the mutation can be run by the same observer.

A failing version. Use the mutation $(a,b)\mapsto (a,a+b)$. Its second observation is $0$ rather than $1$; the corpus names the bad prefix $0,0$ and requires its rejection.

Acceptance test. Run the four commands in appendix E. Require the four exact observation and verdict lines, the final four-case summary, and an empty audit.

Mathematical boundary. The finite run checks the displayed observation equations. It does not prove the productivity theorem, coinduction, bisimulation soundness, or completeness of guardedness checking.