Multiplicative Dirichlet convolution — Exact Proof Explorer

The finite multiplicativity relation excludes an empty positive domain.

Finite multiplicativity includes a genuine arithmetic table, not vacuous missing lookups.

The actual value at one is canonical signed positive one, not an arbitrary signed unit.

Read the exact coprime-product law, including positivity and the inclusive product bound.

Combine the actual table, positive normalization and bounded coprime law without any hidden premise.

No zero-window table satisfies the strict nonempty multiplicativity convention.

Every actual lookup at one has the unique positive-one signed code 2.

The same normalized table is multiplicative on every smaller nonempty positive prefix.

Construct all three actual signed values and their multiplication witness; the law is not merely conditional on absent entries.

Transport a real positive lookup across prefix equality by first constructing the target lookup; no encoding or zero-value equality is required.

Multiplicativity depends only on the represented positive prefix, not on table codes, zeroth values or entries outside the product bound.

The two genuine gcds multiply to the given positive divisor of a coprime product.

Every actual positive factor pair has its coordinates recovered by the two canonical relational gcds.

The positive-divisor product map is injective on genuine divisor pairs of coprime inputs.

Canonical gcd existence supplies real positive divisor coordinates, without a factorization or choice oracle.

For positive inputs each coordinate lies in its actual divisor window, and the coordinates are coprime.

Every positive divisor of a positive coprime product has exactly one bounded positive divisor pair.

Real positive bounded cofactor witnesses have all cross-input coprimality relations and multiply to the true quotient.

For any actual positive divisor pair, a supplied product quotient equals the product of the supplied cofactors.

Actual bounded quotient and remainder determine the next product value; beta-prefix extension constructs new codes and preserves all earlier decoded entries.

Finite HA induction constructs a native-beta pair-product map for every positive width and finite window, including the empty window.

At supplied genuine row and bounded column coordinates, the actual beta code stores their product.

Any decoded value at a certified coordinate equals the actual coordinate product; equality of beta-code components is not asserted.

The original packed table itself is a genuine zero-origin, unit-stride slice; the certified endpoint is unused.

An actual zero-origin, unit-stride slice sum is exactly the existing actual signed prefix sum, independently of slice encoding.

Ordinary length induction concatenates actual affine sum traces at offset o+s*p, including zero length and zero stride.

The two actual consecutive affine sums add to the actual combined sum, without assuming the addition law as a premise.

Actual row sums concatenate into the genuine flattened source sum by row-count induction, including either zero dimension.

The actual flattened signed prefix and actual row-major rectangle are equivalent, not merely two transposed rectangular folds.

Construct an actual signed value shared by the flattened prefix and its row-major rectangular fold, with no supplied trace or row table.

For positive physical width, actual quotient/remainder and actual signed lookups construct each flattened product value.

Unique bounded remainder coordinates and signed lookup functionality recover the actual prescribed cell product.

A real singleton and actual flat product provide the inclusive base prefix.

Actually recode both beta streams, preserve the old represented values, and install the next independently constructed flat product.

Ordinary induction constructs the entire actual finite flattened product prefix; no finite-choice or output-table oracle is supplied.

The actual finite flat construction supplies every in-range row-major product by proved index bounds and unique decoding.

A zero-column rectangle has no constrained cell, but all three table packings remain genuine.

Construct an actual finite signed outer-product beta table for arbitrary dimensions, explicitly including zero width and zero height.

Each actual row slice is a genuine pointwise scalar product by its actual first-input value.

The actual sum of each product row is the signed product of its row scalar and the actual second-input sum.

The genuinely constructed row-sum table is pointwise the first input multiplied by the actual second-input sum.

Two applications of actual signed scalar linearity prove that the rectangular outer-product total is the product of the two actual sums.

The actual flattened product prefix sums to the canonical signed product, using the separately proved flattening bridge; both zero dimensions are included.

Construct the actual outer-product table and all three signed sum traces, and prove their product relation without an assumed constructor or sum witness.

An actual flattened index below a rectangular area has its quotient row below the height, including vacuous zero-area cases.

Every actual index in a finite rectangular window has constructed bounded row and column coordinates, with no positive-width assumption supplied.

An actual in-range product-table lookup supplies real bounded coordinates, both actual source values and their genuine signed product.

