A beta-coded finite addition/multiplication execution; all input/output triples have positive denominators. It does not assert any analytic estimate.
Proposed arity: 4. Parameters: xs length trace result. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.