# The next formal obligation

Lean now accepts the induction that makes every coefficient nonnegative, assuming the recipe is valid and its weights are nonnegative. The next task is to prove those assumptions for the actual rational function in the [analytic argument](source/research/millennium/iterations/0029/sharp-factorization.md).

1. Define the explicit four-index weights and prove their nonnegativity using the counted sign identity and multinomial comparison.
2. Identify the coefficients of `C = (1-Q)^4 R`, prove the initial coefficient is one, and derive the exact Euler recurrence in formal power series.
3. Apply the accepted conditional theorem to those identified coefficients.

These are proof obligations, not delivered results in this update. The later integral-to-Hardy connection is a further formalization task; outside review and originality remain separate open questions.