For every rational x and N, construct ExpPartial(x,N) with witnessed factorial and power tables; prove the successor recurrence and representation independence.
Method: native-induction. Induction: N. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.