Constructed Dirichlet convolution — Exact Proof Explorer

The zeroth summand is canonical zero without looking at either input value at zero.

A positive divisor, actual complementary quotient and actual signed product justify the retained summand.

A proved nondivisor contributes zero independently of both input tables.

Every actual omitted summand is exactly zero, and a supplied product witness cannot override that branch.

A retained entry is the product at the specified actual quotient; nonzero multiplication cancellation identifies every quotient witness.

Actual quotient, lookup and signed-product functionality determine one canonical summand, without identifying table codes.

Decide membership, extract the actual quotient, construct both signed lookups and multiply them; neither choice nor a quotient oracle is assumed.

A real singleton zero table supplies the inclusive zero prefix for every fixed input, independently of F(0) and G(0).

Append one actual product-or-zero entry by paired beta recoding, preserving every earlier canonical signed value.

Ordinary prefix induction constructs every finite summand table; its length is independent of n, and no finite choice principle is assumed.

Every actual decoded entry in the inclusive constructed prefix obeys the independently defined product-or-zero graph.

All genuine summand prefixes agree through their last entry in represented value, without asserting equality of arbitrary table codes.

The same actual summand code restricts to any smaller inclusive window, for its unchanged convolution input n.

At every witnessed positive divisor, the actual summand table contains precisely F(d)*G(q), with n=d*q supplied and checked.

The real prefix has zero at every omitted index, including zero, without any corresponding input-value condition.

Construct the actual weighted divisor prefix and its S n-entry signed fold at every positive in-domain input.

Different actual weighted prefixes and signed representatives give the same canonical convolution value.

The actual finite Dirichlet convolution has one literally unique signed value at every 0<n<=N; the input zero entries are unrestricted.

Zero is outside the convolution-value domain; it is not assigned an artificial finite all-divisors sum.

Only positive in-domain source values matter: a genuine quotient is proved positive and bounded before either source equality is applied.

Positive-source equality gives equality of every actual masked product value, including the forced zero output at index zero.

Actual convolution values depend only on positive input values through n, permitting all four zeroth input values to be unrelated.

Construct the comparison fold before transporting an actual convolution value across positive-source equality; zero entries are untouched.

At bound zero any actual output table is a valid empty positive-window convolution table; no zero-entry value is prescribed.

Append the genuinely computed next convolution value by actual beta recoding, preserving every earlier value including an arbitrary output value at zero.

Finite induction constructs an actual convolution table at every positive index through N, including a genuine table witness when N is zero.

Every positive in-domain convolution-table entry supplies its actual canonical value and complete finite signed fold.

All actual output tables agree at precisely the positive indices through N; their zero entries and beta encodings need not agree.

Construct the entire finite Dirichlet-convolution table and prove positive-window uniqueness, not equality of arbitrary codes or zeroth values.

The same actual inputs and output restrict to every smaller positive window, including J=0, without changing any encoded value.

Actual divisor complementation swaps the two signed factors, while fixed zero/nondivisor positions remain genuinely zero.

Every independently justified summand value is present in the actual prefix, by constructed lookup and functionality.

The actual complement beta map pulls one constructed convolution-summand prefix into the factor-swapped prefix.

A genuinely constructed finite divisor permutation proves commutativity of actual signed Dirichlet-convolution values.

Construct the factor-swapped convolution and prove that the original canonical value is its actual sum.

The same genuine output table represents either convolution order on every positive index; its value at zero remains unrestricted.

A summand beyond a positive input is zero because a positive-input divisor cannot exceed that input.

Every actually stored convolution summand after index n is zero, with the inclusive prefix endpoints retained exactly.

An actual longer summand prefix computes the same convolution after its proved zero tail is removed.

The actual padded fold and the original finite convolution are equivalent; the reverse direction constructs its own genuine sum trace.