Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
IV0001 · dirichlet_unit_at_one_witnessAn actual unit-at-one lookup supplies its canonical signed unit code; no inverse property is hidden in the predicate.
layer 0 · 13 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0002 · dirichlet_unit_at_one_from_valueA genuine lookup with a canonical signed unit value satisfies the two-case unit-at-one predicate.
layer 0 · 13 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0003 · dirichlet_kronecker_delta_table_restrictThe same actual delta table restricts to every smaller positive window, without changing its unrelated zeroth value.
layer 0 · 29 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0004 · dirichlet_inverse_from_right_deltaOne actual right-delta convolution supplies both inverse laws by the already proved finite commutativity theorem.
layer 0 · 17 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0005 · dirichlet_inverse_symmetricSwapping the two actual convolution identities makes the original table an inverse of its inverse.
layer 0 · 13 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0006 · dirichlet_inverse_actual_tablesThe inverse graph entails actual valid input tables; it is never a vacuous equation between missing lookups.
layer 0 · 13 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0007 · dirichlet_inverse_zeroEvery pair of actual zero-window tables has a genuine delta witness and both empty positive-domain inverse identities, with no condition at one.
layer 0 · 29 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0008 · dirichlet_unit_equation_appendConstruct the proper signed remainder, solve its unit-coefficient equation, append the actual new input value and preserve every earlier convolution; the target table is arbitrary.
layer 0 · 134 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0009 · dirichlet_unit_equation_constructFinite induction constructs an actual solution G*F=T for every target table and signed unit F(1), with an arbitrary prescribed G(0), including actual witnesses when N=0.
layer 1 · 88 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV000A · dirichlet_inverse_from_unitConstruct an actual delta target and solve the genuine triangular convolution equation; both inverse laws and the independently prescribed zeroth value follow.
layer 2 · 37 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV000B · dirichlet_inverse_from_unit_at_oneEither actual canonical unit value at one constructively supplies a finite Dirichlet inverse, with any requested value at zero.
layer 3 · 19 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV000C · dirichlet_inverse_zero_constructThe empty positive window has a genuinely constructed inverse for any prescribed zeroth value, without assuming any lookup or unit condition at one.
layer 1 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV000D · dirichlet_inverse_constructThe exact empty-window-or-unit-at-one condition constructs actual inverse witnesses, preserving an arbitrary requested value at zero.
layer 4 · 27 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV000E · dirichlet_inverse_requires_unit_at_oneAt the genuinely in-domain index one, the actual convolution is a signed product equal to one, forcing the original value to be +1 or -1; the nonempty-domain guard is essential.
layer 1 · 87 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV000F · dirichlet_inverse_positive_uniqueAssociativity and independently constructed delta identities force any two actual inverses to agree at every positive input; neither their codes nor their zero values are identified.
layer 0 · 72 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0010 · dirichlet_inverse_restrictAn actual inverse restricts with its actual delta witness to every smaller finite positive window, including zero.
layer 1 · 34 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0011 · dirichlet_inverse_prefix_compatibleIndependently constructed inverse prefixes have identical represented positive values on their common smaller domain.
layer 2 · 21 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0012 · dirichlet_inverse_involutionTaking an actual Dirichlet inverse twice recovers precisely the original positive represented values, with no encoding or zeroth-value uniqueness claim.
layer 1 · 17 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0013 · dirichlet_inverse_criterionAn actual finite signed arithmetic table has a Dirichlet inverse exactly when the positive window is empty or its actual value at one is +1 or -1.
layer 5 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0014 · dirichlet_inverse_positive_criterionOn a nonempty positive domain the general constructive inverse criterion is precisely the actual signed unit-at-one condition.
layer 4 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableIV0015 · dirichlet_inverse_exists_positive_uniqueConstruct an actual inverse with any prescribed zeroth value and prove that every actual inverse agrees with it on all positive inputs, including the genuine empty-window boundary.
layer 5 · 28 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable
Exactly 21 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.