ch:system-t-dialectica: a finite-type witness

Problem and invariant. Represent zero, successor, addition, and a natural recursor. Define evalRec structurally on the natural argument and eval structurally on terms. The accepted step adds predecessor plus one to the accumulator.

Mutation. The AddIndex step omits the successor. It remains well typed but calculates $0+0+1+2=3$ instead of six at input three.

Acceptance and boundary. Require four passes and an empty audit under the appendix E commands. This is a finite evaluator and mutation test, not a normalization or Dialectica soundness proof.