MV0009

mobius_value_exists

Finite prime-square search, actual prime factorization and parity construct the independently defined Möbius value for every positive natural.

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.

Mobius(n,z) is positive-domain only, independently defined from squarefreeness and actual prime-factor parity. Signed codes 0, 2 and 1 represent zero, +1 and -1. This family proves values and prime-adjunction laws; the separate Möbius-inversion family supplies the complete G007 endpoint.

Exact theorem in conservative defined notation

∀ n. ¬n = 0 → ∃ x. Mobius(n,x)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PrimeFactorList(n,b,c,l) · 1Squarefree(n) · 1AlternatingSignedUnit(n,z) · 1HasPrimeSquareDivisor(n) · 1Mobius(n,z) · 1

Actual proof prerequisites

squarefree_or_prime_square_divisor · checked external prerequisitefoundation_prime_factor_list_exists · checked external prerequisitealternating_signed_unit_existsmobius_from_squarefree_factor_countmobius_from_prime_square
Original expanded first-order statement 
forall n. ~(n = 0) -> exists z. (((~((n) = 0)) /\ ((((exists mv_square_prime_exists_valuesquare. ((~((mv_square_prime_exists_valuesquare) = 1) /\ forall pvs_left_exists_valuesquareprime pvs_right_exists_valuesquareprime. (mv_square_prime_exists_valuesquare) = pvs_left_exists_valuesquareprime * pvs_right_exists_valuesquareprime -> pvs_left_exists_valuesquareprime = 1 \/ pvs_right_exists_valuesquareprime = 1) /\ (exists pvs_factor_exists_valuesquaredivisor. (n) = (mv_square_prime_exists_valuesquare * mv_square_prime_exists_valuesquare) * pvs_factor_exists_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_exists_valuesquarefree. (~((sfd_prime_exists_valuesquarefree) = 1) /\ forall pvs_left_exists_valuesquarefreedomain pvs_right_exists_valuesquarefreedomain. (sfd_prime_exists_valuesquarefree) = pvs_left_exists_valuesquarefreedomain * pvs_right_exists_valuesquarefreedomain -> pvs_left_exists_valuesquarefreedomain = 1 \/ pvs_right_exists_valuesquarefreedomain = 1) -> (exists pvs_le_gap_exists_valuesquarefreebound. pvs_le_gap_exists_valuesquarefreebound + (sfd_prime_exists_valuesquarefree) = (n)) -> ~(exists pvs_factor_exists_valuesquarefreesquare. (n) = (sfd_prime_exists_valuesquarefree * sfd_prime_exists_valuesquarefree) * pvs_factor_exists_valuesquarefreesquare)))) /\ (exists mv_factor_code_exists_valuefactors mv_factor_scale_exists_valuefactors mv_factor_count_exists_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_exists_valuefactorsfactorization_product ff_v_fsat_exists_valuefactorsfactorization_product. ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_start. ff_h_fsat_exists_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_start. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_terminal. ff_h_fsat_exists_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_exists_valuefactors)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_terminal. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_exists_valuefactors)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_exists_valuefactorsfactorization_product. (exists ff_lt_fsat_exists_valuefactorsfactorization_product_bound. ff_lt_fsat_exists_valuefactorsfactorization_product_bound + S ff_i_fsat_exists_valuefactorsfactorization_product = mv_factor_count_exists_valuefactors) -> exists ff_p_fsat_exists_valuefactorsfactorization_product ff_r_fsat_exists_valuefactorsfactorization_product ff_s_fsat_exists_valuefactorsfactorization_product. ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_factor. ff_h_fsat_exists_valuefactorsfactorization_product_factor + S (ff_p_fsat_exists_valuefactorsfactorization_product) = S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * mv_factor_scale_exists_valuefactors)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_factor. mv_factor_code_exists_valuefactors = ff_q_fsat_exists_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * mv_factor_scale_exists_valuefactors) + (ff_p_fsat_exists_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_partial. ff_h_fsat_exists_valuefactorsfactorization_product_partial + S (ff_r_fsat_exists_valuefactorsfactorization_product) = S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_partial. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (ff_r_fsat_exists_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_successor. ff_h_fsat_exists_valuefactorsfactorization_product_successor + S (ff_s_fsat_exists_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_successor. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (ff_s_fsat_exists_valuefactorsfactorization_product))) /\ ff_s_fsat_exists_valuefactorsfactorization_product = ff_r_fsat_exists_valuefactorsfactorization_product * ff_p_fsat_exists_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_exists_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_exists_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_exists_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_exists_valuefactorsfactorization_primes = (mv_factor_count_exists_valuefactors)) -> exists ftsf_factor_fsat_exists_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_exists_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_exists_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_exists_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_exists_valuefactorsfactorization_primes)) * mv_factor_scale_exists_valuefactors)) /\ exists ff_q_ftsf_fsat_exists_valuefactorsfactorization_primes_entry. mv_factor_code_exists_valuefactors = ff_q_ftsf_fsat_exists_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_exists_valuefactorsfactorization_primes)) * mv_factor_scale_exists_valuefactors) + (ftsf_factor_fsat_exists_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_exists_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_exists_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_exists_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_exists_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_exists_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_exists_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_exists_valuefactorsparityeven. (mv_factor_count_exists_valuefactors) = 2 * mv_even_half_exists_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_exists_valuefactorsparityodd. (mv_factor_count_exists_valuefactors) = 2 * mv_odd_half_exists_valuefactorsparityodd + 1) /\ ((z) = 1)))))))))))

