MV0005

mobius_input_positive

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.

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

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

Mobius(n,z) is defined only for positive n. The canonical signed codes are 0 for zero, 2 for +1, and 1 for −1. The function is defined independently of any divisor-sum identity. These values and prime-step lemmas are prerequisites for G007; divisor-sum cancellation and full Möbius inversion remain open in this checkpoint. No signed-table proof is included here.

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