MV0014

mobius_prime_square_value_zero

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 22 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

MV000B mobius_value_functional MV0007 mobius_from_prime_square MV0005 mobius_input_positive

Direct dependents

MV0015 mobius_fresh_prime_negates

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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