TS003E · theorem body

nonzero_two_square_iff_even_three_mod_four_prime_valuations

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ n. ¬n = 0 → ((∃ x. ∃ y. n = x · x + y · y) → ∀ x. ∀ y. Prime(x) → Mod4Three(x) → PowerValuation(x,n,y) → ∃ z. y = z + z) ∧ ((∀ x. ∀ y. Prime(x) → Mod4Three(x) → PowerValuation(x,n,y) → ∃ z. y = z + z) → ∃ x. ∃ y. n = x · x + y · y)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0012 Mod4Three PD0046 PowerValuation

In local proof propositions

none
Exact expanded first-order 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)))

Proof neighborhood

Direct theorem prerequisites

TS003V three_mod_four_prime_represented_nonzero_valuation_even TS003D positive_number_with_even_bad_prime_valuations_is_two_square

Direct theorem dependents

TS003F two_square_iff_zero_or_even_three_mod_four_prime_valuations

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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