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 p a b e. ((~(p = 1) /\ forall frm_prime_left_ftsv_prime frm_prime_right_ftsv_prime. p = frm_prime_left_ftsv_prime * frm_prime_right_ftsv_prime -> frm_prime_left_ftsv_prime = 1 \/ frm_prime_right_ftsv_prime = 1)) -> (exists ftsc_four_three_ftsv_prime. (p) = 4 * ftsc_four_three_ftsv_prime + 3) -> ~(a * a + b * b = 0) -> (((exists bpv_gap_ftsv_norm_valuation_exponent_bound. bpv_gap_ftsv_norm_valuation_exponent_bound + e = (a * a + b * b)) /\ (exists bpv_result_ftsv_norm_valuation_selected. ((exists ff_b_ftsv_norm_valuation_selected_power ff_c_ftsv_norm_valuation_selected_power. ((forall ff_i_ftsv_norm_valuation_selected_power_repeat. (exists ff_lt_ftsv_norm_valuation_selected_power_repeat_bound. ff_lt_ftsv_norm_valuation_selected_power_repeat_bound + S ff_i_ftsv_norm_valuation_selected_power_repeat = e) -> (((exists ff_h_ftsv_norm_valuation_selected_power_repeat_decoded. ff_h_ftsv_norm_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_norm_valuation_selected_power_repeat)) * ff_c_ftsv_norm_valuation_selected_power)) /\ exists ff_q_ftsv_norm_valuation_selected_power_repeat_decoded. ff_b_ftsv_norm_valuation_selected_power = ff_q_ftsv_norm_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsv_norm_valuation_selected_power_repeat)) * ff_c_ftsv_norm_valuation_selected_power) + (p)))) /\ (exists ff_u_ftsv_norm_valuation_selected_power_product ff_v_ftsv_norm_valuation_selected_power_product. ((((exists ff_h_ftsv_norm_valuation_selected_power_product_start. ff_h_ftsv_norm_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_norm_valuation_selected_power_product)) /\ exists ff_q_ftsv_norm_valuation_selected_power_product_start. ff_u_ftsv_norm_valuation_selected_power_product = ff_q_ftsv_norm_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsv_norm_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_norm_valuation_selected_power_product_terminal. ff_h_ftsv_norm_valuation_selected_power_product_terminal + S (bpv_result_ftsv_norm_valuation_selected) = S ((S (e)) * ff_v_ftsv_norm_valuation_selected_power_product)) /\ exists ff_q_ftsv_norm_valuation_selected_power_product_terminal. ff_u_ftsv_norm_valuation_selected_power_product = ff_q_ftsv_norm_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_ftsv_norm_valuation_selected_power_product) + (bpv_result_ftsv_norm_valuation_selected))) /\ forall ff_i_ftsv_norm_valuation_selected_power_product. (exists ff_lt_ftsv_norm_valuation_selected_power_product_bound. ff_lt_ftsv_norm_valuation_selected_power_product_bound + S ff_i_ftsv_norm_valuation_selected_power_product = e) -> exists ff_p_ftsv_norm_valuation_selected_power_product ff_r_ftsv_norm_valuation_selected_power_product ff_s_ftsv_norm_valuation_selected_power_product. ((((exists ff_h_ftsv_norm_valuation_selected_power_product_factor. ff_h_ftsv_norm_valuation_selected_power_product_factor + S (ff_p_ftsv_norm_valuation_selected_power_product) = S ((S (ff_i_ftsv_norm_valuation_selected_power_product)) * ff_c_ftsv_norm_valuation_selected_power)) /\ exists ff_q_ftsv_norm_valuation_selected_power_product_factor. ff_b_ftsv_norm_valuation_selected_power = ff_q_ftsv_norm_valuation_selected_power_product_factor * S ((S (ff_i_ftsv_norm_valuation_selected_power_product)) * ff_c_ftsv_norm_valuation_selected_power) + (ff_p_ftsv_norm_valuation_selected_power_product))) /\ ((((exists ff_h_ftsv_norm_valuation_selected_power_product_partial. ff_h_ftsv_norm_valuation_selected_power_product_partial + S (ff_r_ftsv_norm_valuation_selected_power_product) = S ((S (ff_i_ftsv_norm_valuation_selected_power_product)) * ff_v_ftsv_norm_valuation_selected_power_product)) /\ exists ff_q_ftsv_norm_valuation_selected_power_product_partial. ff_u_ftsv_norm_valuation_selected_power_product = ff_q_ftsv_norm_valuation_selected_power_product_partial * S ((S (ff_i_ftsv_norm_valuation_selected_power_product)) * ff_v_ftsv_norm_valuation_selected_power_product) + (ff_r_ftsv_norm_valuation_selected_power_product))) /\ ((((exists ff_h_ftsv_norm_valuation_selected_power_product_successor. ff_h_ftsv_norm_valuation_selected_power_product_successor + S (ff_s_ftsv_norm_valuation_selected_power_product) = S ((S (S ff_i_ftsv_norm_valuation_selected_power_product)) * ff_v_ftsv_norm_valuation_selected_power_product)) /\ exists ff_q_ftsv_norm_valuation_selected_power_product_successor. ff_u_ftsv_norm_valuation_selected_power_product = ff_q_ftsv_norm_valuation_selected_power_product_successor * S ((S (S ff_i_ftsv_norm_valuation_selected_power_product)) * ff_v_ftsv_norm_valuation_selected_power_product) + (ff_s_ftsv_norm_valuation_selected_power_product))) /\ ff_s_ftsv_norm_valuation_selected_power_product = ff_r_ftsv_norm_valuation_selected_power_product * ff_p_ftsv_norm_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_norm_valuation_selected_divides. (a * a + b * b) = bpv_result_ftsv_norm_valuation_selected * bpv_factor_ftsv_norm_valuation_selected_divides)))) /\ forall bpv_candidate_ftsv_norm_valuation. (exists bpv_gap_ftsv_norm_valuation_candidate_bound. bpv_gap_ftsv_norm_valuation_candidate_bound + bpv_candidate_ftsv_norm_valuation = (a * a + b * b)) -> (exists bpv_result_ftsv_norm_valuation_candidate. ((exists ff_b_ftsv_norm_valuation_candidate_power ff_c_ftsv_norm_valuation_candidate_power. ((forall ff_i_ftsv_norm_valuation_candidate_power_repeat. (exists ff_lt_ftsv_norm_valuation_candidate_power_repeat_bound. ff_lt_ftsv_norm_valuation_candidate_power_repeat_bound + S ff_i_ftsv_norm_valuation_candidate_power_repeat = bpv_candidate_ftsv_norm_valuation) -> (((exists ff_h_ftsv_norm_valuation_candidate_power_repeat_decoded. ff_h_ftsv_norm_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_norm_valuation_candidate_power_repeat)) * ff_c_ftsv_norm_valuation_candidate_power)) /\ exists ff_q_ftsv_norm_valuation_candidate_power_repeat_decoded. ff_b_ftsv_norm_valuation_candidate_power = ff_q_ftsv_norm_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_norm_valuation_candidate_power_repeat)) * ff_c_ftsv_norm_valuation_candidate_power) + (p)))) /\ (exists ff_u_ftsv_norm_valuation_candidate_power_product ff_v_ftsv_norm_valuation_candidate_power_product. ((((exists ff_h_ftsv_norm_valuation_candidate_power_product_start. ff_h_ftsv_norm_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_norm_valuation_candidate_power_product)) /\ exists ff_q_ftsv_norm_valuation_candidate_power_product_start. ff_u_ftsv_norm_valuation_candidate_power_product = ff_q_ftsv_norm_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_norm_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_norm_valuation_candidate_power_product_terminal. ff_h_ftsv_norm_valuation_candidate_power_product_terminal + S (bpv_result_ftsv_norm_valuation_candidate) = S ((S (bpv_candidate_ftsv_norm_valuation)) * ff_v_ftsv_norm_valuation_candidate_power_product)) /\ exists ff_q_ftsv_norm_valuation_candidate_power_product_terminal. ff_u_ftsv_norm_valuation_candidate_power_product = ff_q_ftsv_norm_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_norm_valuation)) * ff_v_ftsv_norm_valuation_candidate_power_product) + (bpv_result_ftsv_norm_valuation_candidate))) /\ forall ff_i_ftsv_norm_valuation_candidate_power_product. (exists ff_lt_ftsv_norm_valuation_candidate_power_product_bound. ff_lt_ftsv_norm_valuation_candidate_power_product_bound + S ff_i_ftsv_norm_valuation_candidate_power_product = bpv_candidate_ftsv_norm_valuation) -> exists ff_p_ftsv_norm_valuation_candidate_power_product ff_r_ftsv_norm_valuation_candidate_power_product ff_s_ftsv_norm_valuation_candidate_power_product. ((((exists ff_h_ftsv_norm_valuation_candidate_power_product_factor. ff_h_ftsv_norm_valuation_candidate_power_product_factor + S (ff_p_ftsv_norm_valuation_candidate_power_product) = S ((S (ff_i_ftsv_norm_valuation_candidate_power_product)) * ff_c_ftsv_norm_valuation_candidate_power)) /\ exists ff_q_ftsv_norm_valuation_candidate_power_product_factor. ff_b_ftsv_norm_valuation_candidate_power = ff_q_ftsv_norm_valuation_candidate_power_product_factor * S ((S (ff_i_ftsv_norm_valuation_candidate_power_product)) * ff_c_ftsv_norm_valuation_candidate_power) + (ff_p_ftsv_norm_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsv_norm_valuation_candidate_power_product_partial. ff_h_ftsv_norm_valuation_candidate_power_product_partial + S (ff_r_ftsv_norm_valuation_candidate_power_product) = S ((S (ff_i_ftsv_norm_valuation_candidate_power_product)) * ff_v_ftsv_norm_valuation_candidate_power_product)) /\ exists ff_q_ftsv_norm_valuation_candidate_power_product_partial. ff_u_ftsv_norm_valuation_candidate_power_product = ff_q_ftsv_norm_valuation_candidate_power_product_partial * S ((S (ff_i_ftsv_norm_valuation_candidate_power_product)) * ff_v_ftsv_norm_valuation_candidate_power_product) + (ff_r_ftsv_norm_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsv_norm_valuation_candidate_power_product_successor. ff_h_ftsv_norm_valuation_candidate_power_product_successor + S (ff_s_ftsv_norm_valuation_candidate_power_product) = S ((S (S ff_i_ftsv_norm_valuation_candidate_power_product)) * ff_v_ftsv_norm_valuation_candidate_power_product)) /\ exists ff_q_ftsv_norm_valuation_candidate_power_product_successor. ff_u_ftsv_norm_valuation_candidate_power_product = ff_q_ftsv_norm_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsv_norm_valuation_candidate_power_product)) * ff_v_ftsv_norm_valuation_candidate_power_product) + (ff_s_ftsv_norm_valuation_candidate_power_product))) /\ ff_s_ftsv_norm_valuation_candidate_power_product = ff_r_ftsv_norm_valuation_candidate_power_product * ff_p_ftsv_norm_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_norm_valuation_candidate_divides. (a * a + b * b) = bpv_result_ftsv_norm_valuation_candidate * bpv_factor_ftsv_norm_valuation_candidate_divides))) -> (exists bpv_gap_ftsv_norm_valuation_maximal. bpv_gap_ftsv_norm_valuation_maximal + bpv_candidate_ftsv_norm_valuation = e)) -> ~(e = 0) -> (exists ftsv_first_nonzero ftsv_second_nonzero. ((a = p * ftsv_first_nonzero) /\ ((b = p * ftsv_second_nonzero) /\ (((a * a + b * b = (p * p) * (ftsv_first_nonzero * ftsv_first_nonzero + ftsv_second_nonzero * ftsv_second_nonzero)) /\ ~((ftsv_first_nonzero * ftsv_first_nonzero + ftsv_second_nonzero * ftsv_second_nonzero) = 0))))))Constructive proof overview
Generated structural guide
A positive valuation of a nonzero represented norm at a three-modulo-four prime yields an exact nonzero represented prime-square quotient.
The unchanged tactic script uses 2 declared prerequisites and contains 24 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_nonzero_exponent_divides_base Alpha theorem; checked-use authorized TS003O three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotientDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–9
02Establish hdividesL10–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation nonzero exponent divides base.
- L10
have hdivides : exists ftcn_factor_ftsv_norm_divides. (a * a + b * b) = (p) * ftcn_factor_ftsv_norm_divides - L11
specialize power_valuation_nonzero_exponent_divides_base p - L12
specialize power_valuation_nonzero_exponent_divides_base (a * a + b * b) - L13
specialize power_valuation_nonzero_exponent_divides_base e - L14
apply power_valuation_nonzero_exponent_divides_base - L15
exact hvaluation - L16
exact hexponent - L17
specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient p - L18
specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient a - L19
specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient b
Original exact command ledger · 24 lines
- 0001
intro p - 0002
intro a - 0003
intro b - 0004
intro e - 0005
intro hprime - 0006
intro hthree - 0007
intro hnonzero - 0008
intro hvaluation - 0009
intro hexponent - 0010
have hdivides : exists ftcn_factor_ftsv_norm_divides. (a * a + b * b) = (p) * ftcn_factor_ftsv_norm_divides - 0011
specialize power_valuation_nonzero_exponent_divides_base p - 0012
specialize power_valuation_nonzero_exponent_divides_base (a * a + b * b) - 0013
specialize power_valuation_nonzero_exponent_divides_base e - 0014
apply power_valuation_nonzero_exponent_divides_base - 0015
exact hvaluation - 0016
exact hexponent - 0017
specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient p - 0018
specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient a - 0019
specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient b - 0020
apply three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient - 0021
exact hprime - 0022
exact hthree - 0023
exact hnonzero - 0024
exact hdivides