ch:quantitative-dependent-types: demand calculation

Problem and invariant. Compute ambient demand plus binder-scaled argument demand while retaining the declaration spine.

Two representations. Length-indexed vectors make spine preservation intrinsic. The companion uses named two-declaration spines together with naturals and the zero–one–many semiring, which makes spine mismatches observable.

First complete version. Implement addition, multiplication, named-context scaling, and substitution for both natural and zero–one–many demands. Traverse a usage term to infer duplicate use, compare that demand with a promise, and check preserved and mismatched spines in both semirings.

Observable result. The run prints eight named PASS lines and ends All 8 Chapter 99 corpus cases passed.

A failing version. Omit multiplication by the binder grade in zero–one–many context scaling. The mutant checks, but substitution returns One,One instead of Many,One, so the named oracle fails. In a separate replay, make sameSpine return True; the mismatched natural-number spine oracle then fails.

Acceptance test. Run all four commands in subappendix E.8; require exact stdout and []. Restore the multiplication and repeat the commands.

Mathematical boundary. The program checks finite semiring equations. It does not prove QTT substitution or relate Idris source to erased run-time code.