Unproved contract · No Alpha or Stable authority

IR050 — Weak compositions and homogeneous sums

IR050 · planned

Construct the weak compositions of s into N+1 parts; count them as binomial(N+s,s), and implement the complete homogeneous sum h_s.

Method: native-induction. Induction: N+s. Risk: high.

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

Planned prerequisites and notation

Open this dependency cone