MV000A

mobius_squarefree_evaluation

For a squarefree input, every real factor list computes the same Möbius sign, independently of ordering or chosen witnesses.

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. ∀ b. ∀ c. ∀ l. ∀ z. Squarefree(n) → PrimeFactorList(n,b,c,l) → Mobius(n,z) → AlternatingSignedUnit(l,z)

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

Definition DAG

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

Actual proof prerequisites

squarefree_excludes_prime_square · checked external prerequisitemobius_prime_factor_count_unique
Original expanded first-order statement 
forall n b c l z. (((~((n) = 0)) /\ (forall sfd_prime_evaluation_sf. (~((sfd_prime_evaluation_sf) = 1) /\ forall pvs_left_evaluation_sfdomain pvs_right_evaluation_sfdomain. (sfd_prime_evaluation_sf) = pvs_left_evaluation_sfdomain * pvs_right_evaluation_sfdomain -> pvs_left_evaluation_sfdomain = 1 \/ pvs_right_evaluation_sfdomain = 1) -> (exists pvs_le_gap_evaluation_sfbound. pvs_le_gap_evaluation_sfbound + (sfd_prime_evaluation_sf) = (n)) -> ~(exists pvs_factor_evaluation_sfsquare. (n) = (sfd_prime_evaluation_sf * sfd_prime_evaluation_sf) * pvs_factor_evaluation_sfsquare)))) -> ((~(n = 0) /\ ((exists ff_u_fsat_mv_evaluation_factors_product ff_v_fsat_mv_evaluation_factors_product. ((((exists ff_h_fsat_mv_evaluation_factors_product_start. ff_h_fsat_mv_evaluation_factors_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_start. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_start * S ((S (0)) * ff_v_fsat_mv_evaluation_factors_product) + (1))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_terminal. ff_h_fsat_mv_evaluation_factors_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_terminal. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_terminal * S ((S (l)) * ff_v_fsat_mv_evaluation_factors_product) + (n))) /\ forall ff_i_fsat_mv_evaluation_factors_product. (exists ff_lt_fsat_mv_evaluation_factors_product_bound. ff_lt_fsat_mv_evaluation_factors_product_bound + S ff_i_fsat_mv_evaluation_factors_product = l) -> exists ff_p_fsat_mv_evaluation_factors_product ff_r_fsat_mv_evaluation_factors_product ff_s_fsat_mv_evaluation_factors_product. ((((exists ff_h_fsat_mv_evaluation_factors_product_factor. ff_h_fsat_mv_evaluation_factors_product_factor + S (ff_p_fsat_mv_evaluation_factors_product) = S ((S (ff_i_fsat_mv_evaluation_factors_product)) * c)) /\ exists ff_q_fsat_mv_evaluation_factors_product_factor. b = ff_q_fsat_mv_evaluation_factors_product_factor * S ((S (ff_i_fsat_mv_evaluation_factors_product)) * c) + (ff_p_fsat_mv_evaluation_factors_product))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_partial. ff_h_fsat_mv_evaluation_factors_product_partial + S (ff_r_fsat_mv_evaluation_factors_product) = S ((S (ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_partial. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_partial * S ((S (ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product) + (ff_r_fsat_mv_evaluation_factors_product))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_successor. ff_h_fsat_mv_evaluation_factors_product_successor + S (ff_s_fsat_mv_evaluation_factors_product) = S ((S (S ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_successor. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_successor * S ((S (S ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product) + (ff_s_fsat_mv_evaluation_factors_product))) /\ ff_s_fsat_mv_evaluation_factors_product = ff_r_fsat_mv_evaluation_factors_product * ff_p_fsat_mv_evaluation_factors_product)))))) /\ (forall ftsf_index_fsat_mv_evaluation_factors_primes. (exists ftsf_gap_fsat_mv_evaluation_factors_primes_bound. ftsf_gap_fsat_mv_evaluation_factors_primes_bound + S ftsf_index_fsat_mv_evaluation_factors_primes = (l)) -> exists ftsf_factor_fsat_mv_evaluation_factors_primes. ((((exists ff_h_ftsf_fsat_mv_evaluation_factors_primes_entry. ff_h_ftsf_fsat_mv_evaluation_factors_primes_entry + S (ftsf_factor_fsat_mv_evaluation_factors_primes) = S ((S (ftsf_index_fsat_mv_evaluation_factors_primes)) * c)) /\ exists ff_q_ftsf_fsat_mv_evaluation_factors_primes_entry. b = ff_q_ftsf_fsat_mv_evaluation_factors_primes_entry * S ((S (ftsf_index_fsat_mv_evaluation_factors_primes)) * c) + (ftsf_factor_fsat_mv_evaluation_factors_primes))) /\ ((~(ftsf_factor_fsat_mv_evaluation_factors_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime. ftsf_factor_fsat_mv_evaluation_factors_primes = frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime * frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime -> frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime = 1))))))) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_evaluation_valuesquare. ((~((mv_square_prime_evaluation_valuesquare) = 1) /\ forall pvs_left_evaluation_valuesquareprime pvs_right_evaluation_valuesquareprime. (mv_square_prime_evaluation_valuesquare) = pvs_left_evaluation_valuesquareprime * pvs_right_evaluation_valuesquareprime -> pvs_left_evaluation_valuesquareprime = 1 \/ pvs_right_evaluation_valuesquareprime = 1) /\ (exists pvs_factor_evaluation_valuesquaredivisor. (n) = (mv_square_prime_evaluation_valuesquare * mv_square_prime_evaluation_valuesquare) * pvs_factor_evaluation_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_evaluation_valuesquarefree. (~((sfd_prime_evaluation_valuesquarefree) = 1) /\ forall pvs_left_evaluation_valuesquarefreedomain pvs_right_evaluation_valuesquarefreedomain. (sfd_prime_evaluation_valuesquarefree) = pvs_left_evaluation_valuesquarefreedomain * pvs_right_evaluation_valuesquarefreedomain -> pvs_left_evaluation_valuesquarefreedomain = 1 \/ pvs_right_evaluation_valuesquarefreedomain = 1) -> (exists pvs_le_gap_evaluation_valuesquarefreebound. pvs_le_gap_evaluation_valuesquarefreebound + (sfd_prime_evaluation_valuesquarefree) = (n)) -> ~(exists pvs_factor_evaluation_valuesquarefreesquare. (n) = (sfd_prime_evaluation_valuesquarefree * sfd_prime_evaluation_valuesquarefree) * pvs_factor_evaluation_valuesquarefreesquare)))) /\ (exists mv_factor_code_evaluation_valuefactors mv_factor_scale_evaluation_valuefactors mv_factor_count_evaluation_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_evaluation_valuefactorsfactorization_product ff_v_fsat_evaluation_valuefactorsfactorization_product. ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_start. ff_h_fsat_evaluation_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_start. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_terminal. ff_h_fsat_evaluation_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_evaluation_valuefactors)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_terminal. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_evaluation_valuefactors)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_evaluation_valuefactorsfactorization_product. (exists ff_lt_fsat_evaluation_valuefactorsfactorization_product_bound. ff_lt_fsat_evaluation_valuefactorsfactorization_product_bound + S ff_i_fsat_evaluation_valuefactorsfactorization_product = mv_factor_count_evaluation_valuefactors) -> exists ff_p_fsat_evaluation_valuefactorsfactorization_product ff_r_fsat_evaluation_valuefactorsfactorization_product ff_s_fsat_evaluation_valuefactorsfactorization_product. ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_factor. ff_h_fsat_evaluation_valuefactorsfactorization_product_factor + S (ff_p_fsat_evaluation_valuefactorsfactorization_product) = S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * mv_factor_scale_evaluation_valuefactors)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_factor. mv_factor_code_evaluation_valuefactors = ff_q_fsat_evaluation_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * mv_factor_scale_evaluation_valuefactors) + (ff_p_fsat_evaluation_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_partial. ff_h_fsat_evaluation_valuefactorsfactorization_product_partial + S (ff_r_fsat_evaluation_valuefactorsfactorization_product) = S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_partial. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (ff_r_fsat_evaluation_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_successor. ff_h_fsat_evaluation_valuefactorsfactorization_product_successor + S (ff_s_fsat_evaluation_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_successor. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (ff_s_fsat_evaluation_valuefactorsfactorization_product))) /\ ff_s_fsat_evaluation_valuefactorsfactorization_product = ff_r_fsat_evaluation_valuefactorsfactorization_product * ff_p_fsat_evaluation_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_evaluation_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_evaluation_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_evaluation_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_evaluation_valuefactorsfactorization_primes = (mv_factor_count_evaluation_valuefactors)) -> exists ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_evaluation_valuefactorsfactorization_primes)) * mv_factor_scale_evaluation_valuefactors)) /\ exists ff_q_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry. mv_factor_code_evaluation_valuefactors = ff_q_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_evaluation_valuefactorsfactorization_primes)) * mv_factor_scale_evaluation_valuefactors) + (ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_evaluation_valuefactorsparityeven. (mv_factor_count_evaluation_valuefactors) = 2 * mv_even_half_evaluation_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_evaluation_valuefactorsparityodd. (mv_factor_count_evaluation_valuefactors) = 2 * mv_odd_half_evaluation_valuefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> ((((exists mv_even_half_evaluation_resulteven. (l) = 2 * mv_even_half_evaluation_resulteven) /\ ((z) = 2))) \/ (((exists mv_odd_half_evaluation_resultodd. (l) = 2 * mv_odd_half_evaluation_resultodd + 1) /\ ((z) = 1))))

Complete tactic proof in conservative notation

All 39 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

39 script commands · 8 reading checkpoints · 1 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 (1)
mobius prime factor count unique
01Fix variables and assumptionsL1–8

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro z
  6. L6
    intro hsf
  7. L7
    intro hf
  8. L8
    intro hmu
02Separate the logical casesL9–14

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

  1. L9
    cases hmu
  2. L10
    cases hmu_right
  3. L11
    cases hmu_right_left
  4. L12
    cases hmu_right_left_left
  5. L13
    cases hmu_right_left_left_witness
  6. L14
    exfalso
03Use earlier factsL15–20

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

  1. L15
    specialize squarefree_excludes_prime_square (n)
  2. L16
    specialize squarefree_excludes_prime_square (x)
  3. L17
    apply squarefree_excludes_prime_square
  4. L18
    exact hsf
  5. L19
    exact hmu_right_left_left_witness_left
  6. L20
    exact hmu_right_left_left_witness_right
04Separate the logical casesL21–25

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

  1. L21
    cases hmu_right_right
  2. L22
    cases hmu_right_right_right
  3. L23
    cases hmu_right_right_right_witness
  4. L24
    cases hmu_right_right_right_witness_witness
  5. L25
    cases hmu_right_right_right_witness_witness_witness
05Establish heqL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius prime factor count unique.

  1. L26
    have heq : x2 = l
  2. L27
    specialize mobius_prime_factor_count_unique (n)
  3. L28
    specialize mobius_prime_factor_count_unique (x)
  4. L29
    specialize mobius_prime_factor_count_unique (x1)
  5. L30
    specialize mobius_prime_factor_count_unique (x2)
  6. L31
    specialize mobius_prime_factor_count_unique (b)
  7. L32
    specialize mobius_prime_factor_count_unique (c)
  8. L33
    specialize mobius_prime_factor_count_unique (l)
  9. L34
    apply mobius_prime_factor_count_unique
  10. L35
    exact hmu_right_right_right_witness_witness_witness_left
06Use earlier factsL36–36

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

  1. L36
    exact hf
07Calculate and transport equalitiesL37–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    rewrite heq at hmu_right_right_right_witness_witness_witness_right
  2. L38
    rewrite heq at hmu_right_right_right_witness_witness_witness_right
08Use earlier factsL39–39

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

  1. L39
    exact hmu_right_right_right_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro z
  6. 0006intro hsf
  7. 0007intro hf
  8. 0008intro hmu
  9. 0009cases hmu
  10. 0010cases hmu_right
  11. 0011cases hmu_right_left
  12. 0012cases hmu_right_left_left
  13. 0013cases hmu_right_left_left_witness
  14. 0014exfalso
  15. 0015specialize squarefree_excludes_prime_square (n)
  16. 0016specialize squarefree_excludes_prime_square (x)
  17. 0017apply squarefree_excludes_prime_square
  18. 0018exact hsf
  19. 0019exact hmu_right_left_left_witness_left
  20. 0020exact hmu_right_left_left_witness_right
  21. 0021cases hmu_right_right
  22. 0022cases hmu_right_right_right
  23. 0023cases hmu_right_right_right_witness
  24. 0024cases hmu_right_right_right_witness_witness
  25. 0025cases hmu_right_right_right_witness_witness_witness
  26. 0026have heq : x2 = l
  27. 0027specialize mobius_prime_factor_count_unique (n)
  28. 0028specialize mobius_prime_factor_count_unique (x)
  29. 0029specialize mobius_prime_factor_count_unique (x1)
  30. 0030specialize mobius_prime_factor_count_unique (x2)
  31. 0031specialize mobius_prime_factor_count_unique (b)
  32. 0032specialize mobius_prime_factor_count_unique (c)
  33. 0033specialize mobius_prime_factor_count_unique (l)
  34. 0034apply mobius_prime_factor_count_unique
  35. 0035exact hmu_right_right_right_witness_witness_witness_left
  36. 0036exact hf
  37. 0037rewrite heq at hmu_right_right_right_witness_witness_witness_right
  38. 0038rewrite heq at hmu_right_right_right_witness_witness_witness_right
  39. 0039exact hmu_right_right_right_witness_witness_witness_right