Every coded finite rational list has addition/product/factorial/power fold witnesses; results are unique up to RatEq, not unique codes.
Method: native-induction. Induction: list length. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.