Constructed triangular convolution steps — Exact Proof Explorer

Transport only the first actual lookup at a preserved index; retain the witnessed quotient, second lookup and signed product, including omitted zero entries.

The same actual summand table survives a first-input change strictly above its inclusive prefix bound; no equality at the changed endpoint is assumed.

Appending a first-input entry at l preserves every previously constructed convolution at m<l, with its original actual fold witnesses.

The whole earlier positive output table remains valid after appending the first input, including the vacuous N=0 boundary and arbitrary zero entries.

For n>0 the final divisor entry is exactly F(n)*G(1), using the actual quotient witness n=n*1 in both directions.

Actually construct the remainder prefix through k and its S k-entry fold even when the first input is only an inclusive k-table; the arbitrary value at S k is excluded.

Append the actual endpoint product to the real strict-prefix fold, constructing the full S(S k)-entry convolution without an assumed recurrence.

Change G(S k) only after computing the strict remainder, preserve every earlier summand, and construct the new convolution from the independently proved signed linear equation.

The genuine one-entry fold of an inclusive zero summand prefix is canonical zero, without restricting either input value at zero.

Actual convolution at input one is exactly the actual signed product F(1)*G(1); both implications construct or inspect the real two-entry masked fold.