Arbitrary zeroth values · actual constructors · divisor sums

One and delta convolution tables

Construct one and delta tables and prove the actual two-sided unit and divisor-sum identities.

25 kernel- and Lean-verified Alpha-closed theorems · 23 conservative definitions · 45 notation dependencies

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

48 items
DU0001 dirichlet_constant_one_table_value

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0002 dirichlet_kronecker_delta_table_one_value

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0003 dirichlet_kronecker_delta_table_other_value

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0004 dirichlet_kronecker_delta_value_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0005 dirichlet_constant_one_table_append

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0006 dirichlet_kronecker_delta_table_append

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0007 dirichlet_constant_one_table_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0008 dirichlet_kronecker_delta_table_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0009 dirichlet_constant_one_table_reencoding

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU000A dirichlet_constant_one_table_positive_unique

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU000B dirichlet_kronecker_delta_table_reencoding

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU000C dirichlet_kronecker_delta_table_positive_unique

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU000D dirichlet_delta_right_entry_before_input

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU000E dirichlet_delta_right_last_entry

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU000F dirichlet_delta_right_sum_value

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0010 dirichlet_delta_right_sum

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0011 dirichlet_delta_right_table

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0012 dirichlet_delta_left_table

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0013 dirichlet_delta_unit_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0014 dirichlet_constant_one_entry_to_divisor_mask

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0015 dirichlet_constant_one_entry_from_divisor_mask

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0016 dirichlet_constant_one_prefix_to_divisor_mask

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0017 dirichlet_constant_one_prefix_from_divisor_mask

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0018 dirichlet_constant_one_sum_iff

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
DU0019 dirichlet_constant_one_realizes_divisor_sum

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.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0013 BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative definition · notation layer 0
ND0142 SignedDecode(z,p,n)

The original canonical integer code: even 2p denotes p, and odd 2k+1 denotes −(k+1). The decoded positive and negative parts are normalized.

Conservative definition · notation layer 0
ND0143 SignedBalance(z,p,n)

The original canonical code z represents the integer difference p−n; these supplied components need not be normalized.

Conservative definition · notation layer 1
ND0252 ArithAt(F,i,z)

Two genuine beta entries of the packed table represent the unique canonical signed value z. Distinct component representations need not be equal.

Conservative definition · notation layer 2
PD0003 Dvd(d,n)

The natural number d divides n.

Conservative definition · notation layer 0
ND0145 SignedMul(a,b,c)

Actual multiplication of original canonical signed codes; opposite-sign products remain on the negative side of the balance.

Conservative definition · notation layer 1
ND0301 DirichletEntry(F,G,n,d,z)

At a positive divisor d, witness n=d*q, read the actual signed values F(d) and G(q), and multiply them. Zero and nondivisors contribute canonical zero without reading either input at zero. Source-table validity is separate.

Conservative definition · notation layer 3
ND0251 ArithTable(N,F)

An actual packed signed table with canonical signed entries through index N, including index zero. It contains no divisor transform or inversion hypothesis.

Conservative definition · notation layer 2
ND0302 DirichletPrefix(F,G,n,l,M)

An actual signed table M records the independently defined convolution entry at every inclusive index 0<=d<=l. The endpoint l is included and can differ from n; no sum or convolution identity is assumed.

Conservative definition · notation layer 4
PD0015 Sum(b,c,l,z)

z is the sum of a beta-coded prefix of length l.

Conservative definition · notation layer 1
ND0253 SignedPrefixSum(F,l,z)

The signed balance of two actual natural finite sums, at exactly the indices 0<=i<l. Existence, uniqueness and representation independence are proved separately.

Conservative definition · notation layer 2
ND0303 DirichletSum(F,G,n,z)

Require n>0, construct a real convolution-summand prefix through n, and take its actual signed fold over exactly S n entries. Zero is outside this sum's input domain; no value is assigned by a unit or inversion formula.

Conservative definition · notation layer 5
ND0304 DirichletTable(N,F,G,H)

Three actual finite signed tables whose output H(n), at every 0<n<=N, is the independently defined convolution sum of F and G. All zero entries are unrestricted; only represented positive values, not table codes, are subsequently proved unique.

Conservative definition · notation layer 6
ND0273 DivisorMaskEntry(F,n,d,z)

A positive d with an actual quotient n=d*q keeps the genuine input value F(d); zero and nondivisors give canonical zero. The zero branch never reads or restricts F(0).

Conservative definition · notation layer 3
ND0274 DivisorMask(F,n,l,M)

An actual signed table through the inclusive bound l satisfies the independent divisor-mask entry graph at every represented index. The construction bound l is independent of n, enabling ordinary finite induction.

Conservative definition · notation layer 4
ND0275 DivisorSum(F,n,z)

For explicitly positive n, construct a genuine mask through n and take its actual signed fold over S n entries. Index zero is masked away; neither divisor cancellation nor Möbius inversion is part of the graph.

Conservative definition · notation layer 5
ND0276 ArithPositiveEqual(F,G,N)

Equality of represented values at precisely 0<d<=N. Values at zero are unrestricted, and raw codes or positive/negative representatives are not asserted equal.

Conservative definition · notation layer 3
ND0300 SignedZeroWindow(F,k,l)

Every actual signed lookup on the half-open interval k<=i<l has value zero. Table validity, existence of folds, and equality after padding are separate hypotheses or theorems, not part of this graph.

Conservative definition · notation layer 3
ND0310 ConstantOneTable(N,U)

An actual signed table has canonical one, code 2, at every 0<n<=N. Its value at zero is unrestricted, including when N=0. Existence with any prescribed zero entry and the divisor-sum identity are separately proved.

Conservative definition · notation layer 3
ND0311 KroneckerDeltaTable(N,E)

An actual signed table has code 2 at n=1 and code 0 at all other positive n<=N. Its zero entry is unrestricted and N=0 has an empty positive domain. Both convolution unit laws are theorems, not definition premises.

Conservative definition · notation layer 3

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.