MV000B

mobius_value_functional

Möbius values have literally unique canonical signed codes; square-divisor and squarefree branches are disjoint by proof.

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. ∀ a. ∀ b. Mobius(n,a) → Mobius(n,b) → a = b

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

Definition DAG

AlternatingSignedUnit(n,z) · 1Mobius(n,z) · 2

Actual proof prerequisites

squarefree_excludes_prime_square · checked external prerequisitemobius_squarefree_evaluationalternating_signed_unit_functional
Original expanded first-order statement 
forall n a b. (((~((n) = 0)) /\ ((((exists mv_square_prime_functional_firstsquare. ((~((mv_square_prime_functional_firstsquare) = 1) /\ forall pvs_left_functional_firstsquareprime pvs_right_functional_firstsquareprime. (mv_square_prime_functional_firstsquare) = pvs_left_functional_firstsquareprime * pvs_right_functional_firstsquareprime -> pvs_left_functional_firstsquareprime = 1 \/ pvs_right_functional_firstsquareprime = 1) /\ (exists pvs_factor_functional_firstsquaredivisor. (n) = (mv_square_prime_functional_firstsquare * mv_square_prime_functional_firstsquare) * pvs_factor_functional_firstsquaredivisor))) /\ ((a) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_functional_firstsquarefree. (~((sfd_prime_functional_firstsquarefree) = 1) /\ forall pvs_left_functional_firstsquarefreedomain pvs_right_functional_firstsquarefreedomain. (sfd_prime_functional_firstsquarefree) = pvs_left_functional_firstsquarefreedomain * pvs_right_functional_firstsquarefreedomain -> pvs_left_functional_firstsquarefreedomain = 1 \/ pvs_right_functional_firstsquarefreedomain = 1) -> (exists pvs_le_gap_functional_firstsquarefreebound. pvs_le_gap_functional_firstsquarefreebound + (sfd_prime_functional_firstsquarefree) = (n)) -> ~(exists pvs_factor_functional_firstsquarefreesquare. (n) = (sfd_prime_functional_firstsquarefree * sfd_prime_functional_firstsquarefree) * pvs_factor_functional_firstsquarefreesquare)))) /\ (exists mv_factor_code_functional_firstfactors mv_factor_scale_functional_firstfactors mv_factor_count_functional_firstfactors. (((~(n = 0) /\ ((exists ff_u_fsat_functional_firstfactorsfactorization_product ff_v_fsat_functional_firstfactorsfactorization_product. ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_start. ff_h_fsat_functional_firstfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_start. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_terminal. ff_h_fsat_functional_firstfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_functional_firstfactors)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_terminal. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_terminal * S ((S (mv_factor_count_functional_firstfactors)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_functional_firstfactorsfactorization_product. (exists ff_lt_fsat_functional_firstfactorsfactorization_product_bound. ff_lt_fsat_functional_firstfactorsfactorization_product_bound + S ff_i_fsat_functional_firstfactorsfactorization_product = mv_factor_count_functional_firstfactors) -> exists ff_p_fsat_functional_firstfactorsfactorization_product ff_r_fsat_functional_firstfactorsfactorization_product ff_s_fsat_functional_firstfactorsfactorization_product. ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_factor. ff_h_fsat_functional_firstfactorsfactorization_product_factor + S (ff_p_fsat_functional_firstfactorsfactorization_product) = S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * mv_factor_scale_functional_firstfactors)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_factor. mv_factor_code_functional_firstfactors = ff_q_fsat_functional_firstfactorsfactorization_product_factor * S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * mv_factor_scale_functional_firstfactors) + (ff_p_fsat_functional_firstfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_partial. ff_h_fsat_functional_firstfactorsfactorization_product_partial + S (ff_r_fsat_functional_firstfactorsfactorization_product) = S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_partial. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_partial * S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (ff_r_fsat_functional_firstfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_successor. ff_h_fsat_functional_firstfactorsfactorization_product_successor + S (ff_s_fsat_functional_firstfactorsfactorization_product) = S ((S (S ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_successor. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_successor * S ((S (S ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (ff_s_fsat_functional_firstfactorsfactorization_product))) /\ ff_s_fsat_functional_firstfactorsfactorization_product = ff_r_fsat_functional_firstfactorsfactorization_product * ff_p_fsat_functional_firstfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_functional_firstfactorsfactorization_primes. (exists ftsf_gap_fsat_functional_firstfactorsfactorization_primes_bound. ftsf_gap_fsat_functional_firstfactorsfactorization_primes_bound + S ftsf_index_fsat_functional_firstfactorsfactorization_primes = (mv_factor_count_functional_firstfactors)) -> exists ftsf_factor_fsat_functional_firstfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_functional_firstfactorsfactorization_primes_entry. ff_h_ftsf_fsat_functional_firstfactorsfactorization_primes_entry + S (ftsf_factor_fsat_functional_firstfactorsfactorization_primes) = S ((S (ftsf_index_fsat_functional_firstfactorsfactorization_primes)) * mv_factor_scale_functional_firstfactors)) /\ exists ff_q_ftsf_fsat_functional_firstfactorsfactorization_primes_entry. mv_factor_code_functional_firstfactors = ff_q_ftsf_fsat_functional_firstfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_functional_firstfactorsfactorization_primes)) * mv_factor_scale_functional_firstfactors) + (ftsf_factor_fsat_functional_firstfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_functional_firstfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_functional_firstfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_functional_firstfactorsfactorization_primes_prime. ftsf_factor_fsat_functional_firstfactorsfactorization_primes = frm_prime_left_ftsf_fsat_functional_firstfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_functional_firstfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_functional_firstfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_functional_firstfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_functional_firstfactorsparityeven. (mv_factor_count_functional_firstfactors) = 2 * mv_even_half_functional_firstfactorsparityeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_functional_firstfactorsparityodd. (mv_factor_count_functional_firstfactors) = 2 * mv_odd_half_functional_firstfactorsparityodd + 1) /\ ((a) = 1))))))))))) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_functional_secondsquare. ((~((mv_square_prime_functional_secondsquare) = 1) /\ forall pvs_left_functional_secondsquareprime pvs_right_functional_secondsquareprime. (mv_square_prime_functional_secondsquare) = pvs_left_functional_secondsquareprime * pvs_right_functional_secondsquareprime -> pvs_left_functional_secondsquareprime = 1 \/ pvs_right_functional_secondsquareprime = 1) /\ (exists pvs_factor_functional_secondsquaredivisor. (n) = (mv_square_prime_functional_secondsquare * mv_square_prime_functional_secondsquare) * pvs_factor_functional_secondsquaredivisor))) /\ ((b) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_functional_secondsquarefree. (~((sfd_prime_functional_secondsquarefree) = 1) /\ forall pvs_left_functional_secondsquarefreedomain pvs_right_functional_secondsquarefreedomain. (sfd_prime_functional_secondsquarefree) = pvs_left_functional_secondsquarefreedomain * pvs_right_functional_secondsquarefreedomain -> pvs_left_functional_secondsquarefreedomain = 1 \/ pvs_right_functional_secondsquarefreedomain = 1) -> (exists pvs_le_gap_functional_secondsquarefreebound. pvs_le_gap_functional_secondsquarefreebound + (sfd_prime_functional_secondsquarefree) = (n)) -> ~(exists pvs_factor_functional_secondsquarefreesquare. (n) = (sfd_prime_functional_secondsquarefree * sfd_prime_functional_secondsquarefree) * pvs_factor_functional_secondsquarefreesquare)))) /\ (exists mv_factor_code_functional_secondfactors mv_factor_scale_functional_secondfactors mv_factor_count_functional_secondfactors. (((~(n = 0) /\ ((exists ff_u_fsat_functional_secondfactorsfactorization_product ff_v_fsat_functional_secondfactorsfactorization_product. ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_start. ff_h_fsat_functional_secondfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_start. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_terminal. ff_h_fsat_functional_secondfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_functional_secondfactors)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_terminal. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_terminal * S ((S (mv_factor_count_functional_secondfactors)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_functional_secondfactorsfactorization_product. (exists ff_lt_fsat_functional_secondfactorsfactorization_product_bound. ff_lt_fsat_functional_secondfactorsfactorization_product_bound + S ff_i_fsat_functional_secondfactorsfactorization_product = mv_factor_count_functional_secondfactors) -> exists ff_p_fsat_functional_secondfactorsfactorization_product ff_r_fsat_functional_secondfactorsfactorization_product ff_s_fsat_functional_secondfactorsfactorization_product. ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_factor. ff_h_fsat_functional_secondfactorsfactorization_product_factor + S (ff_p_fsat_functional_secondfactorsfactorization_product) = S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * mv_factor_scale_functional_secondfactors)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_factor. mv_factor_code_functional_secondfactors = ff_q_fsat_functional_secondfactorsfactorization_product_factor * S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * mv_factor_scale_functional_secondfactors) + (ff_p_fsat_functional_secondfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_partial. ff_h_fsat_functional_secondfactorsfactorization_product_partial + S (ff_r_fsat_functional_secondfactorsfactorization_product) = S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_partial. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_partial * S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (ff_r_fsat_functional_secondfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_successor. ff_h_fsat_functional_secondfactorsfactorization_product_successor + S (ff_s_fsat_functional_secondfactorsfactorization_product) = S ((S (S ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_successor. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_successor * S ((S (S ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (ff_s_fsat_functional_secondfactorsfactorization_product))) /\ ff_s_fsat_functional_secondfactorsfactorization_product = ff_r_fsat_functional_secondfactorsfactorization_product * ff_p_fsat_functional_secondfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_functional_secondfactorsfactorization_primes. (exists ftsf_gap_fsat_functional_secondfactorsfactorization_primes_bound. ftsf_gap_fsat_functional_secondfactorsfactorization_primes_bound + S ftsf_index_fsat_functional_secondfactorsfactorization_primes = (mv_factor_count_functional_secondfactors)) -> exists ftsf_factor_fsat_functional_secondfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_functional_secondfactorsfactorization_primes_entry. ff_h_ftsf_fsat_functional_secondfactorsfactorization_primes_entry + S (ftsf_factor_fsat_functional_secondfactorsfactorization_primes) = S ((S (ftsf_index_fsat_functional_secondfactorsfactorization_primes)) * mv_factor_scale_functional_secondfactors)) /\ exists ff_q_ftsf_fsat_functional_secondfactorsfactorization_primes_entry. mv_factor_code_functional_secondfactors = ff_q_ftsf_fsat_functional_secondfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_functional_secondfactorsfactorization_primes)) * mv_factor_scale_functional_secondfactors) + (ftsf_factor_fsat_functional_secondfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_functional_secondfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_functional_secondfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_functional_secondfactorsfactorization_primes_prime. ftsf_factor_fsat_functional_secondfactorsfactorization_primes = frm_prime_left_ftsf_fsat_functional_secondfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_functional_secondfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_functional_secondfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_functional_secondfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_functional_secondfactorsparityeven. (mv_factor_count_functional_secondfactors) = 2 * mv_even_half_functional_secondfactorsparityeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_functional_secondfactorsparityodd. (mv_factor_count_functional_secondfactors) = 2 * mv_odd_half_functional_secondfactorsparityodd + 1) /\ ((b) = 1))))))))))) -> a = b