Complete tactic proof in conservative notation

All 37 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

37 script commands · 12 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
alternating signed unit existsmobius from squarefree factor countmobius from prime square
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro hn
02Establish hcaseL3–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply squarefree or prime square divisor.

  1. L3
    have hcase : Squarefree(n) ∨ HasPrimeSquareDivisor(n)Definitions: Squarefree(n)HasPrimeSquareDivisor(n)Original native command in the exact edition
  2. L4
    specialize squarefree_or_prime_square_divisor (n)
  3. L5
    apply squarefree_or_prime_square_divisor
  4. L6
    exact hn
03Separate the logical casesL7–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hcase
04Establish hfL8–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply foundation prime factor list exists.

  1. L8
    have hf : ∃ l. ∃ b. ∃ c. PrimeFactorList(n,b,c,l)Definitions: PrimeFactorList(n,b,c,l)Original native command in the exact edition
  2. L9
    specialize foundation_prime_factor_list_exists (n)
  3. L10
    apply foundation_prime_factor_list_exists
  4. L11
    exact hn
05Separate the logical casesL12–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hf
  2. L13
    cases hf_witness
  3. L14
    cases hf_witness_witness
06Establish hsL15–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply alternating signed unit exists.

  1. L15
    have hs : ∃ z. AlternatingSignedUnit(x,z)Definitions: AlternatingSignedUnit(x,z)Original native command in the exact edition
  2. L16
    specialize alternating_signed_unit_exists (x)
  3. L17
    apply alternating_signed_unit_exists
07Separate the logical casesL18–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L18
    cases hs
08Construct an explicit witnessL19–19

Supply the displayed value, then prove that it has the required property.

  1. L19
    exists x3
09Use earlier factsL20–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    specialize mobius_from_squarefree_factor_count (n)
  2. L21
    specialize mobius_from_squarefree_factor_count (x1)
  3. L22
    specialize mobius_from_squarefree_factor_count (x2)
  4. L23
    specialize mobius_from_squarefree_factor_count (x)
  5. L24
    specialize mobius_from_squarefree_factor_count (x3)
  6. L25
    apply mobius_from_squarefree_factor_count
  7. L26
    exact hcase_left
  8. L27
    exact hf_witness_witness_witness
  9. L28
    exact hs_witness
10Separate the logical casesL29–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hcase_right
  2. L30
    cases hcase_right_witness
11Construct an explicit witnessL31–31

Supply the displayed value, then prove that it has the required property.

  1. L31
    exists 0
12Use earlier factsL32–37

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    specialize mobius_from_prime_square (n)
  2. L33
    specialize mobius_from_prime_square (x)
  3. L34
    apply mobius_from_prime_square
  4. L35
    exact hn
  5. L36
    exact hcase_right_witness_left
  6. L37
    exact hcase_right_witness_right

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hcase : Squarefree(n) ∨ HasPrimeSquareDivisor(n)
  4. 0004specialize squarefree_or_prime_square_divisor (n)
  5. 0005apply squarefree_or_prime_square_divisor
  6. 0006exact hn
  7. 0007cases hcase
  8. 0008have hf : ∃ l. ∃ b. ∃ c. PrimeFactorList(n,b,c,l)
  9. 0009specialize foundation_prime_factor_list_exists (n)
  10. 0010apply foundation_prime_factor_list_exists
  11. 0011exact hn
  12. 0012cases hf
  13. 0013cases hf_witness
  14. 0014cases hf_witness_witness
  15. 0015have hs : ∃ z. AlternatingSignedUnit(x,z)
  16. 0016specialize alternating_signed_unit_exists (x)
  17. 0017apply alternating_signed_unit_exists
  18. 0018cases hs
  19. 0019exists x3
  20. 0020specialize mobius_from_squarefree_factor_count (n)
  21. 0021specialize mobius_from_squarefree_factor_count (x1)
  22. 0022specialize mobius_from_squarefree_factor_count (x2)
  23. 0023specialize mobius_from_squarefree_factor_count (x)
  24. 0024specialize mobius_from_squarefree_factor_count (x3)
  25. 0025apply mobius_from_squarefree_factor_count
  26. 0026exact hcase_left
  27. 0027exact hf_witness_witness_witness
  28. 0028exact hs_witness
  29. 0029cases hcase_right
  30. 0030cases hcase_right_witness
  31. 0031exists 0
  32. 0032specialize mobius_from_prime_square (n)
  33. 0033specialize mobius_from_prime_square (x)
  34. 0034apply mobius_from_prime_square
  35. 0035exact hn
  36. 0036exact hcase_right_witness_left
  37. 0037exact hcase_right_witness_right