Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
DU0001 dirichlet_constant_one_table_valueEvery 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 StableDU0002 dirichlet_kronecker_delta_table_one_valueThe 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 StableDU0003 dirichlet_kronecker_delta_table_other_valueEvery 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 StableDU0004 dirichlet_kronecker_delta_value_existsConstructively 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 StableDU0005 dirichlet_constant_one_table_appendActually 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 StableDU0006 dirichlet_kronecker_delta_table_appendAppend 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 StableDU0007 dirichlet_constant_one_table_existsFor 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 StableDU0008 dirichlet_kronecker_delta_table_existsFinite 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 StableDU0009 dirichlet_constant_one_table_reencodingEqual 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 StableDU000A dirichlet_constant_one_table_positive_uniqueAll 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 StableDU000B dirichlet_kronecker_delta_table_reencodingEqual 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 StableDU000C dirichlet_kronecker_delta_table_positive_uniqueAll 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 StableDU000D dirichlet_delta_right_entry_before_inputEvery 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 StableDU000E dirichlet_delta_right_last_entryAt 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 StableDU000F dirichlet_delta_right_sum_valueThe 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 StableDU0010 dirichlet_delta_right_sumConstruct 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 StableDU0011 dirichlet_delta_right_tableThe 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 StableDU0012 dirichlet_delta_left_tableActual 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 StableDU0013 dirichlet_delta_unit_existsEvery 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 StableDU0014 dirichlet_constant_one_entry_to_divisor_maskAt 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 StableDU0015 dirichlet_constant_one_entry_from_divisor_maskConstruct 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 StableDU0016 dirichlet_constant_one_prefix_to_divisor_maskThe 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 StableDU0017 dirichlet_constant_one_prefix_from_divisor_maskThe 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 StableDU0018 dirichlet_constant_one_sum_iffActual 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 StableDU0019 dirichlet_constant_one_realizes_divisor_sumConstruct 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 StablePD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0058 MatrixMinorFourCode(z,up,us,un,ut)One canonical injective doubled-Cantor code for all four signed-minor beta-code parameters.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0ND0142 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 0ND0143 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 1ND0252 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 2PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0ND0145 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 1ND0301 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 3ND0251 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 2ND0302 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 4PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1ND0253 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 2ND0303 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 5ND0304 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 6ND0273 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 3ND0274 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 4ND0275 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 5ND0276 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 3ND0300 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 3ND0310 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 3ND0311 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.