v0.5: proof-language step for fuel arithmetic under symbolic depth (nested-key equation theorems of SP-25) #249

Filed from #91 stage 4 (PR 5), as the maintainer asked.

Problem. SP-25 proves, by term_cases, that the declared RuntimeSemantics run of equal and compare in supportCrate equals the calculus primitive of the same name, for the core profile's scalars (bool, nat, int, the eight widths; Ordering for equal) and for pairs of two scalars. The calculus admits deeper pairs for compare (calculus/check.rs, orderable: Pair(orderable, orderable)), and for those the row has no equation theorem: each pair level spends a constant amount of rtRun fuel, so an induction over the depth needs arithmetic on that fuel under a symbolic depth (fuel = K + c*d, unified with Nat.succ at each unfolding), and the language-1.2 proof strategies (term_cases, cases, induction, simplify, linear_arithmetic) have no rewrite step that does it inside a simp only unfolding. Today the evidence for nested keys is the RB-17 differential over seeded keys of depth two and three (validation, never a proof).

Wanted (one of, as its own row with plants).

1. A Nat-arithmetic rewrite step for simplify/term_cases that normalizes K + c*(d+1) to Nat.succ (K + c*d + (c-1)) under the named definitions; or
2. a fuel-free (structurally recursive over the RuntimeSyntax expression) evaluator for RuntimeSyntax, so depth costs no fuel.

Plants: a fuel too small for one level (the theorem must be unprovable, never a false equation), a pair impl that returns the second component's order when the first ties wrongly, an induction step that drops a hypothesis.

Not v0.4. The proof language is closed on the v0.4 line; this is a language change for one proof shape.

Refs: #91, SP-25, RB-17.