TS003E

nonzero_two_square_iff_even_three_mod_four_prime_valuations

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

Complete nonzero Fermat two-square classification: witnessed representation is equivalent to even valuation at every three-modulo-four prime.

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 n. ~(n = 0) -> (((exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result) -> (forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value)) /\ ((forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value) -> (exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result)))

Constructive proof overview

Generated structural guide

Complete nonzero Fermat two-square classification: witnessed representation is equivalent to even valuation at every three-modulo-four prime.

The unchanged tactic script uses 2 declared prerequisites and contains 23 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

TS003V three_mod_four_prime_represented_nonzero_valuation_even TS003D positive_number_with_even_bad_prime_valuations_is_two_square

Direct dependents

TS003F two_square_iff_zero_or_even_three_mod_four_prime_valuations

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

23 script commands · 6 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
three mod four prime represented nonzero valuation evenpositive number with even bad prime valuations is two square
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hnonzero
02Separate the logical casesL3–3

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

  1. L3
    split
03Fix variables and assumptionsL4–9

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

  1. L4
    intro hrepresented
  2. L5
    intro p
  3. L6
    intro e
  4. L7
    intro hprime
  5. L8
    intro hthree
  6. L9
    intro hvaluation
04Use earlier factsL10–18

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

  1. L10
    specialize three_mod_four_prime_represented_nonzero_valuation_even p
  2. L11
    specialize three_mod_four_prime_represented_nonzero_valuation_even n
  3. L12
    specialize three_mod_four_prime_represented_nonzero_valuation_even e
  4. L13
    apply three_mod_four_prime_represented_nonzero_valuation_even
  5. L14
    exact hprime
  6. L15
    exact hthree
  7. L16
    exact hnonzero
  8. L17
    exact hrepresented
  9. L18
    exact hvaluation
05Fix variables and assumptionsL19–19

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

  1. L19
    intro hparity
06Use earlier factsL20–23

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

  1. L20
    specialize positive_number_with_even_bad_prime_valuations_is_two_square n
  2. L21
    apply positive_number_with_even_bad_prime_valuations_is_two_square
  3. L22
    exact hnonzero
  4. L23
    exact hparity

Library-wide reading audit

Original exact command ledger · 23 lines
  1. 0001intro n
  2. 0002intro hnonzero
  3. 0003split
  4. 0004intro hrepresented
  5. 0005intro p
  6. 0006intro e
  7. 0007intro hprime
  8. 0008intro hthree
  9. 0009intro hvaluation
  10. 0010specialize three_mod_four_prime_represented_nonzero_valuation_even p
  11. 0011specialize three_mod_four_prime_represented_nonzero_valuation_even n
  12. 0012specialize three_mod_four_prime_represented_nonzero_valuation_even e
  13. 0013apply three_mod_four_prime_represented_nonzero_valuation_even
  14. 0014exact hprime
  15. 0015exact hthree
  16. 0016exact hnonzero
  17. 0017exact hrepresented
  18. 0018exact hvaluation
  19. 0019intro hparity
  20. 0020specialize positive_number_with_even_bad_prime_valuations_is_two_square n
  21. 0021apply positive_number_with_even_bad_prime_valuations_is_two_square
  22. 0022exact hnonzero
  23. 0023exact hparity