Unproved contract · No Alpha or Stable authority

IRD08 — ExpPartial

IRD08 · proposed

value=sum(j<=N,x^j/j!) by witnessed powers, factorials and a rational fold; denominator positivity is explicit.

Proposed arity: 4. Parameters: x N value trace. No reviewed kernel definition exists yet.

This is a human-readable planning contract, not a parsed kernel formula or accepted proof.

Planned prerequisites and notation

Open this dependency cone