MV0014

mobius_prime_square_value_zero

Every independently defined Möbius value at an actual prime-square multiple is the canonical zero code.

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. ∀ p. ∀ z. Prime(p) → Dvd(p · p,n) → Mobius(n,z) → z = 0

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

Definition DAG

Mobius(n,z) · 1Dvd(d,n) · 1Prime(p) · 1

Actual proof prerequisites

mobius_value_functionalmobius_from_prime_squaremobius_input_positive
Original expanded first-order statement 
forall n p z. (~((p) = 1) /\ forall pvs_left_square_value_prime pvs_right_square_value_prime. (p) = pvs_left_square_value_prime * pvs_right_square_value_prime -> pvs_left_square_value_prime = 1 \/ pvs_right_square_value_prime = 1) -> (exists pvs_factor_square_value_divisor. (n) = (p * p) * pvs_factor_square_value_divisor) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_square_value_inputsquare. ((~((mv_square_prime_square_value_inputsquare) = 1) /\ forall pvs_left_square_value_inputsquareprime pvs_right_square_value_inputsquareprime. (mv_square_prime_square_value_inputsquare) = pvs_left_square_value_inputsquareprime * pvs_right_square_value_inputsquareprime -> pvs_left_square_value_inputsquareprime = 1 \/ pvs_right_square_value_inputsquareprime = 1) /\ (exists pvs_factor_square_value_inputsquaredivisor. (n) = (mv_square_prime_square_value_inputsquare * mv_square_prime_square_value_inputsquare) * pvs_factor_square_value_inputsquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_square_value_inputsquarefree. (~((sfd_prime_square_value_inputsquarefree) = 1) /\ forall pvs_left_square_value_inputsquarefreedomain pvs_right_square_value_inputsquarefreedomain. (sfd_prime_square_value_inputsquarefree) = pvs_left_square_value_inputsquarefreedomain * pvs_right_square_value_inputsquarefreedomain -> pvs_left_square_value_inputsquarefreedomain = 1 \/ pvs_right_square_value_inputsquarefreedomain = 1) -> (exists pvs_le_gap_square_value_inputsquarefreebound. pvs_le_gap_square_value_inputsquarefreebound + (sfd_prime_square_value_inputsquarefree) = (n)) -> ~(exists pvs_factor_square_value_inputsquarefreesquare. (n) = (sfd_prime_square_value_inputsquarefree * sfd_prime_square_value_inputsquarefree) * pvs_factor_square_value_inputsquarefreesquare)))) /\ (exists mv_factor_code_square_value_inputfactors mv_factor_scale_square_value_inputfactors mv_factor_count_square_value_inputfactors. (((~(n = 0) /\ ((exists ff_u_fsat_square_value_inputfactorsfactorization_product ff_v_fsat_square_value_inputfactorsfactorization_product. ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_start. ff_h_fsat_square_value_inputfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_start. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_terminal. ff_h_fsat_square_value_inputfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_square_value_inputfactors)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_terminal. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_terminal * S ((S (mv_factor_count_square_value_inputfactors)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_square_value_inputfactorsfactorization_product. (exists ff_lt_fsat_square_value_inputfactorsfactorization_product_bound. ff_lt_fsat_square_value_inputfactorsfactorization_product_bound + S ff_i_fsat_square_value_inputfactorsfactorization_product = mv_factor_count_square_value_inputfactors) -> exists ff_p_fsat_square_value_inputfactorsfactorization_product ff_r_fsat_square_value_inputfactorsfactorization_product ff_s_fsat_square_value_inputfactorsfactorization_product. ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_factor. ff_h_fsat_square_value_inputfactorsfactorization_product_factor + S (ff_p_fsat_square_value_inputfactorsfactorization_product) = S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * mv_factor_scale_square_value_inputfactors)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_factor. mv_factor_code_square_value_inputfactors = ff_q_fsat_square_value_inputfactorsfactorization_product_factor * S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * mv_factor_scale_square_value_inputfactors) + (ff_p_fsat_square_value_inputfactorsfactorization_product))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_partial. ff_h_fsat_square_value_inputfactorsfactorization_product_partial + S (ff_r_fsat_square_value_inputfactorsfactorization_product) = S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_partial. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_partial * S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (ff_r_fsat_square_value_inputfactorsfactorization_product))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_successor. ff_h_fsat_square_value_inputfactorsfactorization_product_successor + S (ff_s_fsat_square_value_inputfactorsfactorization_product) = S ((S (S ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_successor. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_successor * S ((S (S ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (ff_s_fsat_square_value_inputfactorsfactorization_product))) /\ ff_s_fsat_square_value_inputfactorsfactorization_product = ff_r_fsat_square_value_inputfactorsfactorization_product * ff_p_fsat_square_value_inputfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_square_value_inputfactorsfactorization_primes. (exists ftsf_gap_fsat_square_value_inputfactorsfactorization_primes_bound. ftsf_gap_fsat_square_value_inputfactorsfactorization_primes_bound + S ftsf_index_fsat_square_value_inputfactorsfactorization_primes = (mv_factor_count_square_value_inputfactors)) -> exists ftsf_factor_fsat_square_value_inputfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry. ff_h_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry + S (ftsf_factor_fsat_square_value_inputfactorsfactorization_primes) = S ((S (ftsf_index_fsat_square_value_inputfactorsfactorization_primes)) * mv_factor_scale_square_value_inputfactors)) /\ exists ff_q_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry. mv_factor_code_square_value_inputfactors = ff_q_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_square_value_inputfactorsfactorization_primes)) * mv_factor_scale_square_value_inputfactors) + (ftsf_factor_fsat_square_value_inputfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_square_value_inputfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime. ftsf_factor_fsat_square_value_inputfactorsfactorization_primes = frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_square_value_inputfactorsparityeven. (mv_factor_count_square_value_inputfactors) = 2 * mv_even_half_square_value_inputfactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_square_value_inputfactorsparityodd. (mv_factor_count_square_value_inputfactors) = 2 * mv_odd_half_square_value_inputfactorsparityodd + 1) /\ ((z) = 1))))))))))) -> z = 0

