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 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)Constructive proof overview
Generated structural guide
The independent Möbius graph explicitly excludes the infinite-divisor boundary zero.
The unchanged tactic script uses 0 declared prerequisites and contains 5 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
none
Direct dependents
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
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.