MV0005

mobius_input_positive

The independent Möbius graph explicitly excludes the infinite-divisor boundary zero.

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. ∀ z. Mobius(n,z) → ¬n = 0

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

Definition DAG

Mobius(n,z) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall n z. (((~((n) = 0)) /\ ((((exists mv_square_prime_positivesquare. ((~((mv_square_prime_positivesquare) = 1) /\ forall pvs_left_positivesquareprime pvs_right_positivesquareprime. (mv_square_prime_positivesquare) = pvs_left_positivesquareprime * pvs_right_positivesquareprime -> pvs_left_positivesquareprime = 1 \/ pvs_right_positivesquareprime = 1) /\ (exists pvs_factor_positivesquaredivisor. (n) = (mv_square_prime_positivesquare * mv_square_prime_positivesquare) * pvs_factor_positivesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_positivesquarefree. (~((sfd_prime_positivesquarefree) = 1) /\ forall pvs_left_positivesquarefreedomain pvs_right_positivesquarefreedomain. (sfd_prime_positivesquarefree) = pvs_left_positivesquarefreedomain * pvs_right_positivesquarefreedomain -> pvs_left_positivesquarefreedomain = 1 \/ pvs_right_positivesquarefreedomain = 1) -> (exists pvs_le_gap_positivesquarefreebound. pvs_le_gap_positivesquarefreebound + (sfd_prime_positivesquarefree) = (n)) -> ~(exists pvs_factor_positivesquarefreesquare. (n) = (sfd_prime_positivesquarefree * sfd_prime_positivesquarefree) * pvs_factor_positivesquarefreesquare)))) /\ (exists mv_factor_code_positivefactors mv_factor_scale_positivefactors mv_factor_count_positivefactors. (((~(n = 0) /\ ((exists ff_u_fsat_positivefactorsfactorization_product ff_v_fsat_positivefactorsfactorization_product. ((((exists ff_h_fsat_positivefactorsfactorization_product_start. ff_h_fsat_positivefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_start. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_positivefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_positivefactorsfactorization_product_terminal. ff_h_fsat_positivefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_positivefactors)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_terminal. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_terminal * S ((S (mv_factor_count_positivefactors)) * ff_v_fsat_positivefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_positivefactorsfactorization_product. (exists ff_lt_fsat_positivefactorsfactorization_product_bound. ff_lt_fsat_positivefactorsfactorization_product_bound + S ff_i_fsat_positivefactorsfactorization_product = mv_factor_count_positivefactors) -> exists ff_p_fsat_positivefactorsfactorization_product ff_r_fsat_positivefactorsfactorization_product ff_s_fsat_positivefactorsfactorization_product. ((((exists ff_h_fsat_positivefactorsfactorization_product_factor. ff_h_fsat_positivefactorsfactorization_product_factor + S (ff_p_fsat_positivefactorsfactorization_product) = S ((S (ff_i_fsat_positivefactorsfactorization_product)) * mv_factor_scale_positivefactors)) /\ exists ff_q_fsat_positivefactorsfactorization_product_factor. mv_factor_code_positivefactors = ff_q_fsat_positivefactorsfactorization_product_factor * S ((S (ff_i_fsat_positivefactorsfactorization_product)) * mv_factor_scale_positivefactors) + (ff_p_fsat_positivefactorsfactorization_product))) /\ ((((exists ff_h_fsat_positivefactorsfactorization_product_partial. ff_h_fsat_positivefactorsfactorization_product_partial + S (ff_r_fsat_positivefactorsfactorization_product) = S ((S (ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_partial. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_partial * S ((S (ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product) + (ff_r_fsat_positivefactorsfactorization_product))) /\ ((((exists ff_h_fsat_positivefactorsfactorization_product_successor. ff_h_fsat_positivefactorsfactorization_product_successor + S (ff_s_fsat_positivefactorsfactorization_product) = S ((S (S ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_successor. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_successor * S ((S (S ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product) + (ff_s_fsat_positivefactorsfactorization_product))) /\ ff_s_fsat_positivefactorsfactorization_product = ff_r_fsat_positivefactorsfactorization_product * ff_p_fsat_positivefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_positivefactorsfactorization_primes. (exists ftsf_gap_fsat_positivefactorsfactorization_primes_bound. ftsf_gap_fsat_positivefactorsfactorization_primes_bound + S ftsf_index_fsat_positivefactorsfactorization_primes = (mv_factor_count_positivefactors)) -> exists ftsf_factor_fsat_positivefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_positivefactorsfactorization_primes_entry. ff_h_ftsf_fsat_positivefactorsfactorization_primes_entry + S (ftsf_factor_fsat_positivefactorsfactorization_primes) = S ((S (ftsf_index_fsat_positivefactorsfactorization_primes)) * mv_factor_scale_positivefactors)) /\ exists ff_q_ftsf_fsat_positivefactorsfactorization_primes_entry. mv_factor_code_positivefactors = ff_q_ftsf_fsat_positivefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_positivefactorsfactorization_primes)) * mv_factor_scale_positivefactors) + (ftsf_factor_fsat_positivefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_positivefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_positivefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_positivefactorsfactorization_primes_prime. ftsf_factor_fsat_positivefactorsfactorization_primes = frm_prime_left_ftsf_fsat_positivefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_positivefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_positivefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_positivefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_positivefactorsparityeven. (mv_factor_count_positivefactors) = 2 * mv_even_half_positivefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_positivefactorsparityodd. (mv_factor_count_positivefactors) = 2 * mv_odd_half_positivefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> ~(n = 0)

Complete tactic proof in conservative notation

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

5 script commands · 3 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro z
  3. L3
    intro h
02Separate the logical casesL4–4

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

  1. L4
    cases h
03Use earlier factsL5–5

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

  1. L5
    exact h_left

Library-wide reading audit

Original defined command ledger · 5 lines
  1. 0001intro n
  2. 0002intro z
  3. 0003intro h
  4. 0004cases h
  5. 0005exact h_left