Complete tactic proof in conservative notation

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

46 script commands · 11 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 (2)
mobius squarefree evaluationalternating signed unit functional
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro ha
  5. L5
    intro hb
02Separate the logical casesL6–11

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

  1. L6
    cases ha
  2. L7
    cases ha_right
  3. L8
    cases ha_right_left
  4. L9
    cases hb
  5. L10
    cases hb_right
  6. L11
    cases hb_right_left
03Calculate and transport equalitiesL12–12

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

  1. L12
    trans 0
04Use earlier factsL13–13

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

  1. L13
    exact ha_right_left_right
05Calculate and transport equalitiesL14–14

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

  1. L14
    symm
06Use earlier factsL15–15

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

  1. L15
    exact hb_right_left_right
07Separate the logical casesL16–19

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

  1. L16
    cases hb_right_right
  2. L17
    cases ha_right_left_left
  3. L18
    cases ha_right_left_left_witness
  4. L19
    exfalso
08Use earlier factsL20–25

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

  1. L20
    specialize squarefree_excludes_prime_square (n)
  2. L21
    specialize squarefree_excludes_prime_square (x)
  3. L22
    apply squarefree_excludes_prime_square
  4. L23
    exact hb_right_right_left
  5. L24
    exact ha_right_left_left_witness_left
  6. L25
    exact ha_right_left_left_witness_right
