Independent signed values · squarefreeness · genuine factor lists
Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.
Define Möbius values from squarefreeness and the parity of actual prime-factor lists, prove unique values, and trace how a fresh prime changes the sign.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
MV0001 alternating_signed_unit_existsParity constructs an actual canonical code for the alternating unit at every natural exponent.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0002 alternating_signed_unit_functionalConstructive parity exclusivity makes the signed alternating-unit code unique.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0003 alternating_signed_unit_zeroExponent zero has canonical positive-unit code two, not code one.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0004 mobius_prime_factor_count_uniqueActual unordered prime-factor uniqueness proves literal equality of factor counts; no canonical list is assumed.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0005 mobius_input_positiveThe independent Möbius graph explicitly excludes the infinite-divisor boundary zero.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0006 mobius_zero_has_no_valueNo canonical signed value is asserted for the excluded input zero.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0007 mobius_from_prime_squareA supplied actual prime-square divisor of a positive input constructs its canonical zero Möbius value.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0008 mobius_from_squarefree_factor_countSquarefreeness, a real prime-factor list and its actual length parity construct the nonzero Möbius value.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0009 mobius_value_existsFinite prime-square search, actual prime factorization and parity construct the independently defined Möbius value for every positive natural.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV000A mobius_squarefree_evaluationFor a squarefree input, every real factor list computes the same Möbius sign, independently of ordering or chosen witnesses.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV000B mobius_value_functionalMöbius values have literally unique canonical signed codes; square-divisor and squarefree branches are disjoint by proof.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV000C mobius_value_exists_uniqueEvery positive natural has one actual, uniquely determined, factorization-defined canonical Möbius value.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV000D mobius_oneThe unit boundary has Möbius value positive one (signed code two), proved from its actual empty prime factorization.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV000F mobius_prime_squarefreeNo genuine prime has a squared prime divisor; both nonzero and nonunit boundaries are proved from primality.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0012 mobius_positive_unit_negates_to_negative_unitCanonical code two is positive one and code one is its genuine decoded additive inverse.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableMV0014 mobius_prime_square_value_zeroEvery independently defined Möbius value at an actual prime-square multiple is the canonical zero code.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StablePD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0024 BoundedPrefix(b,c,l)Every decoded entry below l is itself below l.
Conservative definition · notation layer 1PD0025 InjectivePrefix(b,c,l)Equal decoded values below l have equal indices.
Conservative definition · notation layer 1PD0026 SurjectivePrefix(b,c,l)Every value below l occurs at an index below l.
Conservative definition · notation layer 1ND0142 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 0ND0146 SignedNegate(a,b)Canonical signed negation swaps the positive and negative decoded parts.
Conservative definition · notation layer 1PD0009 Even(n)n has an even decomposition.
Conservative definition · notation layer 0PD0010 Odd(n)n has an odd decomposition.
Conservative definition · notation layer 0ND0233 AlternatingSignedUnit(n,z)The actual signed code of (-1)^n from parity: even exponents give code 2 (+1), odd exponents code 1 (-1).
Conservative definition · notation layer 1ND0234 HasPrimeSquareDivisor(n)A genuine prime p and an actual quotient witness p*p dividing n. This is not an asserted factorization oracle.
Conservative definition · notation layer 1PD0028 AllPrime(b,c,l)Every decoded factor below l is prime.
Conservative definition · notation layer 1ND0149 PrimeFactorList(n,b,c,l)A positive number n, an actual length-l beta product equal to n, and prime entries. No sortedness or supplied canonicalization is required.
Conservative definition · notation layer 2ND0235 FactorParitySign(n,z)A genuine finite prime-factor list for n has a length whose alternating signed unit is z. Independence of the factor list is proved.
Conservative definition · notation layer 3PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0ND0188 Squarefree(n)Positive n with no squared prime divisor p² for any prime p≤n. The bounded condition is proved to exclude all squared prime divisors.
Conservative definition · notation layer 1ND0236 Mobius(n,z)For positive n, an actual prime-square divisor gives signed zero; otherwise squarefreeness and real factor-count parity give the signed unit. No divisor-sum or inversion identity occurs here.
Conservative definition · notation layer 4Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.