Complete tactic proof in conservative notation

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

22 script commands · 4 reading checkpoints · 0 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)
mobius value functionalmobius from prime squaremobius input positive
01Fix variables and assumptionsL1–6

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro z
  4. L4
    intro hp
  5. L5
    intro hdiv
  6. L6
    intro hmu
02Use earlier factsL7–14

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

  1. L7
    specialize mobius_value_functional (n)
  2. L8
    specialize mobius_value_functional (z)
  3. L9
    specialize mobius_value_functional (0)
  4. L10
    apply mobius_value_functional
  5. L11
    exact hmu
  6. L12
    specialize mobius_from_prime_square (n)
  7. L13
    specialize mobius_from_prime_square (p)
  8. L14
    apply mobius_from_prime_square
03Fix variables and assumptionsL15–15

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

  1. L15
    intro hz
04Use earlier factsL16–22

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

  1. L16
    specialize mobius_input_positive (n)
  2. L17
    specialize mobius_input_positive (z)
  3. L18
    apply mobius_input_positive
  4. L19
    exact hmu
  5. L20
    exact hz
  6. L21
    exact hp
  7. L22
    exact hdiv

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro z
  4. 0004intro hp
  5. 0005intro hdiv
  6. 0006intro hmu
  7. 0007specialize mobius_value_functional (n)
  8. 0008specialize mobius_value_functional (z)
  9. 0009specialize mobius_value_functional (0)
  10. 0010apply mobius_value_functional
  11. 0011exact hmu
  12. 0012specialize mobius_from_prime_square (n)
  13. 0013specialize mobius_from_prime_square (p)
  14. 0014apply mobius_from_prime_square
  15. 0015intro hz
  16. 0016specialize mobius_input_positive (n)
  17. 0017specialize mobius_input_positive (z)
  18. 0018apply mobius_input_positive
  19. 0019exact hmu
  20. 0020exact hz
  21. 0021exact hp
  22. 0022exact hdiv