09Separate the logical casesL26–30

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

  1. L26
    cases ha_right_right
  2. L27
    cases ha_right_right_right
  3. L28
    cases ha_right_right_right_witness
  4. L29
    cases ha_right_right_right_witness_witness
  5. L30
    cases ha_right_right_right_witness_witness_witness
10Establish hsL31–40

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius squarefree evaluation.

  1. L31
    have hs : AlternatingSignedUnit(x2,b)Definitions: AlternatingSignedUnit(x2,b)Original native command in the exact edition
  2. L32
    specialize mobius_squarefree_evaluation (n)
  3. L33
    specialize mobius_squarefree_evaluation (x)
  4. L34
    specialize mobius_squarefree_evaluation (x1)
  5. L35
    specialize mobius_squarefree_evaluation (x2)
  6. L36
    specialize mobius_squarefree_evaluation (b)
  7. L37
    apply mobius_squarefree_evaluation
  8. L38
    exact ha_right_right_left
  9. L39
    exact ha_right_right_right_witness_witness_witness_left
  10. L40
    exact hb
11Use earlier factsL41–46

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

  1. L41
    specialize alternating_signed_unit_functional (x2)
  2. L42
    specialize alternating_signed_unit_functional (a)
  3. L43
    specialize alternating_signed_unit_functional (b)
  4. L44
    apply alternating_signed_unit_functional
  5. L45
    exact ha_right_right_right_witness_witness_witness_right
  6. L46
    exact hs

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro ha
  5. 0005intro hb
  6. 0006cases ha
  7. 0007cases ha_right
  8. 0008cases ha_right_left
  9. 0009cases hb
  10. 0010cases hb_right
  11. 0011cases hb_right_left
  12. 0012trans 0
  13. 0013exact ha_right_left_right
  14. 0014symm
  15. 0015exact hb_right_left_right
  16. 0016cases hb_right_right
  17. 0017cases ha_right_left_left
  18. 0018cases ha_right_left_left_witness
  19. 0019exfalso
  20. 0020specialize squarefree_excludes_prime_square (n)
  21. 0021specialize squarefree_excludes_prime_square (x)
  22. 0022apply squarefree_excludes_prime_square
  23. 0023exact hb_right_right_left
  24. 0024exact ha_right_left_left_witness_left
  25. 0025exact ha_right_left_left_witness_right
  26. 0026cases ha_right_right
  27. 0027cases ha_right_right_right
  28. 0028cases ha_right_right_right_witness
  29. 0029cases ha_right_right_right_witness_witness
  30. 0030cases ha_right_right_right_witness_witness_witness
  31. 0031have hs : AlternatingSignedUnit(x2,b)
  32. 0032specialize mobius_squarefree_evaluation (n)
  33. 0033specialize mobius_squarefree_evaluation (x)
  34. 0034specialize mobius_squarefree_evaluation (x1)
  35. 0035specialize mobius_squarefree_evaluation (x2)
  36. 0036specialize mobius_squarefree_evaluation (b)
  37. 0037apply mobius_squarefree_evaluation
  38. 0038exact ha_right_right_left
  39. 0039exact ha_right_right_right_witness_witness_witness_left
  40. 0040exact hb
  41. 0041specialize alternating_signed_unit_functional (x2)
  42. 0042specialize alternating_signed_unit_functional (a)
  43. 0043specialize alternating_signed_unit_functional (b)
  44. 0044apply alternating_signed_unit_functional
  45. 0045exact ha_right_right_right_witness_witness_witness_right
  46. 0046exact hs