Every in-range flat index has actual bounded row and column coordinates, so all outer-product encodings represent the same signed value there.

Any real recoding preserving precisely the flattened product window remains the same outer product; the unused endpoint may change.

Construct the actual outer product and prove value uniqueness on its exact strict finite window, without asserting uniqueness of beta codes.

An actual signed sum with one arbitrary-position entry and proved zero windows has exactly that entry value.

Construct actual fold traces for an arbitrary-position signed spike, including zero and negative values.

Pointwise zero values away from one actual bounded index imply the two zero windows needed for the spike sum.

An actual source lookup and actual beta image supply the retained incidence cell.

An actual source lookup and beta image construct a zero cell at every different target index.

Actual signed lookup and beta uniqueness recover the independently stated hit-or-zero cell cases.

The actual incidence value is unique, independent of witnesses and component representations.

Every cell is constructively computed from a real signed lookup, a real natural beta image, and decidable equality.

Every incidence cell of a represented zero source is zero, even at an out-of-window image.

A nonzero incidence value witnesses both the identical actual source value and the actual beta image.

Division by the positive padded width S M and actual incidence lookup construct every flat value, including M=0.

Uniqueness of actual quotient and strict remainder recovers the specified incidence coordinates.

A real singleton encodes the first actual flat incidence cell.

Constructively append one actual flat cell and preserve every preceding represented value.

Ordinary induction constructs the entire inclusive prefix by real beta-stream extension, with no choice or sum oracle.

The genuine inclusive flat prefix covers every strict rectangular cell; the extra column and endpoint are unused.

Construct an actual padded incidence table for every pair of finite dimensions, including either zero dimension.

An actual affine row-slice entry is the incidence cell at the same strict row and column indices.

An actual affine column-slice entry is the same incidence cell after proved natural index commutation.

Each actual incidence row is zero or one genuinely bounded spike, so its actual sum is the actual source value.

Target coverage supplies the actual nonzero spike; active injectivity excludes other nonzero cells and preservation handles zero targets.

Every actual incidence row-sum table agrees with the represented source values on precisely the strict source window.

Every actual incidence column-sum table agrees with the represented target values on precisely the strict target window.

Construct the actual incidence and both fold tables; ordinary finite Fubini proves equality under support-only reindexing, including unequal or empty windows.

Actually construct both signed finite folds and their common canonical value; neither fold is assumed as an oracle.

Reorder four actual signed factors by constructing the intermediate product and using checked associativity and commutativity.

A nonzero actual signed product has two nonzero factors, by the signed zero laws and functionality.

A genuinely nonzero convolution summand supplies a positive divisor and its actual quotient; omitted indices cannot enter the support.

On a genuine coprime divisor pair, construct positive cofactors and six signed lookups, apply both bounded multiplicative laws, and factor the actual target summand.

The product of the two actual pair summands is a genuine target convolution entry; its value is identified using a constructed target entry, never assumed.

Every genuinely nonzero product-table entry decodes to a positive divisor pair and two actual nonzero convolution summands; zero and nondivisor collisions are excluded constructively.

Each nonzero source slot has its actual beta image in the shorter target window and exactly the same signed value, by proved summand factorization.

Equal beta images of two genuinely nonzero source slots give the same positive divisor pair by gcd uniqueness, hence the same flattened index; inactive collisions remain permitted.

Every nonzero target summand has a genuine bounded source slot: construct its unique positive divisor pair, both input summands and the product-table lookup, then prove exact value preservation.

The actual native-beta divisor-product map is a value-preserving bijection of nonzero support between two unequal finite windows; no whole-window permutation is asserted.

From the actual three summand prefixes construct the Cartesian product table and native-beta index map, with no assumed table, map, sum or reindexing conclusion.

The actual convolution values at positive coprime m,n multiply to the actual value at mn, using genuine divisor-pair support reindexing and only in-prefix multiplicativity.

An actual convolution table of two normalized multiplicative signed prefixes is itself normalized and multiplicative on every positive coprime product through the inclusive bound.

Construct a genuine multiplicative convolution table and prove uniqueness of its represented positive values, without identifying arbitrary zero values or table encodings.

Positive-one normalization gives an actual two-sided finite Dirichlet inverse with any prescribed zeroth value; this corollary does not assert multiplicativity of the inverse.