MV0009

mobius_value_exists

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.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

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

Exact expanded first-order arithmetic 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)))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 37 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

squarefree_or_prime_square_divisor Alpha theorem; checked-use authorized foundation_prime_factor_list_exists Alpha theorem; checked-use authorized MV0001 alternating_signed_unit_exists MV0008 mobius_from_squarefree_factor_count MV0007 mobius_from_prime_square

Direct dependents

MV000C mobius_value_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

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.

Named ingredients (3)
alternating signed unit existsmobius from squarefree factor countmobius from prime square

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: SquarefreeHasPrimeSquareDivisor
  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
  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 : exists z. ((((exists mv_even_half_exists_signeven. (x) = 2 * mv_even_half_exists_signeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_exists_signodd. (x) = 2 * mv_odd_half_exists_signodd + 1) /\ ((z) = 1))))
  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 exact command ledger · 37 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hcase : (((~((n) = 0)) /\ (forall sfd_prime_exists_decision. (~((sfd_prime_exists_decision) = 1) /\ forall pvs_left_exists_decisiondomain pvs_right_exists_decisiondomain. (sfd_prime_exists_decision) = pvs_left_exists_decisiondomain * pvs_right_exists_decisiondomain -> pvs_left_exists_decisiondomain = 1 \/ pvs_right_exists_decisiondomain = 1) -> (exists pvs_le_gap_exists_decisionbound. pvs_le_gap_exists_decisionbound + (sfd_prime_exists_decision) = (n)) -> ~(exists pvs_factor_exists_decisionsquare. (n) = (sfd_prime_exists_decision * sfd_prime_exists_decision) * pvs_factor_exists_decisionsquare)))) \/ exists p. (~((p) = 1) /\ forall pvs_left_exists_prime pvs_right_exists_prime. (p) = pvs_left_exists_prime * pvs_right_exists_prime -> pvs_left_exists_prime = 1 \/ pvs_right_exists_prime = 1) /\ (exists pvs_factor_exists_square. (n) = (p * p) * pvs_factor_exists_square)
  4. 0004specialize squarefree_or_prime_square_divisor (n)
  5. 0005apply squarefree_or_prime_square_divisor
  6. 0006exact hn
  7. 0007cases hcase
  8. 0008have hf : exists l b c. ((~(n = 0) /\ ((exists ff_u_fsat_mv_exists_factors_product ff_v_fsat_mv_exists_factors_product. ((((exists ff_h_fsat_mv_exists_factors_product_start. ff_h_fsat_mv_exists_factors_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_exists_factors_product)) /\ exists ff_q_fsat_mv_exists_factors_product_start. ff_u_fsat_mv_exists_factors_product = ff_q_fsat_mv_exists_factors_product_start * S ((S (0)) * ff_v_fsat_mv_exists_factors_product) + (1))) /\ ((((exists ff_h_fsat_mv_exists_factors_product_terminal. ff_h_fsat_mv_exists_factors_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mv_exists_factors_product)) /\ exists ff_q_fsat_mv_exists_factors_product_terminal. ff_u_fsat_mv_exists_factors_product = ff_q_fsat_mv_exists_factors_product_terminal * S ((S (l)) * ff_v_fsat_mv_exists_factors_product) + (n))) /\ forall ff_i_fsat_mv_exists_factors_product. (exists ff_lt_fsat_mv_exists_factors_product_bound. ff_lt_fsat_mv_exists_factors_product_bound + S ff_i_fsat_mv_exists_factors_product = l) -> exists ff_p_fsat_mv_exists_factors_product ff_r_fsat_mv_exists_factors_product ff_s_fsat_mv_exists_factors_product. ((((exists ff_h_fsat_mv_exists_factors_product_factor. ff_h_fsat_mv_exists_factors_product_factor + S (ff_p_fsat_mv_exists_factors_product) = S ((S (ff_i_fsat_mv_exists_factors_product)) * c)) /\ exists ff_q_fsat_mv_exists_factors_product_factor. b = ff_q_fsat_mv_exists_factors_product_factor * S ((S (ff_i_fsat_mv_exists_factors_product)) * c) + (ff_p_fsat_mv_exists_factors_product))) /\ ((((exists ff_h_fsat_mv_exists_factors_product_partial. ff_h_fsat_mv_exists_factors_product_partial + S (ff_r_fsat_mv_exists_factors_product) = S ((S (ff_i_fsat_mv_exists_factors_product)) * ff_v_fsat_mv_exists_factors_product)) /\ exists ff_q_fsat_mv_exists_factors_product_partial. ff_u_fsat_mv_exists_factors_product = ff_q_fsat_mv_exists_factors_product_partial * S ((S (ff_i_fsat_mv_exists_factors_product)) * ff_v_fsat_mv_exists_factors_product) + (ff_r_fsat_mv_exists_factors_product))) /\ ((((exists ff_h_fsat_mv_exists_factors_product_successor. ff_h_fsat_mv_exists_factors_product_successor + S (ff_s_fsat_mv_exists_factors_product) = S ((S (S ff_i_fsat_mv_exists_factors_product)) * ff_v_fsat_mv_exists_factors_product)) /\ exists ff_q_fsat_mv_exists_factors_product_successor. ff_u_fsat_mv_exists_factors_product = ff_q_fsat_mv_exists_factors_product_successor * S ((S (S ff_i_fsat_mv_exists_factors_product)) * ff_v_fsat_mv_exists_factors_product) + (ff_s_fsat_mv_exists_factors_product))) /\ ff_s_fsat_mv_exists_factors_product = ff_r_fsat_mv_exists_factors_product * ff_p_fsat_mv_exists_factors_product)))))) /\ (forall ftsf_index_fsat_mv_exists_factors_primes. (exists ftsf_gap_fsat_mv_exists_factors_primes_bound. ftsf_gap_fsat_mv_exists_factors_primes_bound + S ftsf_index_fsat_mv_exists_factors_primes = (l)) -> exists ftsf_factor_fsat_mv_exists_factors_primes. ((((exists ff_h_ftsf_fsat_mv_exists_factors_primes_entry. ff_h_ftsf_fsat_mv_exists_factors_primes_entry + S (ftsf_factor_fsat_mv_exists_factors_primes) = S ((S (ftsf_index_fsat_mv_exists_factors_primes)) * c)) /\ exists ff_q_ftsf_fsat_mv_exists_factors_primes_entry. b = ff_q_ftsf_fsat_mv_exists_factors_primes_entry * S ((S (ftsf_index_fsat_mv_exists_factors_primes)) * c) + (ftsf_factor_fsat_mv_exists_factors_primes))) /\ ((~(ftsf_factor_fsat_mv_exists_factors_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_exists_factors_primes_prime frm_prime_right_ftsf_fsat_mv_exists_factors_primes_prime. ftsf_factor_fsat_mv_exists_factors_primes = frm_prime_left_ftsf_fsat_mv_exists_factors_primes_prime * frm_prime_right_ftsf_fsat_mv_exists_factors_primes_prime -> frm_prime_left_ftsf_fsat_mv_exists_factors_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_exists_factors_primes_prime = 1)))))))
  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 : exists z. ((((exists mv_even_half_exists_signeven. (x) = 2 * mv_even_half_exists_signeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_exists_signodd. (x) = 2 * mv_odd_half_exists_signodd + 1) /\ ((z) = 1))))
  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