TS0039

all_bad_prime_even_valuations_strip_square_factor

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

Removing a nonzero natural-square block preserves every three-modulo-four prime's constructive even-valuation invariant.

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.

Exact expanded first-order arithmetic statement

forall z n. ~(z = 0) -> ~(n = 0) -> (forall ftsp_bad_prime_parity_square_product ftsp_bad_exponent_parity_square_product. ((~(ftsp_bad_prime_parity_square_product = 1) /\ forall frm_prime_left_ftsp_parity_square_product_prime frm_prime_right_ftsp_parity_square_product_prime. ftsp_bad_prime_parity_square_product = frm_prime_left_ftsp_parity_square_product_prime * frm_prime_right_ftsp_parity_square_product_prime -> frm_prime_left_ftsp_parity_square_product_prime = 1 \/ frm_prime_right_ftsp_parity_square_product_prime = 1)) -> (exists ftsc_four_three_ftsp_parity_square_product_three. (ftsp_bad_prime_parity_square_product) = 4 * ftsc_four_three_ftsp_parity_square_product_three + 3) -> (((exists bpv_gap_ftsp_parity_square_product_valuation_exponent_bound. bpv_gap_ftsp_parity_square_product_valuation_exponent_bound + ftsp_bad_exponent_parity_square_product = (n * (z * z))) /\ (exists bpv_result_ftsp_parity_square_product_valuation_selected. ((exists ff_b_ftsp_parity_square_product_valuation_selected_power ff_c_ftsp_parity_square_product_valuation_selected_power. ((forall ff_i_ftsp_parity_square_product_valuation_selected_power_repeat. (exists ff_lt_ftsp_parity_square_product_valuation_selected_power_repeat_bound. ff_lt_ftsp_parity_square_product_valuation_selected_power_repeat_bound + S ff_i_ftsp_parity_square_product_valuation_selected_power_repeat = ftsp_bad_exponent_parity_square_product) -> (((exists ff_h_ftsp_parity_square_product_valuation_selected_power_repeat_decoded. ff_h_ftsp_parity_square_product_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_parity_square_product) = S ((S (ff_i_ftsp_parity_square_product_valuation_selected_power_repeat)) * ff_c_ftsp_parity_square_product_valuation_selected_power)) /\ exists ff_q_ftsp_parity_square_product_valuation_selected_power_repeat_decoded. ff_b_ftsp_parity_square_product_valuation_selected_power = ff_q_ftsp_parity_square_product_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_parity_square_product_valuation_selected_power_repeat)) * ff_c_ftsp_parity_square_product_valuation_selected_power) + (ftsp_bad_prime_parity_square_product)))) /\ (exists ff_u_ftsp_parity_square_product_valuation_selected_power_product ff_v_ftsp_parity_square_product_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_square_product_valuation_selected_power_product_start. ff_h_ftsp_parity_square_product_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_selected_power_product_start. ff_u_ftsp_parity_square_product_valuation_selected_power_product = ff_q_ftsp_parity_square_product_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_square_product_valuation_selected_power_product_terminal. ff_h_ftsp_parity_square_product_valuation_selected_power_product_terminal + S (bpv_result_ftsp_parity_square_product_valuation_selected) = S ((S (ftsp_bad_exponent_parity_square_product)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_selected_power_product_terminal. ff_u_ftsp_parity_square_product_valuation_selected_power_product = ff_q_ftsp_parity_square_product_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_parity_square_product)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product) + (bpv_result_ftsp_parity_square_product_valuation_selected))) /\ forall ff_i_ftsp_parity_square_product_valuation_selected_power_product. (exists ff_lt_ftsp_parity_square_product_valuation_selected_power_product_bound. ff_lt_ftsp_parity_square_product_valuation_selected_power_product_bound + S ff_i_ftsp_parity_square_product_valuation_selected_power_product = ftsp_bad_exponent_parity_square_product) -> exists ff_p_ftsp_parity_square_product_valuation_selected_power_product ff_r_ftsp_parity_square_product_valuation_selected_power_product ff_s_ftsp_parity_square_product_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_square_product_valuation_selected_power_product_factor. ff_h_ftsp_parity_square_product_valuation_selected_power_product_factor + S (ff_p_ftsp_parity_square_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_square_product_valuation_selected_power_product)) * ff_c_ftsp_parity_square_product_valuation_selected_power)) /\ exists ff_q_ftsp_parity_square_product_valuation_selected_power_product_factor. ff_b_ftsp_parity_square_product_valuation_selected_power = ff_q_ftsp_parity_square_product_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_parity_square_product_valuation_selected_power_product)) * ff_c_ftsp_parity_square_product_valuation_selected_power) + (ff_p_ftsp_parity_square_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_square_product_valuation_selected_power_product_partial. ff_h_ftsp_parity_square_product_valuation_selected_power_product_partial + S (ff_r_ftsp_parity_square_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_square_product_valuation_selected_power_product)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_selected_power_product_partial. ff_u_ftsp_parity_square_product_valuation_selected_power_product = ff_q_ftsp_parity_square_product_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_parity_square_product_valuation_selected_power_product)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product) + (ff_r_ftsp_parity_square_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_square_product_valuation_selected_power_product_successor. ff_h_ftsp_parity_square_product_valuation_selected_power_product_successor + S (ff_s_ftsp_parity_square_product_valuation_selected_power_product) = S ((S (S ff_i_ftsp_parity_square_product_valuation_selected_power_product)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_selected_power_product_successor. ff_u_ftsp_parity_square_product_valuation_selected_power_product = ff_q_ftsp_parity_square_product_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_parity_square_product_valuation_selected_power_product)) * ff_v_ftsp_parity_square_product_valuation_selected_power_product) + (ff_s_ftsp_parity_square_product_valuation_selected_power_product))) /\ ff_s_ftsp_parity_square_product_valuation_selected_power_product = ff_r_ftsp_parity_square_product_valuation_selected_power_product * ff_p_ftsp_parity_square_product_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_square_product_valuation_selected_divides. (n * (z * z)) = bpv_result_ftsp_parity_square_product_valuation_selected * bpv_factor_ftsp_parity_square_product_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_parity_square_product_valuation. (exists bpv_gap_ftsp_parity_square_product_valuation_candidate_bound. bpv_gap_ftsp_parity_square_product_valuation_candidate_bound + bpv_candidate_ftsp_parity_square_product_valuation = (n * (z * z))) -> (exists bpv_result_ftsp_parity_square_product_valuation_candidate. ((exists ff_b_ftsp_parity_square_product_valuation_candidate_power ff_c_ftsp_parity_square_product_valuation_candidate_power. ((forall ff_i_ftsp_parity_square_product_valuation_candidate_power_repeat. (exists ff_lt_ftsp_parity_square_product_valuation_candidate_power_repeat_bound. ff_lt_ftsp_parity_square_product_valuation_candidate_power_repeat_bound + S ff_i_ftsp_parity_square_product_valuation_candidate_power_repeat = bpv_candidate_ftsp_parity_square_product_valuation) -> (((exists ff_h_ftsp_parity_square_product_valuation_candidate_power_repeat_decoded. ff_h_ftsp_parity_square_product_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_parity_square_product) = S ((S (ff_i_ftsp_parity_square_product_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_square_product_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_square_product_valuation_candidate_power_repeat_decoded. ff_b_ftsp_parity_square_product_valuation_candidate_power = ff_q_ftsp_parity_square_product_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_parity_square_product_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_square_product_valuation_candidate_power) + (ftsp_bad_prime_parity_square_product)))) /\ (exists ff_u_ftsp_parity_square_product_valuation_candidate_power_product ff_v_ftsp_parity_square_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_square_product_valuation_candidate_power_product_start. ff_h_ftsp_parity_square_product_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_candidate_power_product_start. ff_u_ftsp_parity_square_product_valuation_candidate_power_product = ff_q_ftsp_parity_square_product_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_square_product_valuation_candidate_power_product_terminal. ff_h_ftsp_parity_square_product_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_parity_square_product_valuation_candidate) = S ((S (bpv_candidate_ftsp_parity_square_product_valuation)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_candidate_power_product_terminal. ff_u_ftsp_parity_square_product_valuation_candidate_power_product = ff_q_ftsp_parity_square_product_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_parity_square_product_valuation)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product) + (bpv_result_ftsp_parity_square_product_valuation_candidate))) /\ forall ff_i_ftsp_parity_square_product_valuation_candidate_power_product. (exists ff_lt_ftsp_parity_square_product_valuation_candidate_power_product_bound. ff_lt_ftsp_parity_square_product_valuation_candidate_power_product_bound + S ff_i_ftsp_parity_square_product_valuation_candidate_power_product = bpv_candidate_ftsp_parity_square_product_valuation) -> exists ff_p_ftsp_parity_square_product_valuation_candidate_power_product ff_r_ftsp_parity_square_product_valuation_candidate_power_product ff_s_ftsp_parity_square_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_square_product_valuation_candidate_power_product_factor. ff_h_ftsp_parity_square_product_valuation_candidate_power_product_factor + S (ff_p_ftsp_parity_square_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_square_product_valuation_candidate_power_product)) * ff_c_ftsp_parity_square_product_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_square_product_valuation_candidate_power_product_factor. ff_b_ftsp_parity_square_product_valuation_candidate_power = ff_q_ftsp_parity_square_product_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_parity_square_product_valuation_candidate_power_product)) * ff_c_ftsp_parity_square_product_valuation_candidate_power) + (ff_p_ftsp_parity_square_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_square_product_valuation_candidate_power_product_partial. ff_h_ftsp_parity_square_product_valuation_candidate_power_product_partial + S (ff_r_ftsp_parity_square_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_square_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_candidate_power_product_partial. ff_u_ftsp_parity_square_product_valuation_candidate_power_product = ff_q_ftsp_parity_square_product_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_parity_square_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product) + (ff_r_ftsp_parity_square_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_square_product_valuation_candidate_power_product_successor. ff_h_ftsp_parity_square_product_valuation_candidate_power_product_successor + S (ff_s_ftsp_parity_square_product_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_parity_square_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_square_product_valuation_candidate_power_product_successor. ff_u_ftsp_parity_square_product_valuation_candidate_power_product = ff_q_ftsp_parity_square_product_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_parity_square_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_square_product_valuation_candidate_power_product) + (ff_s_ftsp_parity_square_product_valuation_candidate_power_product))) /\ ff_s_ftsp_parity_square_product_valuation_candidate_power_product = ff_r_ftsp_parity_square_product_valuation_candidate_power_product * ff_p_ftsp_parity_square_product_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_square_product_valuation_candidate_divides. (n * (z * z)) = bpv_result_ftsp_parity_square_product_valuation_candidate * bpv_factor_ftsp_parity_square_product_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_parity_square_product_valuation_maximal. bpv_gap_ftsp_parity_square_product_valuation_maximal + bpv_candidate_ftsp_parity_square_product_valuation = ftsp_bad_exponent_parity_square_product)) -> exists ftsp_bad_half_parity_square_product. ftsp_bad_exponent_parity_square_product = ftsp_bad_half_parity_square_product + ftsp_bad_half_parity_square_product) -> (forall ftsp_bad_prime_parity_source ftsp_bad_exponent_parity_source. ((~(ftsp_bad_prime_parity_source = 1) /\ forall frm_prime_left_ftsp_parity_source_prime frm_prime_right_ftsp_parity_source_prime. ftsp_bad_prime_parity_source = frm_prime_left_ftsp_parity_source_prime * frm_prime_right_ftsp_parity_source_prime -> frm_prime_left_ftsp_parity_source_prime = 1 \/ frm_prime_right_ftsp_parity_source_prime = 1)) -> (exists ftsc_four_three_ftsp_parity_source_three. (ftsp_bad_prime_parity_source) = 4 * ftsc_four_three_ftsp_parity_source_three + 3) -> (((exists bpv_gap_ftsp_parity_source_valuation_exponent_bound. bpv_gap_ftsp_parity_source_valuation_exponent_bound + ftsp_bad_exponent_parity_source = (n)) /\ (exists bpv_result_ftsp_parity_source_valuation_selected. ((exists ff_b_ftsp_parity_source_valuation_selected_power ff_c_ftsp_parity_source_valuation_selected_power. ((forall ff_i_ftsp_parity_source_valuation_selected_power_repeat. (exists ff_lt_ftsp_parity_source_valuation_selected_power_repeat_bound. ff_lt_ftsp_parity_source_valuation_selected_power_repeat_bound + S ff_i_ftsp_parity_source_valuation_selected_power_repeat = ftsp_bad_exponent_parity_source) -> (((exists ff_h_ftsp_parity_source_valuation_selected_power_repeat_decoded. ff_h_ftsp_parity_source_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_parity_source) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_repeat)) * ff_c_ftsp_parity_source_valuation_selected_power)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_repeat_decoded. ff_b_ftsp_parity_source_valuation_selected_power = ff_q_ftsp_parity_source_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_repeat)) * ff_c_ftsp_parity_source_valuation_selected_power) + (ftsp_bad_prime_parity_source)))) /\ (exists ff_u_ftsp_parity_source_valuation_selected_power_product ff_v_ftsp_parity_source_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_start. ff_h_ftsp_parity_source_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_start. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_terminal. ff_h_ftsp_parity_source_valuation_selected_power_product_terminal + S (bpv_result_ftsp_parity_source_valuation_selected) = S ((S (ftsp_bad_exponent_parity_source)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_terminal. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_parity_source)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (bpv_result_ftsp_parity_source_valuation_selected))) /\ forall ff_i_ftsp_parity_source_valuation_selected_power_product. (exists ff_lt_ftsp_parity_source_valuation_selected_power_product_bound. ff_lt_ftsp_parity_source_valuation_selected_power_product_bound + S ff_i_ftsp_parity_source_valuation_selected_power_product = ftsp_bad_exponent_parity_source) -> exists ff_p_ftsp_parity_source_valuation_selected_power_product ff_r_ftsp_parity_source_valuation_selected_power_product ff_s_ftsp_parity_source_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_factor. ff_h_ftsp_parity_source_valuation_selected_power_product_factor + S (ff_p_ftsp_parity_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_c_ftsp_parity_source_valuation_selected_power)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_factor. ff_b_ftsp_parity_source_valuation_selected_power = ff_q_ftsp_parity_source_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_c_ftsp_parity_source_valuation_selected_power) + (ff_p_ftsp_parity_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_partial. ff_h_ftsp_parity_source_valuation_selected_power_product_partial + S (ff_r_ftsp_parity_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_partial. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (ff_r_ftsp_parity_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_successor. ff_h_ftsp_parity_source_valuation_selected_power_product_successor + S (ff_s_ftsp_parity_source_valuation_selected_power_product) = S ((S (S ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_successor. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (ff_s_ftsp_parity_source_valuation_selected_power_product))) /\ ff_s_ftsp_parity_source_valuation_selected_power_product = ff_r_ftsp_parity_source_valuation_selected_power_product * ff_p_ftsp_parity_source_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_source_valuation_selected_divides. (n) = bpv_result_ftsp_parity_source_valuation_selected * bpv_factor_ftsp_parity_source_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_parity_source_valuation. (exists bpv_gap_ftsp_parity_source_valuation_candidate_bound. bpv_gap_ftsp_parity_source_valuation_candidate_bound + bpv_candidate_ftsp_parity_source_valuation = (n)) -> (exists bpv_result_ftsp_parity_source_valuation_candidate. ((exists ff_b_ftsp_parity_source_valuation_candidate_power ff_c_ftsp_parity_source_valuation_candidate_power. ((forall ff_i_ftsp_parity_source_valuation_candidate_power_repeat. (exists ff_lt_ftsp_parity_source_valuation_candidate_power_repeat_bound. ff_lt_ftsp_parity_source_valuation_candidate_power_repeat_bound + S ff_i_ftsp_parity_source_valuation_candidate_power_repeat = bpv_candidate_ftsp_parity_source_valuation) -> (((exists ff_h_ftsp_parity_source_valuation_candidate_power_repeat_decoded. ff_h_ftsp_parity_source_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_parity_source) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_source_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_repeat_decoded. ff_b_ftsp_parity_source_valuation_candidate_power = ff_q_ftsp_parity_source_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_source_valuation_candidate_power) + (ftsp_bad_prime_parity_source)))) /\ (exists ff_u_ftsp_parity_source_valuation_candidate_power_product ff_v_ftsp_parity_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_start. ff_h_ftsp_parity_source_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_start. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_terminal. ff_h_ftsp_parity_source_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_parity_source_valuation_candidate) = S ((S (bpv_candidate_ftsp_parity_source_valuation)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_terminal. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_parity_source_valuation)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (bpv_result_ftsp_parity_source_valuation_candidate))) /\ forall ff_i_ftsp_parity_source_valuation_candidate_power_product. (exists ff_lt_ftsp_parity_source_valuation_candidate_power_product_bound. ff_lt_ftsp_parity_source_valuation_candidate_power_product_bound + S ff_i_ftsp_parity_source_valuation_candidate_power_product = bpv_candidate_ftsp_parity_source_valuation) -> exists ff_p_ftsp_parity_source_valuation_candidate_power_product ff_r_ftsp_parity_source_valuation_candidate_power_product ff_s_ftsp_parity_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_factor. ff_h_ftsp_parity_source_valuation_candidate_power_product_factor + S (ff_p_ftsp_parity_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_c_ftsp_parity_source_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_factor. ff_b_ftsp_parity_source_valuation_candidate_power = ff_q_ftsp_parity_source_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_c_ftsp_parity_source_valuation_candidate_power) + (ff_p_ftsp_parity_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_partial. ff_h_ftsp_parity_source_valuation_candidate_power_product_partial + S (ff_r_ftsp_parity_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_partial. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (ff_r_ftsp_parity_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_successor. ff_h_ftsp_parity_source_valuation_candidate_power_product_successor + S (ff_s_ftsp_parity_source_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_successor. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (ff_s_ftsp_parity_source_valuation_candidate_power_product))) /\ ff_s_ftsp_parity_source_valuation_candidate_power_product = ff_r_ftsp_parity_source_valuation_candidate_power_product * ff_p_ftsp_parity_source_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_source_valuation_candidate_divides. (n) = bpv_result_ftsp_parity_source_valuation_candidate * bpv_factor_ftsp_parity_source_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_parity_source_valuation_maximal. bpv_gap_ftsp_parity_source_valuation_maximal + bpv_candidate_ftsp_parity_source_valuation = ftsp_bad_exponent_parity_source)) -> exists ftsp_bad_half_parity_source. ftsp_bad_exponent_parity_source = ftsp_bad_half_parity_source + ftsp_bad_half_parity_source)

Constructive proof overview

Generated structural guide

Removing a nonzero natural-square block preserves every three-modulo-four prime's constructive even-valuation invariant.

The unchanged tactic script uses 4 declared prerequisites and contains 45 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

power_valuation_exists Alpha theorem; checked-use authorized power_valuation_value_eq_transport Alpha theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized TS0036 square_factor_even_valuation_reflects_cofactor

Direct dependents

TS003C all_bad_prime_even_two_square_sufficiency_bounded

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

45 script commands · 9 reading checkpoints · 4 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 (1)
square factor even valuation reflects cofactor

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro z
  2. L2
    intro n
  3. L3
    intro hznonzero
  4. L4
    intro hnnonzero
  5. L5
    intro htotal
  6. L6
    intro p
  7. L7
    intro f
  8. L8
    intro hpprime
  9. L9
    intro hpbad
  10. L10
    intro hnvaluation
02Establish hzvaluationL11–12

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

  1. L11
    have hzvaluation : ∃ e. BoundedPowerValuation(p,z,z,e)Definitions: BoundedPowerValuation
  2. L12
    apply power_valuation_exists
03Separate the logical casesL13–13

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

  1. L13
    cases hzvaluation
04Establish hproductL14–15

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

  1. L14
    have hproduct : ∃ g. BoundedPowerValuation(p,z · z · n,z · z · n,g)Definitions: BoundedPowerValuation
  2. L15
    apply power_valuation_exists
05Separate the logical casesL16–16

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

  1. L16
    cases hproduct
06Establish hrightvaluationL17–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation value eq transport.

  1. L17
    have hrightvaluation : BoundedPowerValuation(p,n · (z · z),n · (z · z),x1)Definitions: BoundedPowerValuation
  2. L18
    specialize power_valuation_value_eq_transport p
  3. L19
    specialize power_valuation_value_eq_transport ((z * z) * n)
  4. L20
    specialize power_valuation_value_eq_transport (n * (z * z))
  5. L21
    specialize power_valuation_value_eq_transport x1
  6. L22
    apply power_valuation_value_eq_transport
  7. L23
    apply mul_comm
  8. L24
    exact hproduct_witness
07Establish hevenL25–34

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

  1. L25
    have heven : exists h. x1 = h + h
  2. L26
    specialize htotal p
  3. L27
    specialize htotal x1
  4. L28
    apply htotal
  5. L29
    exact hpprime
  6. L30
    exact hpbad
  7. L31
    exact hrightvaluation
  8. L32
    specialize square_factor_even_valuation_reflects_cofactor p
  9. L33
    specialize square_factor_even_valuation_reflects_cofactor z
  10. L34
    specialize square_factor_even_valuation_reflects_cofactor n
08Use earlier factsL35–44

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

  1. L35
    specialize square_factor_even_valuation_reflects_cofactor x
  2. L36
    specialize square_factor_even_valuation_reflects_cofactor f
  3. L37
    specialize square_factor_even_valuation_reflects_cofactor x1
  4. L38
    apply square_factor_even_valuation_reflects_cofactor
  5. L39
    exact hpprime
  6. L40
    exact hznonzero
  7. L41
    exact hnnonzero
  8. L42
    exact hzvaluation_witness
  9. L43
    exact hnvaluation
  10. L44
    exact hproduct_witness
09Use earlier factsL45–45

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

  1. L45
    exact heven

Library-wide reading audit

Original exact command ledger · 45 lines
  1. 0001intro z
  2. 0002intro n
  3. 0003intro hznonzero
  4. 0004intro hnnonzero
  5. 0005intro htotal
  6. 0006intro p
  7. 0007intro f
  8. 0008intro hpprime
  9. 0009intro hpbad
  10. 0010intro hnvaluation
  11. 0011have hzvaluation : exists e. (((exists bpv_gap_ftsp_square_factor_exponent_bound. bpv_gap_ftsp_square_factor_exponent_bound + e = z) /\ (exists bpv_result_ftsp_square_factor_selected. ((exists ff_b_ftsp_square_factor_selected_power ff_c_ftsp_square_factor_selected_power. ((forall ff_i_ftsp_square_factor_selected_power_repeat. (exists ff_lt_ftsp_square_factor_selected_power_repeat_bound. ff_lt_ftsp_square_factor_selected_power_repeat_bound + S ff_i_ftsp_square_factor_selected_power_repeat = e) -> (((exists ff_h_ftsp_square_factor_selected_power_repeat_decoded. ff_h_ftsp_square_factor_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_square_factor_selected_power_repeat)) * ff_c_ftsp_square_factor_selected_power)) /\ exists ff_q_ftsp_square_factor_selected_power_repeat_decoded. ff_b_ftsp_square_factor_selected_power = ff_q_ftsp_square_factor_selected_power_repeat_decoded * S ((S (ff_i_ftsp_square_factor_selected_power_repeat)) * ff_c_ftsp_square_factor_selected_power) + (p)))) /\ (exists ff_u_ftsp_square_factor_selected_power_product ff_v_ftsp_square_factor_selected_power_product. ((((exists ff_h_ftsp_square_factor_selected_power_product_start. ff_h_ftsp_square_factor_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_square_factor_selected_power_product)) /\ exists ff_q_ftsp_square_factor_selected_power_product_start. ff_u_ftsp_square_factor_selected_power_product = ff_q_ftsp_square_factor_selected_power_product_start * S ((S (0)) * ff_v_ftsp_square_factor_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_square_factor_selected_power_product_terminal. ff_h_ftsp_square_factor_selected_power_product_terminal + S (bpv_result_ftsp_square_factor_selected) = S ((S (e)) * ff_v_ftsp_square_factor_selected_power_product)) /\ exists ff_q_ftsp_square_factor_selected_power_product_terminal. ff_u_ftsp_square_factor_selected_power_product = ff_q_ftsp_square_factor_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_square_factor_selected_power_product) + (bpv_result_ftsp_square_factor_selected))) /\ forall ff_i_ftsp_square_factor_selected_power_product. (exists ff_lt_ftsp_square_factor_selected_power_product_bound. ff_lt_ftsp_square_factor_selected_power_product_bound + S ff_i_ftsp_square_factor_selected_power_product = e) -> exists ff_p_ftsp_square_factor_selected_power_product ff_r_ftsp_square_factor_selected_power_product ff_s_ftsp_square_factor_selected_power_product. ((((exists ff_h_ftsp_square_factor_selected_power_product_factor. ff_h_ftsp_square_factor_selected_power_product_factor + S (ff_p_ftsp_square_factor_selected_power_product) = S ((S (ff_i_ftsp_square_factor_selected_power_product)) * ff_c_ftsp_square_factor_selected_power)) /\ exists ff_q_ftsp_square_factor_selected_power_product_factor. ff_b_ftsp_square_factor_selected_power = ff_q_ftsp_square_factor_selected_power_product_factor * S ((S (ff_i_ftsp_square_factor_selected_power_product)) * ff_c_ftsp_square_factor_selected_power) + (ff_p_ftsp_square_factor_selected_power_product))) /\ ((((exists ff_h_ftsp_square_factor_selected_power_product_partial. ff_h_ftsp_square_factor_selected_power_product_partial + S (ff_r_ftsp_square_factor_selected_power_product) = S ((S (ff_i_ftsp_square_factor_selected_power_product)) * ff_v_ftsp_square_factor_selected_power_product)) /\ exists ff_q_ftsp_square_factor_selected_power_product_partial. ff_u_ftsp_square_factor_selected_power_product = ff_q_ftsp_square_factor_selected_power_product_partial * S ((S (ff_i_ftsp_square_factor_selected_power_product)) * ff_v_ftsp_square_factor_selected_power_product) + (ff_r_ftsp_square_factor_selected_power_product))) /\ ((((exists ff_h_ftsp_square_factor_selected_power_product_successor. ff_h_ftsp_square_factor_selected_power_product_successor + S (ff_s_ftsp_square_factor_selected_power_product) = S ((S (S ff_i_ftsp_square_factor_selected_power_product)) * ff_v_ftsp_square_factor_selected_power_product)) /\ exists ff_q_ftsp_square_factor_selected_power_product_successor. ff_u_ftsp_square_factor_selected_power_product = ff_q_ftsp_square_factor_selected_power_product_successor * S ((S (S ff_i_ftsp_square_factor_selected_power_product)) * ff_v_ftsp_square_factor_selected_power_product) + (ff_s_ftsp_square_factor_selected_power_product))) /\ ff_s_ftsp_square_factor_selected_power_product = ff_r_ftsp_square_factor_selected_power_product * ff_p_ftsp_square_factor_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_square_factor_selected_divides. z = bpv_result_ftsp_square_factor_selected * bpv_factor_ftsp_square_factor_selected_divides)))) /\ forall bpv_candidate_ftsp_square_factor. (exists bpv_gap_ftsp_square_factor_candidate_bound. bpv_gap_ftsp_square_factor_candidate_bound + bpv_candidate_ftsp_square_factor = z) -> (exists bpv_result_ftsp_square_factor_candidate. ((exists ff_b_ftsp_square_factor_candidate_power ff_c_ftsp_square_factor_candidate_power. ((forall ff_i_ftsp_square_factor_candidate_power_repeat. (exists ff_lt_ftsp_square_factor_candidate_power_repeat_bound. ff_lt_ftsp_square_factor_candidate_power_repeat_bound + S ff_i_ftsp_square_factor_candidate_power_repeat = bpv_candidate_ftsp_square_factor) -> (((exists ff_h_ftsp_square_factor_candidate_power_repeat_decoded. ff_h_ftsp_square_factor_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_square_factor_candidate_power_repeat)) * ff_c_ftsp_square_factor_candidate_power)) /\ exists ff_q_ftsp_square_factor_candidate_power_repeat_decoded. ff_b_ftsp_square_factor_candidate_power = ff_q_ftsp_square_factor_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_square_factor_candidate_power_repeat)) * ff_c_ftsp_square_factor_candidate_power) + (p)))) /\ (exists ff_u_ftsp_square_factor_candidate_power_product ff_v_ftsp_square_factor_candidate_power_product. ((((exists ff_h_ftsp_square_factor_candidate_power_product_start. ff_h_ftsp_square_factor_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_square_factor_candidate_power_product)) /\ exists ff_q_ftsp_square_factor_candidate_power_product_start. ff_u_ftsp_square_factor_candidate_power_product = ff_q_ftsp_square_factor_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_square_factor_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_square_factor_candidate_power_product_terminal. ff_h_ftsp_square_factor_candidate_power_product_terminal + S (bpv_result_ftsp_square_factor_candidate) = S ((S (bpv_candidate_ftsp_square_factor)) * ff_v_ftsp_square_factor_candidate_power_product)) /\ exists ff_q_ftsp_square_factor_candidate_power_product_terminal. ff_u_ftsp_square_factor_candidate_power_product = ff_q_ftsp_square_factor_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_square_factor)) * ff_v_ftsp_square_factor_candidate_power_product) + (bpv_result_ftsp_square_factor_candidate))) /\ forall ff_i_ftsp_square_factor_candidate_power_product. (exists ff_lt_ftsp_square_factor_candidate_power_product_bound. ff_lt_ftsp_square_factor_candidate_power_product_bound + S ff_i_ftsp_square_factor_candidate_power_product = bpv_candidate_ftsp_square_factor) -> exists ff_p_ftsp_square_factor_candidate_power_product ff_r_ftsp_square_factor_candidate_power_product ff_s_ftsp_square_factor_candidate_power_product. ((((exists ff_h_ftsp_square_factor_candidate_power_product_factor. ff_h_ftsp_square_factor_candidate_power_product_factor + S (ff_p_ftsp_square_factor_candidate_power_product) = S ((S (ff_i_ftsp_square_factor_candidate_power_product)) * ff_c_ftsp_square_factor_candidate_power)) /\ exists ff_q_ftsp_square_factor_candidate_power_product_factor. ff_b_ftsp_square_factor_candidate_power = ff_q_ftsp_square_factor_candidate_power_product_factor * S ((S (ff_i_ftsp_square_factor_candidate_power_product)) * ff_c_ftsp_square_factor_candidate_power) + (ff_p_ftsp_square_factor_candidate_power_product))) /\ ((((exists ff_h_ftsp_square_factor_candidate_power_product_partial. ff_h_ftsp_square_factor_candidate_power_product_partial + S (ff_r_ftsp_square_factor_candidate_power_product) = S ((S (ff_i_ftsp_square_factor_candidate_power_product)) * ff_v_ftsp_square_factor_candidate_power_product)) /\ exists ff_q_ftsp_square_factor_candidate_power_product_partial. ff_u_ftsp_square_factor_candidate_power_product = ff_q_ftsp_square_factor_candidate_power_product_partial * S ((S (ff_i_ftsp_square_factor_candidate_power_product)) * ff_v_ftsp_square_factor_candidate_power_product) + (ff_r_ftsp_square_factor_candidate_power_product))) /\ ((((exists ff_h_ftsp_square_factor_candidate_power_product_successor. ff_h_ftsp_square_factor_candidate_power_product_successor + S (ff_s_ftsp_square_factor_candidate_power_product) = S ((S (S ff_i_ftsp_square_factor_candidate_power_product)) * ff_v_ftsp_square_factor_candidate_power_product)) /\ exists ff_q_ftsp_square_factor_candidate_power_product_successor. ff_u_ftsp_square_factor_candidate_power_product = ff_q_ftsp_square_factor_candidate_power_product_successor * S ((S (S ff_i_ftsp_square_factor_candidate_power_product)) * ff_v_ftsp_square_factor_candidate_power_product) + (ff_s_ftsp_square_factor_candidate_power_product))) /\ ff_s_ftsp_square_factor_candidate_power_product = ff_r_ftsp_square_factor_candidate_power_product * ff_p_ftsp_square_factor_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_square_factor_candidate_divides. z = bpv_result_ftsp_square_factor_candidate * bpv_factor_ftsp_square_factor_candidate_divides))) -> (exists bpv_gap_ftsp_square_factor_maximal. bpv_gap_ftsp_square_factor_maximal + bpv_candidate_ftsp_square_factor = e))
  12. 0012apply power_valuation_exists
  13. 0013cases hzvaluation
  14. 0014have hproduct : exists g. (((exists bpv_gap_ftsp_square_product_exponent_bound. bpv_gap_ftsp_square_product_exponent_bound + g = ((z * z) * n)) /\ (exists bpv_result_ftsp_square_product_selected. ((exists ff_b_ftsp_square_product_selected_power ff_c_ftsp_square_product_selected_power. ((forall ff_i_ftsp_square_product_selected_power_repeat. (exists ff_lt_ftsp_square_product_selected_power_repeat_bound. ff_lt_ftsp_square_product_selected_power_repeat_bound + S ff_i_ftsp_square_product_selected_power_repeat = g) -> (((exists ff_h_ftsp_square_product_selected_power_repeat_decoded. ff_h_ftsp_square_product_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_square_product_selected_power_repeat)) * ff_c_ftsp_square_product_selected_power)) /\ exists ff_q_ftsp_square_product_selected_power_repeat_decoded. ff_b_ftsp_square_product_selected_power = ff_q_ftsp_square_product_selected_power_repeat_decoded * S ((S (ff_i_ftsp_square_product_selected_power_repeat)) * ff_c_ftsp_square_product_selected_power) + (p)))) /\ (exists ff_u_ftsp_square_product_selected_power_product ff_v_ftsp_square_product_selected_power_product. ((((exists ff_h_ftsp_square_product_selected_power_product_start. ff_h_ftsp_square_product_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_square_product_selected_power_product)) /\ exists ff_q_ftsp_square_product_selected_power_product_start. ff_u_ftsp_square_product_selected_power_product = ff_q_ftsp_square_product_selected_power_product_start * S ((S (0)) * ff_v_ftsp_square_product_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_square_product_selected_power_product_terminal. ff_h_ftsp_square_product_selected_power_product_terminal + S (bpv_result_ftsp_square_product_selected) = S ((S (g)) * ff_v_ftsp_square_product_selected_power_product)) /\ exists ff_q_ftsp_square_product_selected_power_product_terminal. ff_u_ftsp_square_product_selected_power_product = ff_q_ftsp_square_product_selected_power_product_terminal * S ((S (g)) * ff_v_ftsp_square_product_selected_power_product) + (bpv_result_ftsp_square_product_selected))) /\ forall ff_i_ftsp_square_product_selected_power_product. (exists ff_lt_ftsp_square_product_selected_power_product_bound. ff_lt_ftsp_square_product_selected_power_product_bound + S ff_i_ftsp_square_product_selected_power_product = g) -> exists ff_p_ftsp_square_product_selected_power_product ff_r_ftsp_square_product_selected_power_product ff_s_ftsp_square_product_selected_power_product. ((((exists ff_h_ftsp_square_product_selected_power_product_factor. ff_h_ftsp_square_product_selected_power_product_factor + S (ff_p_ftsp_square_product_selected_power_product) = S ((S (ff_i_ftsp_square_product_selected_power_product)) * ff_c_ftsp_square_product_selected_power)) /\ exists ff_q_ftsp_square_product_selected_power_product_factor. ff_b_ftsp_square_product_selected_power = ff_q_ftsp_square_product_selected_power_product_factor * S ((S (ff_i_ftsp_square_product_selected_power_product)) * ff_c_ftsp_square_product_selected_power) + (ff_p_ftsp_square_product_selected_power_product))) /\ ((((exists ff_h_ftsp_square_product_selected_power_product_partial. ff_h_ftsp_square_product_selected_power_product_partial + S (ff_r_ftsp_square_product_selected_power_product) = S ((S (ff_i_ftsp_square_product_selected_power_product)) * ff_v_ftsp_square_product_selected_power_product)) /\ exists ff_q_ftsp_square_product_selected_power_product_partial. ff_u_ftsp_square_product_selected_power_product = ff_q_ftsp_square_product_selected_power_product_partial * S ((S (ff_i_ftsp_square_product_selected_power_product)) * ff_v_ftsp_square_product_selected_power_product) + (ff_r_ftsp_square_product_selected_power_product))) /\ ((((exists ff_h_ftsp_square_product_selected_power_product_successor. ff_h_ftsp_square_product_selected_power_product_successor + S (ff_s_ftsp_square_product_selected_power_product) = S ((S (S ff_i_ftsp_square_product_selected_power_product)) * ff_v_ftsp_square_product_selected_power_product)) /\ exists ff_q_ftsp_square_product_selected_power_product_successor. ff_u_ftsp_square_product_selected_power_product = ff_q_ftsp_square_product_selected_power_product_successor * S ((S (S ff_i_ftsp_square_product_selected_power_product)) * ff_v_ftsp_square_product_selected_power_product) + (ff_s_ftsp_square_product_selected_power_product))) /\ ff_s_ftsp_square_product_selected_power_product = ff_r_ftsp_square_product_selected_power_product * ff_p_ftsp_square_product_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_square_product_selected_divides. ((z * z) * n) = bpv_result_ftsp_square_product_selected * bpv_factor_ftsp_square_product_selected_divides)))) /\ forall bpv_candidate_ftsp_square_product. (exists bpv_gap_ftsp_square_product_candidate_bound. bpv_gap_ftsp_square_product_candidate_bound + bpv_candidate_ftsp_square_product = ((z * z) * n)) -> (exists bpv_result_ftsp_square_product_candidate. ((exists ff_b_ftsp_square_product_candidate_power ff_c_ftsp_square_product_candidate_power. ((forall ff_i_ftsp_square_product_candidate_power_repeat. (exists ff_lt_ftsp_square_product_candidate_power_repeat_bound. ff_lt_ftsp_square_product_candidate_power_repeat_bound + S ff_i_ftsp_square_product_candidate_power_repeat = bpv_candidate_ftsp_square_product) -> (((exists ff_h_ftsp_square_product_candidate_power_repeat_decoded. ff_h_ftsp_square_product_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_square_product_candidate_power_repeat)) * ff_c_ftsp_square_product_candidate_power)) /\ exists ff_q_ftsp_square_product_candidate_power_repeat_decoded. ff_b_ftsp_square_product_candidate_power = ff_q_ftsp_square_product_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_square_product_candidate_power_repeat)) * ff_c_ftsp_square_product_candidate_power) + (p)))) /\ (exists ff_u_ftsp_square_product_candidate_power_product ff_v_ftsp_square_product_candidate_power_product. ((((exists ff_h_ftsp_square_product_candidate_power_product_start. ff_h_ftsp_square_product_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_square_product_candidate_power_product)) /\ exists ff_q_ftsp_square_product_candidate_power_product_start. ff_u_ftsp_square_product_candidate_power_product = ff_q_ftsp_square_product_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_square_product_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_square_product_candidate_power_product_terminal. ff_h_ftsp_square_product_candidate_power_product_terminal + S (bpv_result_ftsp_square_product_candidate) = S ((S (bpv_candidate_ftsp_square_product)) * ff_v_ftsp_square_product_candidate_power_product)) /\ exists ff_q_ftsp_square_product_candidate_power_product_terminal. ff_u_ftsp_square_product_candidate_power_product = ff_q_ftsp_square_product_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_square_product)) * ff_v_ftsp_square_product_candidate_power_product) + (bpv_result_ftsp_square_product_candidate))) /\ forall ff_i_ftsp_square_product_candidate_power_product. (exists ff_lt_ftsp_square_product_candidate_power_product_bound. ff_lt_ftsp_square_product_candidate_power_product_bound + S ff_i_ftsp_square_product_candidate_power_product = bpv_candidate_ftsp_square_product) -> exists ff_p_ftsp_square_product_candidate_power_product ff_r_ftsp_square_product_candidate_power_product ff_s_ftsp_square_product_candidate_power_product. ((((exists ff_h_ftsp_square_product_candidate_power_product_factor. ff_h_ftsp_square_product_candidate_power_product_factor + S (ff_p_ftsp_square_product_candidate_power_product) = S ((S (ff_i_ftsp_square_product_candidate_power_product)) * ff_c_ftsp_square_product_candidate_power)) /\ exists ff_q_ftsp_square_product_candidate_power_product_factor. ff_b_ftsp_square_product_candidate_power = ff_q_ftsp_square_product_candidate_power_product_factor * S ((S (ff_i_ftsp_square_product_candidate_power_product)) * ff_c_ftsp_square_product_candidate_power) + (ff_p_ftsp_square_product_candidate_power_product))) /\ ((((exists ff_h_ftsp_square_product_candidate_power_product_partial. ff_h_ftsp_square_product_candidate_power_product_partial + S (ff_r_ftsp_square_product_candidate_power_product) = S ((S (ff_i_ftsp_square_product_candidate_power_product)) * ff_v_ftsp_square_product_candidate_power_product)) /\ exists ff_q_ftsp_square_product_candidate_power_product_partial. ff_u_ftsp_square_product_candidate_power_product = ff_q_ftsp_square_product_candidate_power_product_partial * S ((S (ff_i_ftsp_square_product_candidate_power_product)) * ff_v_ftsp_square_product_candidate_power_product) + (ff_r_ftsp_square_product_candidate_power_product))) /\ ((((exists ff_h_ftsp_square_product_candidate_power_product_successor. ff_h_ftsp_square_product_candidate_power_product_successor + S (ff_s_ftsp_square_product_candidate_power_product) = S ((S (S ff_i_ftsp_square_product_candidate_power_product)) * ff_v_ftsp_square_product_candidate_power_product)) /\ exists ff_q_ftsp_square_product_candidate_power_product_successor. ff_u_ftsp_square_product_candidate_power_product = ff_q_ftsp_square_product_candidate_power_product_successor * S ((S (S ff_i_ftsp_square_product_candidate_power_product)) * ff_v_ftsp_square_product_candidate_power_product) + (ff_s_ftsp_square_product_candidate_power_product))) /\ ff_s_ftsp_square_product_candidate_power_product = ff_r_ftsp_square_product_candidate_power_product * ff_p_ftsp_square_product_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_square_product_candidate_divides. ((z * z) * n) = bpv_result_ftsp_square_product_candidate * bpv_factor_ftsp_square_product_candidate_divides))) -> (exists bpv_gap_ftsp_square_product_maximal. bpv_gap_ftsp_square_product_maximal + bpv_candidate_ftsp_square_product = g))
  15. 0015apply power_valuation_exists
  16. 0016cases hproduct
  17. 0017have hrightvaluation : (((exists bpv_gap_ftsp_square_right_transport_exponent_bound. bpv_gap_ftsp_square_right_transport_exponent_bound + x1 = (n * (z * z))) /\ (exists bpv_result_ftsp_square_right_transport_selected. ((exists ff_b_ftsp_square_right_transport_selected_power ff_c_ftsp_square_right_transport_selected_power. ((forall ff_i_ftsp_square_right_transport_selected_power_repeat. (exists ff_lt_ftsp_square_right_transport_selected_power_repeat_bound. ff_lt_ftsp_square_right_transport_selected_power_repeat_bound + S ff_i_ftsp_square_right_transport_selected_power_repeat = x1) -> (((exists ff_h_ftsp_square_right_transport_selected_power_repeat_decoded. ff_h_ftsp_square_right_transport_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_square_right_transport_selected_power_repeat)) * ff_c_ftsp_square_right_transport_selected_power)) /\ exists ff_q_ftsp_square_right_transport_selected_power_repeat_decoded. ff_b_ftsp_square_right_transport_selected_power = ff_q_ftsp_square_right_transport_selected_power_repeat_decoded * S ((S (ff_i_ftsp_square_right_transport_selected_power_repeat)) * ff_c_ftsp_square_right_transport_selected_power) + (p)))) /\ (exists ff_u_ftsp_square_right_transport_selected_power_product ff_v_ftsp_square_right_transport_selected_power_product. ((((exists ff_h_ftsp_square_right_transport_selected_power_product_start. ff_h_ftsp_square_right_transport_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_square_right_transport_selected_power_product)) /\ exists ff_q_ftsp_square_right_transport_selected_power_product_start. ff_u_ftsp_square_right_transport_selected_power_product = ff_q_ftsp_square_right_transport_selected_power_product_start * S ((S (0)) * ff_v_ftsp_square_right_transport_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_square_right_transport_selected_power_product_terminal. ff_h_ftsp_square_right_transport_selected_power_product_terminal + S (bpv_result_ftsp_square_right_transport_selected) = S ((S (x1)) * ff_v_ftsp_square_right_transport_selected_power_product)) /\ exists ff_q_ftsp_square_right_transport_selected_power_product_terminal. ff_u_ftsp_square_right_transport_selected_power_product = ff_q_ftsp_square_right_transport_selected_power_product_terminal * S ((S (x1)) * ff_v_ftsp_square_right_transport_selected_power_product) + (bpv_result_ftsp_square_right_transport_selected))) /\ forall ff_i_ftsp_square_right_transport_selected_power_product. (exists ff_lt_ftsp_square_right_transport_selected_power_product_bound. ff_lt_ftsp_square_right_transport_selected_power_product_bound + S ff_i_ftsp_square_right_transport_selected_power_product = x1) -> exists ff_p_ftsp_square_right_transport_selected_power_product ff_r_ftsp_square_right_transport_selected_power_product ff_s_ftsp_square_right_transport_selected_power_product. ((((exists ff_h_ftsp_square_right_transport_selected_power_product_factor. ff_h_ftsp_square_right_transport_selected_power_product_factor + S (ff_p_ftsp_square_right_transport_selected_power_product) = S ((S (ff_i_ftsp_square_right_transport_selected_power_product)) * ff_c_ftsp_square_right_transport_selected_power)) /\ exists ff_q_ftsp_square_right_transport_selected_power_product_factor. ff_b_ftsp_square_right_transport_selected_power = ff_q_ftsp_square_right_transport_selected_power_product_factor * S ((S (ff_i_ftsp_square_right_transport_selected_power_product)) * ff_c_ftsp_square_right_transport_selected_power) + (ff_p_ftsp_square_right_transport_selected_power_product))) /\ ((((exists ff_h_ftsp_square_right_transport_selected_power_product_partial. ff_h_ftsp_square_right_transport_selected_power_product_partial + S (ff_r_ftsp_square_right_transport_selected_power_product) = S ((S (ff_i_ftsp_square_right_transport_selected_power_product)) * ff_v_ftsp_square_right_transport_selected_power_product)) /\ exists ff_q_ftsp_square_right_transport_selected_power_product_partial. ff_u_ftsp_square_right_transport_selected_power_product = ff_q_ftsp_square_right_transport_selected_power_product_partial * S ((S (ff_i_ftsp_square_right_transport_selected_power_product)) * ff_v_ftsp_square_right_transport_selected_power_product) + (ff_r_ftsp_square_right_transport_selected_power_product))) /\ ((((exists ff_h_ftsp_square_right_transport_selected_power_product_successor. ff_h_ftsp_square_right_transport_selected_power_product_successor + S (ff_s_ftsp_square_right_transport_selected_power_product) = S ((S (S ff_i_ftsp_square_right_transport_selected_power_product)) * ff_v_ftsp_square_right_transport_selected_power_product)) /\ exists ff_q_ftsp_square_right_transport_selected_power_product_successor. ff_u_ftsp_square_right_transport_selected_power_product = ff_q_ftsp_square_right_transport_selected_power_product_successor * S ((S (S ff_i_ftsp_square_right_transport_selected_power_product)) * ff_v_ftsp_square_right_transport_selected_power_product) + (ff_s_ftsp_square_right_transport_selected_power_product))) /\ ff_s_ftsp_square_right_transport_selected_power_product = ff_r_ftsp_square_right_transport_selected_power_product * ff_p_ftsp_square_right_transport_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_square_right_transport_selected_divides. (n * (z * z)) = bpv_result_ftsp_square_right_transport_selected * bpv_factor_ftsp_square_right_transport_selected_divides)))) /\ forall bpv_candidate_ftsp_square_right_transport. (exists bpv_gap_ftsp_square_right_transport_candidate_bound. bpv_gap_ftsp_square_right_transport_candidate_bound + bpv_candidate_ftsp_square_right_transport = (n * (z * z))) -> (exists bpv_result_ftsp_square_right_transport_candidate. ((exists ff_b_ftsp_square_right_transport_candidate_power ff_c_ftsp_square_right_transport_candidate_power. ((forall ff_i_ftsp_square_right_transport_candidate_power_repeat. (exists ff_lt_ftsp_square_right_transport_candidate_power_repeat_bound. ff_lt_ftsp_square_right_transport_candidate_power_repeat_bound + S ff_i_ftsp_square_right_transport_candidate_power_repeat = bpv_candidate_ftsp_square_right_transport) -> (((exists ff_h_ftsp_square_right_transport_candidate_power_repeat_decoded. ff_h_ftsp_square_right_transport_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_square_right_transport_candidate_power_repeat)) * ff_c_ftsp_square_right_transport_candidate_power)) /\ exists ff_q_ftsp_square_right_transport_candidate_power_repeat_decoded. ff_b_ftsp_square_right_transport_candidate_power = ff_q_ftsp_square_right_transport_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_square_right_transport_candidate_power_repeat)) * ff_c_ftsp_square_right_transport_candidate_power) + (p)))) /\ (exists ff_u_ftsp_square_right_transport_candidate_power_product ff_v_ftsp_square_right_transport_candidate_power_product. ((((exists ff_h_ftsp_square_right_transport_candidate_power_product_start. ff_h_ftsp_square_right_transport_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_square_right_transport_candidate_power_product)) /\ exists ff_q_ftsp_square_right_transport_candidate_power_product_start. ff_u_ftsp_square_right_transport_candidate_power_product = ff_q_ftsp_square_right_transport_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_square_right_transport_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_square_right_transport_candidate_power_product_terminal. ff_h_ftsp_square_right_transport_candidate_power_product_terminal + S (bpv_result_ftsp_square_right_transport_candidate) = S ((S (bpv_candidate_ftsp_square_right_transport)) * ff_v_ftsp_square_right_transport_candidate_power_product)) /\ exists ff_q_ftsp_square_right_transport_candidate_power_product_terminal. ff_u_ftsp_square_right_transport_candidate_power_product = ff_q_ftsp_square_right_transport_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_square_right_transport)) * ff_v_ftsp_square_right_transport_candidate_power_product) + (bpv_result_ftsp_square_right_transport_candidate))) /\ forall ff_i_ftsp_square_right_transport_candidate_power_product. (exists ff_lt_ftsp_square_right_transport_candidate_power_product_bound. ff_lt_ftsp_square_right_transport_candidate_power_product_bound + S ff_i_ftsp_square_right_transport_candidate_power_product = bpv_candidate_ftsp_square_right_transport) -> exists ff_p_ftsp_square_right_transport_candidate_power_product ff_r_ftsp_square_right_transport_candidate_power_product ff_s_ftsp_square_right_transport_candidate_power_product. ((((exists ff_h_ftsp_square_right_transport_candidate_power_product_factor. ff_h_ftsp_square_right_transport_candidate_power_product_factor + S (ff_p_ftsp_square_right_transport_candidate_power_product) = S ((S (ff_i_ftsp_square_right_transport_candidate_power_product)) * ff_c_ftsp_square_right_transport_candidate_power)) /\ exists ff_q_ftsp_square_right_transport_candidate_power_product_factor. ff_b_ftsp_square_right_transport_candidate_power = ff_q_ftsp_square_right_transport_candidate_power_product_factor * S ((S (ff_i_ftsp_square_right_transport_candidate_power_product)) * ff_c_ftsp_square_right_transport_candidate_power) + (ff_p_ftsp_square_right_transport_candidate_power_product))) /\ ((((exists ff_h_ftsp_square_right_transport_candidate_power_product_partial. ff_h_ftsp_square_right_transport_candidate_power_product_partial + S (ff_r_ftsp_square_right_transport_candidate_power_product) = S ((S (ff_i_ftsp_square_right_transport_candidate_power_product)) * ff_v_ftsp_square_right_transport_candidate_power_product)) /\ exists ff_q_ftsp_square_right_transport_candidate_power_product_partial. ff_u_ftsp_square_right_transport_candidate_power_product = ff_q_ftsp_square_right_transport_candidate_power_product_partial * S ((S (ff_i_ftsp_square_right_transport_candidate_power_product)) * ff_v_ftsp_square_right_transport_candidate_power_product) + (ff_r_ftsp_square_right_transport_candidate_power_product))) /\ ((((exists ff_h_ftsp_square_right_transport_candidate_power_product_successor. ff_h_ftsp_square_right_transport_candidate_power_product_successor + S (ff_s_ftsp_square_right_transport_candidate_power_product) = S ((S (S ff_i_ftsp_square_right_transport_candidate_power_product)) * ff_v_ftsp_square_right_transport_candidate_power_product)) /\ exists ff_q_ftsp_square_right_transport_candidate_power_product_successor. ff_u_ftsp_square_right_transport_candidate_power_product = ff_q_ftsp_square_right_transport_candidate_power_product_successor * S ((S (S ff_i_ftsp_square_right_transport_candidate_power_product)) * ff_v_ftsp_square_right_transport_candidate_power_product) + (ff_s_ftsp_square_right_transport_candidate_power_product))) /\ ff_s_ftsp_square_right_transport_candidate_power_product = ff_r_ftsp_square_right_transport_candidate_power_product * ff_p_ftsp_square_right_transport_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_square_right_transport_candidate_divides. (n * (z * z)) = bpv_result_ftsp_square_right_transport_candidate * bpv_factor_ftsp_square_right_transport_candidate_divides))) -> (exists bpv_gap_ftsp_square_right_transport_maximal. bpv_gap_ftsp_square_right_transport_maximal + bpv_candidate_ftsp_square_right_transport = x1))
  18. 0018specialize power_valuation_value_eq_transport p
  19. 0019specialize power_valuation_value_eq_transport ((z * z) * n)
  20. 0020specialize power_valuation_value_eq_transport (n * (z * z))
  21. 0021specialize power_valuation_value_eq_transport x1
  22. 0022apply power_valuation_value_eq_transport
  23. 0023apply mul_comm
  24. 0024exact hproduct_witness
  25. 0025have heven : exists h. x1 = h + h
  26. 0026specialize htotal p
  27. 0027specialize htotal x1
  28. 0028apply htotal
  29. 0029exact hpprime
  30. 0030exact hpbad
  31. 0031exact hrightvaluation
  32. 0032specialize square_factor_even_valuation_reflects_cofactor p
  33. 0033specialize square_factor_even_valuation_reflects_cofactor z
  34. 0034specialize square_factor_even_valuation_reflects_cofactor n
  35. 0035specialize square_factor_even_valuation_reflects_cofactor x
  36. 0036specialize square_factor_even_valuation_reflects_cofactor f
  37. 0037specialize square_factor_even_valuation_reflects_cofactor x1
  38. 0038apply square_factor_even_valuation_reflects_cofactor
  39. 0039exact hpprime
  40. 0040exact hznonzero
  41. 0041exact hnnonzero
  42. 0042exact hzvaluation_witness
  43. 0043exact hnvaluation
  44. 0044exact hproduct_witness
  45. 0045exact heven