PV000F

prime_valuation_support_one

One has the actual empty distinct-prime support and empty product one, with no fictitious prime or positive valuation.

Alpha v34 checked-use · first admitted v29 · 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. Exact original first-admission records.

This is a shared constructive tool, not an additional major blueprint goal. The list covers every prime divisor, has no repeated primes, and contains actual prime-power values. One uses the empty support; zero is excluded.

Exact theorem in conservative defined notation

PrimeValuationSupport(1,0,0,0,0,0,0,0)

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

Definition DAG

PrimeValuationSupport(n,pb,pc,eb,ec,vb,vc,l) · 1Product(b,c,l,z) · 1

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisitedivisor_one · checked external prerequisitefactor_permutation_product_exists · checked external prerequisitebeta_product_zero · checked external prerequisite
Original expanded first-order statement 
((~((1) = 0)) /\ (((forall pfp_i_pvs_unit_supportdistinct pfp_j_pvs_unit_supportdistinct pfp_a_pvs_unit_supportdistinct. (exists pfp_gap_pvs_unit_supportdistinctfirst. pfp_gap_pvs_unit_supportdistinctfirst + S (pfp_i_pvs_unit_supportdistinct) = (0)) -> (exists pfp_gap_pvs_unit_supportdistinctsecond. pfp_gap_pvs_unit_supportdistinctsecond + S (pfp_j_pvs_unit_supportdistinct) = (0)) -> (((exists ff_h_pfp_pvs_unit_supportdistinctleft. ff_h_pfp_pvs_unit_supportdistinctleft + S (pfp_a_pvs_unit_supportdistinct) = S ((S (pfp_i_pvs_unit_supportdistinct)) * 0)) /\ exists ff_q_pfp_pvs_unit_supportdistinctleft. 0 = ff_q_pfp_pvs_unit_supportdistinctleft * S ((S (pfp_i_pvs_unit_supportdistinct)) * 0) + (pfp_a_pvs_unit_supportdistinct))) -> (((exists ff_h_pfp_pvs_unit_supportdistinctright. ff_h_pfp_pvs_unit_supportdistinctright + S (pfp_a_pvs_unit_supportdistinct) = S ((S (pfp_j_pvs_unit_supportdistinct)) * 0)) /\ exists ff_q_pfp_pvs_unit_supportdistinctright. 0 = ff_q_pfp_pvs_unit_supportdistinctright * S ((S (pfp_j_pvs_unit_supportdistinct)) * 0) + (pfp_a_pvs_unit_supportdistinct))) -> pfp_i_pvs_unit_supportdistinct = pfp_j_pvs_unit_supportdistinct) /\ (((forall pvs_index_unit_supportentries. (exists pvs_gap_unit_supportentriesindex. pvs_gap_unit_supportentriesindex + S (pvs_index_unit_supportentries) = (0)) -> exists pvs_prime_unit_supportentries pvs_exponent_unit_supportentries pvs_power_unit_supportentries. (((((exists ff_h_pvs_unit_supportentriesprime. ff_h_pvs_unit_supportentriesprime + S (pvs_prime_unit_supportentries) = S ((S (pvs_index_unit_supportentries)) * 0)) /\ exists ff_q_pvs_unit_supportentriesprime. 0 = ff_q_pvs_unit_supportentriesprime * S ((S (pvs_index_unit_supportentries)) * 0) + (pvs_prime_unit_supportentries))) /\ (((((exists ff_h_pvs_unit_supportentriesexponent. ff_h_pvs_unit_supportentriesexponent + S (pvs_exponent_unit_supportentries) = S ((S (pvs_index_unit_supportentries)) * 0)) /\ exists ff_q_pvs_unit_supportentriesexponent. 0 = ff_q_pvs_unit_supportentriesexponent * S ((S (pvs_index_unit_supportentries)) * 0) + (pvs_exponent_unit_supportentries))) /\ (((((exists ff_h_pvs_unit_supportentriespower. ff_h_pvs_unit_supportentriespower + S (pvs_power_unit_supportentries) = S ((S (pvs_index_unit_supportentries)) * 0)) /\ exists ff_q_pvs_unit_supportentriespower. 0 = ff_q_pvs_unit_supportentriespower * S ((S (pvs_index_unit_supportentries)) * 0) + (pvs_power_unit_supportentries))) /\ (((~((pvs_prime_unit_supportentries) = 1) /\ forall pvs_left_unit_supportentriesdomain pvs_right_unit_supportentriesdomain. (pvs_prime_unit_supportentries) = pvs_left_unit_supportentriesdomain * pvs_right_unit_supportentriesdomain -> pvs_left_unit_supportentriesdomain = 1 \/ pvs_right_unit_supportentriesdomain = 1) /\ (((~(pvs_exponent_unit_supportentries = 0)) /\ (((((exists bpd_gap_pvs_unit_supportentriesvaluation_selected_bound. bpd_gap_pvs_unit_supportentriesvaluation_selected_bound + (pvs_exponent_unit_supportentries) = (1)) /\ (exists bpvi_result_pvs_unit_supportentriesvaluation_selected. ((exists bpvi_b_pvs_unit_supportentriesvaluation_selected_power bpvi_c_pvs_unit_supportentriesvaluation_selected_power. ((forall bpvi_i_pvs_unit_supportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_unit_supportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_unit_supportentriesvaluation_selected_power + S bpvi_i_pvs_unit_supportentriesvaluation_selected_power = pvs_exponent_unit_supportentries) -> (((exists bpvi_h_pvs_unit_supportentriesvaluation_selected_power_repeat. bpvi_h_pvs_unit_supportentriesvaluation_selected_power_repeat + S (pvs_prime_unit_supportentries) = S ((S (bpvi_i_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_c_pvs_unit_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_selected_power_repeat. bpvi_b_pvs_unit_supportentriesvaluation_selected_power = bpvi_q_pvs_unit_supportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_c_pvs_unit_supportentriesvaluation_selected_power) + (pvs_prime_unit_supportentries)))) /\ (exists bpvi_u_pvs_unit_supportentriesvaluation_selected_power bpvi_v_pvs_unit_supportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_unit_supportentriesvaluation_selected_power_start. bpvi_h_pvs_unit_supportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_selected_power_start. bpvi_u_pvs_unit_supportentriesvaluation_selected_power = bpvi_q_pvs_unit_supportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_unit_supportentriesvaluation_selected_power_terminal. bpvi_h_pvs_unit_supportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_unit_supportentriesvaluation_selected) = S ((S (pvs_exponent_unit_supportentries)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_selected_power_terminal. bpvi_u_pvs_unit_supportentriesvaluation_selected_power = bpvi_q_pvs_unit_supportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_unit_supportentries)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power) + (bpvi_result_pvs_unit_supportentriesvaluation_selected))) /\ forall bpvi_j_pvs_unit_supportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_unit_supportentriesvaluation_selected_power. bpvi_product_gap_pvs_unit_supportentriesvaluation_selected_power + S bpvi_j_pvs_unit_supportentriesvaluation_selected_power = pvs_exponent_unit_supportentries) -> exists bpvi_factor_pvs_unit_supportentriesvaluation_selected_power bpvi_partial_pvs_unit_supportentriesvaluation_selected_power bpvi_successor_pvs_unit_supportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_unit_supportentriesvaluation_selected_power_factor. bpvi_h_pvs_unit_supportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_unit_supportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_c_pvs_unit_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_selected_power_factor. bpvi_b_pvs_unit_supportentriesvaluation_selected_power = bpvi_q_pvs_unit_supportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_c_pvs_unit_supportentriesvaluation_selected_power) + (bpvi_factor_pvs_unit_supportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_unit_supportentriesvaluation_selected_power_partial. bpvi_h_pvs_unit_supportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_unit_supportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_selected_power_partial. bpvi_u_pvs_unit_supportentriesvaluation_selected_power = bpvi_q_pvs_unit_supportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power) + (bpvi_partial_pvs_unit_supportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_unit_supportentriesvaluation_selected_power_successor. bpvi_h_pvs_unit_supportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_unit_supportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_selected_power_successor. bpvi_u_pvs_unit_supportentriesvaluation_selected_power = bpvi_q_pvs_unit_supportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_unit_supportentriesvaluation_selected_power)) * bpvi_v_pvs_unit_supportentriesvaluation_selected_power) + (bpvi_successor_pvs_unit_supportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_unit_supportentriesvaluation_selected_power = bpvi_partial_pvs_unit_supportentriesvaluation_selected_power * bpvi_factor_pvs_unit_supportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_unit_supportentriesvaluation_selected. 1 = bpvi_result_pvs_unit_supportentriesvaluation_selected * bpvi_divisor_factor_pvs_unit_supportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_unit_supportentriesvaluation. (exists bpd_gap_pvs_unit_supportentriesvaluation_candidate_bound. bpd_gap_pvs_unit_supportentriesvaluation_candidate_bound + (bpd_candidate_pvs_unit_supportentriesvaluation) = (1)) -> (exists bpvi_result_pvs_unit_supportentriesvaluation_candidate. ((exists bpvi_b_pvs_unit_supportentriesvaluation_candidate_power bpvi_c_pvs_unit_supportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_unit_supportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_unit_supportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_unit_supportentriesvaluation_candidate_power + S bpvi_i_pvs_unit_supportentriesvaluation_candidate_power = bpd_candidate_pvs_unit_supportentriesvaluation) -> (((exists bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_repeat + S (pvs_prime_unit_supportentries) = S ((S (bpvi_i_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_unit_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_unit_supportentriesvaluation_candidate_power = bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_unit_supportentriesvaluation_candidate_power) + (pvs_prime_unit_supportentries)))) /\ (exists bpvi_u_pvs_unit_supportentriesvaluation_candidate_power bpvi_v_pvs_unit_supportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_start. bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_start. bpvi_u_pvs_unit_supportentriesvaluation_candidate_power = bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_unit_supportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_unit_supportentriesvaluation)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_unit_supportentriesvaluation_candidate_power = bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_unit_supportentriesvaluation)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power) + (bpvi_result_pvs_unit_supportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_unit_supportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_unit_supportentriesvaluation_candidate_power. bpvi_product_gap_pvs_unit_supportentriesvaluation_candidate_power + S bpvi_j_pvs_unit_supportentriesvaluation_candidate_power = bpd_candidate_pvs_unit_supportentriesvaluation) -> exists bpvi_factor_pvs_unit_supportentriesvaluation_candidate_power bpvi_partial_pvs_unit_supportentriesvaluation_candidate_power bpvi_successor_pvs_unit_supportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_factor. bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_unit_supportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_unit_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_factor. bpvi_b_pvs_unit_supportentriesvaluation_candidate_power = bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_unit_supportentriesvaluation_candidate_power) + (bpvi_factor_pvs_unit_supportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_partial. bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_unit_supportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_partial. bpvi_u_pvs_unit_supportentriesvaluation_candidate_power = bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power) + (bpvi_partial_pvs_unit_supportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_successor. bpvi_h_pvs_unit_supportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_unit_supportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_successor. bpvi_u_pvs_unit_supportentriesvaluation_candidate_power = bpvi_q_pvs_unit_supportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_unit_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_unit_supportentriesvaluation_candidate_power) + (bpvi_successor_pvs_unit_supportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_unit_supportentriesvaluation_candidate_power = bpvi_partial_pvs_unit_supportentriesvaluation_candidate_power * bpvi_factor_pvs_unit_supportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_unit_supportentriesvaluation_candidate. 1 = bpvi_result_pvs_unit_supportentriesvaluation_candidate * bpvi_divisor_factor_pvs_unit_supportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_unit_supportentriesvaluation_maximal. bpd_gap_pvs_unit_supportentriesvaluation_maximal + (bpd_candidate_pvs_unit_supportentriesvaluation) = (pvs_exponent_unit_supportentries))) /\ (exists pa_b_pvs_unit_supportentriesvalue pa_c_pvs_unit_supportentriesvalue. ((forall pa_i_pvs_unit_supportentriesvalue_repeat. (exists pa_lt_pvs_unit_supportentriesvalue_repeat_bound. pa_lt_pvs_unit_supportentriesvalue_repeat_bound + S pa_i_pvs_unit_supportentriesvalue_repeat = pvs_exponent_unit_supportentries) -> (((exists pa_h_pvs_unit_supportentriesvalue_repeat_decoded. pa_h_pvs_unit_supportentriesvalue_repeat_decoded + S (pvs_prime_unit_supportentries) = S ((S (pa_i_pvs_unit_supportentriesvalue_repeat)) * pa_c_pvs_unit_supportentriesvalue)) /\ exists pa_q_pvs_unit_supportentriesvalue_repeat_decoded. pa_b_pvs_unit_supportentriesvalue = pa_q_pvs_unit_supportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_unit_supportentriesvalue_repeat)) * pa_c_pvs_unit_supportentriesvalue) + (pvs_prime_unit_supportentries)))) /\ (exists pa_u_pvs_unit_supportentriesvalue_product pa_v_pvs_unit_supportentriesvalue_product. ((((exists pa_h_pvs_unit_supportentriesvalue_product_start. pa_h_pvs_unit_supportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_unit_supportentriesvalue_product)) /\ exists pa_q_pvs_unit_supportentriesvalue_product_start. pa_u_pvs_unit_supportentriesvalue_product = pa_q_pvs_unit_supportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_unit_supportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_unit_supportentriesvalue_product_terminal. pa_h_pvs_unit_supportentriesvalue_product_terminal + S (pvs_power_unit_supportentries) = S ((S (pvs_exponent_unit_supportentries)) * pa_v_pvs_unit_supportentriesvalue_product)) /\ exists pa_q_pvs_unit_supportentriesvalue_product_terminal. pa_u_pvs_unit_supportentriesvalue_product = pa_q_pvs_unit_supportentriesvalue_product_terminal * S ((S (pvs_exponent_unit_supportentries)) * pa_v_pvs_unit_supportentriesvalue_product) + (pvs_power_unit_supportentries))) /\ forall pa_i_pvs_unit_supportentriesvalue_product. (exists pa_lt_pvs_unit_supportentriesvalue_product_bound. pa_lt_pvs_unit_supportentriesvalue_product_bound + S pa_i_pvs_unit_supportentriesvalue_product = pvs_exponent_unit_supportentries) -> exists pa_p_pvs_unit_supportentriesvalue_product pa_r_pvs_unit_supportentriesvalue_product pa_s_pvs_unit_supportentriesvalue_product. ((((exists pa_h_pvs_unit_supportentriesvalue_product_factor. pa_h_pvs_unit_supportentriesvalue_product_factor + S (pa_p_pvs_unit_supportentriesvalue_product) = S ((S (pa_i_pvs_unit_supportentriesvalue_product)) * pa_c_pvs_unit_supportentriesvalue)) /\ exists pa_q_pvs_unit_supportentriesvalue_product_factor. pa_b_pvs_unit_supportentriesvalue = pa_q_pvs_unit_supportentriesvalue_product_factor * S ((S (pa_i_pvs_unit_supportentriesvalue_product)) * pa_c_pvs_unit_supportentriesvalue) + (pa_p_pvs_unit_supportentriesvalue_product))) /\ ((((exists pa_h_pvs_unit_supportentriesvalue_product_partial. pa_h_pvs_unit_supportentriesvalue_product_partial + S (pa_r_pvs_unit_supportentriesvalue_product) = S ((S (pa_i_pvs_unit_supportentriesvalue_product)) * pa_v_pvs_unit_supportentriesvalue_product)) /\ exists pa_q_pvs_unit_supportentriesvalue_product_partial. pa_u_pvs_unit_supportentriesvalue_product = pa_q_pvs_unit_supportentriesvalue_product_partial * S ((S (pa_i_pvs_unit_supportentriesvalue_product)) * pa_v_pvs_unit_supportentriesvalue_product) + (pa_r_pvs_unit_supportentriesvalue_product))) /\ ((((exists pa_h_pvs_unit_supportentriesvalue_product_successor. pa_h_pvs_unit_supportentriesvalue_product_successor + S (pa_s_pvs_unit_supportentriesvalue_product) = S ((S (S pa_i_pvs_unit_supportentriesvalue_product)) * pa_v_pvs_unit_supportentriesvalue_product)) /\ exists pa_q_pvs_unit_supportentriesvalue_product_successor. pa_u_pvs_unit_supportentriesvalue_product = pa_q_pvs_unit_supportentriesvalue_product_successor * S ((S (S pa_i_pvs_unit_supportentriesvalue_product)) * pa_v_pvs_unit_supportentriesvalue_product) + (pa_s_pvs_unit_supportentriesvalue_product))) /\ pa_s_pvs_unit_supportentriesvalue_product = pa_r_pvs_unit_supportentriesvalue_product * pa_p_pvs_unit_supportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_unit_supportcover. (~((pvs_divisor_unit_supportcover) = 1) /\ forall pvs_left_unit_supportcoverprime pvs_right_unit_supportcoverprime. (pvs_divisor_unit_supportcover) = pvs_left_unit_supportcoverprime * pvs_right_unit_supportcoverprime -> pvs_left_unit_supportcoverprime = 1 \/ pvs_right_unit_supportcoverprime = 1) -> (exists pvs_factor_unit_supportcoverdivides. (1) = (pvs_divisor_unit_supportcover) * pvs_factor_unit_supportcoverdivides) -> exists pvs_position_unit_supportcover. (exists pvs_gap_unit_supportcoverbound. pvs_gap_unit_supportcoverbound + S (pvs_position_unit_supportcover) = (0)) /\ (((exists ff_h_pvs_unit_supportcoverentry. ff_h_pvs_unit_supportcoverentry + S (pvs_divisor_unit_supportcover) = S ((S (pvs_position_unit_supportcover)) * 0)) /\ exists ff_q_pvs_unit_supportcoverentry. 0 = ff_q_pvs_unit_supportcoverentry * S ((S (pvs_position_unit_supportcover)) * 0) + (pvs_divisor_unit_supportcover)))) /\ (exists ff_u_pvs_unit_supportproduct ff_v_pvs_unit_supportproduct. ((((exists ff_h_pvs_unit_supportproduct_start. ff_h_pvs_unit_supportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_unit_supportproduct)) /\ exists ff_q_pvs_unit_supportproduct_start. ff_u_pvs_unit_supportproduct = ff_q_pvs_unit_supportproduct_start * S ((S (0)) * ff_v_pvs_unit_supportproduct) + (1))) /\ ((((exists ff_h_pvs_unit_supportproduct_terminal. ff_h_pvs_unit_supportproduct_terminal + S (1) = S ((S (0)) * ff_v_pvs_unit_supportproduct)) /\ exists ff_q_pvs_unit_supportproduct_terminal. ff_u_pvs_unit_supportproduct = ff_q_pvs_unit_supportproduct_terminal * S ((S (0)) * ff_v_pvs_unit_supportproduct) + (1))) /\ forall ff_i_pvs_unit_supportproduct. (exists ff_lt_pvs_unit_supportproduct_bound. ff_lt_pvs_unit_supportproduct_bound + S ff_i_pvs_unit_supportproduct = 0) -> exists ff_p_pvs_unit_supportproduct ff_r_pvs_unit_supportproduct ff_s_pvs_unit_supportproduct. ((((exists ff_h_pvs_unit_supportproduct_factor. ff_h_pvs_unit_supportproduct_factor + S (ff_p_pvs_unit_supportproduct) = S ((S (ff_i_pvs_unit_supportproduct)) * 0)) /\ exists ff_q_pvs_unit_supportproduct_factor. 0 = ff_q_pvs_unit_supportproduct_factor * S ((S (ff_i_pvs_unit_supportproduct)) * 0) + (ff_p_pvs_unit_supportproduct))) /\ ((((exists ff_h_pvs_unit_supportproduct_partial. ff_h_pvs_unit_supportproduct_partial + S (ff_r_pvs_unit_supportproduct) = S ((S (ff_i_pvs_unit_supportproduct)) * ff_v_pvs_unit_supportproduct)) /\ exists ff_q_pvs_unit_supportproduct_partial. ff_u_pvs_unit_supportproduct = ff_q_pvs_unit_supportproduct_partial * S ((S (ff_i_pvs_unit_supportproduct)) * ff_v_pvs_unit_supportproduct) + (ff_r_pvs_unit_supportproduct))) /\ ((((exists ff_h_pvs_unit_supportproduct_successor. ff_h_pvs_unit_supportproduct_successor + S (ff_s_pvs_unit_supportproduct) = S ((S (S ff_i_pvs_unit_supportproduct)) * ff_v_pvs_unit_supportproduct)) /\ exists ff_q_pvs_unit_supportproduct_successor. ff_u_pvs_unit_supportproduct = ff_q_pvs_unit_supportproduct_successor * S ((S (S ff_i_pvs_unit_supportproduct)) * ff_v_pvs_unit_supportproduct) + (ff_s_pvs_unit_supportproduct))) /\ ff_s_pvs_unit_supportproduct = ff_r_pvs_unit_supportproduct * ff_p_pvs_unit_supportproduct)))))))))))))

Complete tactic proof in conservative notation

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

48 script commands · 18 reading checkpoints · 2 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.

01Separate the logical casesL1–1

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

  1. L1
    split
02Fix variables and assumptionsL2–2

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

  1. L2
    intro hz
03Use earlier factsL3–4

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

  1. L3
    apply PA1
  2. L4
    exact hz
04Separate the logical casesL5–5

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

  1. L5
    split
05Fix variables and assumptionsL6–12

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

  1. L6
    intro i
  2. L7
    intro j
  3. L8
    intro p
  4. L9
    intro hi
  5. L10
    intro hj
  6. L11
    intro hleft
  7. L12
    intro hright
06Separate the logical casesL13–13

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

  1. L13
    exfalso
07Use earlier factsL14–16

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

  1. L14
    specialize factor_permutation_below_zero_impossible (i)
  2. L15
    apply factor_permutation_below_zero_impossible
  3. L16
    exact hi
08Separate the logical casesL17–17

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

  1. L17
    split
09Fix variables and assumptionsL18–19

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

  1. L18
    intro i
  2. L19
    intro hi
10Separate the logical casesL20–20

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

  1. L20
    exfalso
11Use earlier factsL21–23

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

  1. L21
    specialize factor_permutation_below_zero_impossible (i)
  2. L22
    apply factor_permutation_below_zero_impossible
  3. L23
    exact hi
12Separate the logical casesL24–24

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

  1. L24
    split
13Fix variables and assumptionsL25–27

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

  1. L25
    intro p
  2. L26
    intro hp
  3. L27
    intro hdiv
14Separate the logical casesL28–29

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

  1. L28
    exfalso
  2. L29
    cases hp
15Use earlier factsL30–33

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

  1. L30
    apply hp_left
  2. L31
    specialize divisor_one (p)
  3. L32
    apply divisor_one
  4. L33
    exact hdiv
16Establish hprodL34–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation product exists.

  1. L34
    have hprod : ∃ v. Product(0,0,0,v)Definitions: Product(0,0,0,v)Original native command in the exact edition
  2. L35
    specialize factor_permutation_product_exists (0)
  3. L36
    specialize factor_permutation_product_exists (0)
  4. L37
    specialize factor_permutation_product_exists (0)
  5. L38
    apply factor_permutation_product_exists
17Separate the logical casesL39–39

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

  1. L39
    cases hprod
18Establish heqL40–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product zero.

  1. L40
    have heq : x = 1
  2. L41
    specialize beta_product_zero (0)
  3. L42
    specialize beta_product_zero (0)
  4. L43
    specialize beta_product_zero (x)
  5. L44
    apply beta_product_zero
  6. L45
    exact hprod_witness
  7. L46
    rewrite heq at hprod_witness
  8. L47
    rewrite heq at hprod_witness
  9. L48
    exact hprod_witness

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001split
  2. 0002intro hz
  3. 0003apply PA1
  4. 0004exact hz
  5. 0005split
  6. 0006intro i
  7. 0007intro j
  8. 0008intro p
  9. 0009intro hi
  10. 0010intro hj
  11. 0011intro hleft
  12. 0012intro hright
  13. 0013exfalso
  14. 0014specialize factor_permutation_below_zero_impossible (i)
  15. 0015apply factor_permutation_below_zero_impossible
  16. 0016exact hi
  17. 0017split
  18. 0018intro i
  19. 0019intro hi
  20. 0020exfalso
  21. 0021specialize factor_permutation_below_zero_impossible (i)
  22. 0022apply factor_permutation_below_zero_impossible
  23. 0023exact hi
  24. 0024split
  25. 0025intro p
  26. 0026intro hp
  27. 0027intro hdiv
  28. 0028exfalso
  29. 0029cases hp
  30. 0030apply hp_left
  31. 0031specialize divisor_one (p)
  32. 0032apply divisor_one
  33. 0033exact hdiv
  34. 0034have hprod : ∃ v. Product(0,0,0,v)
  35. 0035specialize factor_permutation_product_exists (0)
  36. 0036specialize factor_permutation_product_exists (0)
  37. 0037specialize factor_permutation_product_exists (0)
  38. 0038apply factor_permutation_product_exists
  39. 0039cases hprod
  40. 0040have heq : x = 1
  41. 0041specialize beta_product_zero (0)
  42. 0042specialize beta_product_zero (0)
  43. 0043specialize beta_product_zero (x)
  44. 0044apply beta_product_zero
  45. 0045exact hprod_witness
  46. 0046rewrite heq at hprod_witness
  47. 0047rewrite heq at hprod_witness
  48. 0048exact hprod_witness