One and delta convolution tables — Exact Proof Explorer

Every actual positive in-domain lookup in a constant-one table is canonical signed one, independently of its zero entry.

The actual entry at index one is signed one whenever that index lies in the finite table domain.

Every other positive in-domain delta entry is canonical zero; the omitted index-zero case remains unrestricted.

Constructively decide whether an index is one, obtaining its actual zero-or-one signed value before extending any table.

Actually append signed one at the next positive index by paired beta recoding, preserving the full previous prefix including zero.

Append the separately chosen actual delta value, preserving every earlier signed entry rather than assuming a table oracle.

For every finite bound, construct a genuine constant-one table retaining any prescribed signed value at zero, including the empty positive domain.

Finite constructive equality decisions and actual beta extensions build the delta table for every N, preserving any zero entry.

Equal represented positive values preserve this table graph without equating table codes, component representatives or their arbitrary zero entries.

All constructed representations agree at every positive in-domain entry; neither equality at zero nor equality of arbitrary table encodings is asserted.

Equal represented positive values preserve this table graph without equating table codes, component representatives or their arbitrary zero entries.

All constructed representations agree at every positive in-domain entry; neither equality at zero nor equality of arbitrary table encodings is asserted.

Every actual summand before n vanishes: a real complementary quotient is positive and cannot be one, while omitted indices are already zero.

At the final divisor n, actually read delta(1), use the quotient n=n*1, and multiply F(n) by signed one.

The actual zero-prefix/last-entry fold proves (F*delta)(n)=F(n), with positivity supplied by the convolution itself.

Construct a genuine convolution fold and prove its value equals the given actual F(n), rather than postulating the desired unit identity.

The original represented table F is a genuine whole-table right-unit convolution output on every positive input through N.

Actual divisor-complement commutativity turns the proved right-unit table into the left-unit table without imposing a zero-entry condition.

Every actual finite signed arithmetic table has a constructed two-sided convolution unit, with any requested unrelated value at index zero.

At every actual positive divisor the complementary one-table factor is signed one, so the convolution entry is precisely the existing divisor-mask entry.

Construct the actual bounded complementary lookup and its signed product from a genuine divisor-mask entry; omitted zero/nondivisor entries stay zero.

The same actual signed prefix represents the weighted convolution mask and the existing divisor mask; this preserves all witnesses and arbitrary prefix lengths.

The same actual signed prefix represents the weighted convolution mask and the existing divisor mask; this preserves all witnesses and arbitrary prefix lengths.

Actual convolution with a constant-one table is equivalent to the independently defined signed divisor sum, with exactly the same constructed mask and fold.

Construct an actual constant-one table with any chosen zero entry, and prove simultaneously at every positive in-domain input that its convolution is the existing divisor transform.