MV0001 · alternating_signed_unit_existsParity constructs an actual canonical code for the alternating unit at every natural exponent.
layer 0 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableCurrent library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
MV0002 · alternating_signed_unit_functionalConstructive parity exclusivity makes the signed alternating-unit code unique.
layer 0 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0003 · alternating_signed_unit_zeroExponent zero has canonical positive-unit code two, not code one.
layer 0 · 6 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0004 · mobius_prime_factor_count_uniqueActual unordered prime-factor uniqueness proves literal equality of factor counts; no canonical list is assumed.
layer 0 · 22 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0005 · mobius_input_positiveThe independent Möbius graph explicitly excludes the infinite-divisor boundary zero.
layer 0 · 5 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0006 · mobius_zero_has_no_valueNo canonical signed value is asserted for the excluded input zero.
layer 1 · 7 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0007 · mobius_from_prime_squareA supplied actual prime-square divisor of a positive input constructs its canonical zero Möbius value.
layer 0 · 14 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0008 · mobius_from_squarefree_factor_countSquarefreeness, a real prime-factor list and its actual length parity construct the nonzero Möbius value.
layer 0 · 20 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0009 · mobius_value_existsFinite prime-square search, actual prime factorization and parity construct the independently defined Möbius value for every positive natural.
layer 1 · 37 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV000A · mobius_squarefree_evaluationFor a squarefree input, every real factor list computes the same Möbius sign, independently of ordering or chosen witnesses.
layer 1 · 39 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV000B · mobius_value_functionalMöbius values have literally unique canonical signed codes; square-divisor and squarefree branches are disjoint by proof.
layer 2 · 46 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV000C · mobius_value_exists_uniqueEvery positive natural has one actual, uniquely determined, factorization-defined canonical Möbius value.
layer 3 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV000D · mobius_oneThe unit boundary has Möbius value positive one (signed code two), proved from its actual empty prime factorization.
layer 1 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV000E · mobius_squarefree_divisorA genuine divisor of a positive squarefree input is positive and squarefree, with no bound assumption on its prime-square witnesses.
layer 0 · 30 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV000F · mobius_prime_squarefreeNo genuine prime has a squared prime divisor; both nonzero and nonunit boundaries are proved from primality.
layer 0 · 49 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0010 · mobius_squarefree_fresh_prime_productAdjoining an actual prime not dividing a squarefree input preserves squarefreeness; Euclid cancellation excludes every possible squared prime divisor.
layer 0 · 70 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0011 · mobius_prime_factor_list_appendThe beta extension theorem constructs a new actual prime list with one more occurrence and product n*p; no sorted or preselected factorization is supplied.
layer 0 · 53 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0012 · mobius_positive_unit_negates_to_negative_unitCanonical code two is positive one and code one is its genuine decoded additive inverse.
layer 0 · 17 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0013 · alternating_signed_unit_successor_negatesThe alternating unit at the successor exponent is the canonical signed negation, proved by the two constructive parity cases.
layer 1 · 49 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0014 · mobius_prime_square_value_zeroEvery independently defined Möbius value at an actual prime-square multiple is the canonical zero code.
layer 3 · 22 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMV0015 · mobius_fresh_prime_negatesFor an actual prime not dividing n, adjoining that prime negates the genuine Möbius value, including all nonsquarefree zero cases.
layer 4 · 74 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 21 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.