TS003D · theorem body

positive_number_with_even_bad_prime_valuations_is_two_square

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Every nonzero natural whose three-modulo-four prime valuations are all even has an explicitly witnessed two-square representation.

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. 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) -> (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

le_refl · Stable closed TS003C all_bad_prime_even_two_square_sufficiency_bounded

Direct theorem dependents

TS003E nonzero_two_square_iff_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

10 script commands · 2 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 (1)
all bad prime even two square sufficiency bounded
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro hnonzero
  3. L3
    intro hparity
02Use earlier factsL4–10

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

  1. L4
    specialize all_bad_prime_even_two_square_sufficiency_bounded n
  2. L5
    specialize all_bad_prime_even_two_square_sufficiency_bounded n
  3. L6
    apply all_bad_prime_even_two_square_sufficiency_bounded
  4. L7
    specialize le_refl n
  5. L8
    exact le_refl
  6. L9
    exact hnonzero
  7. L10
    exact hparity

Library-wide reading audit

Original defined command ledger · 10 lines
  1. 0001intro n
  2. 0002intro hnonzero
  3. 0003intro hparity
  4. 0004specialize all_bad_prime_even_two_square_sufficiency_bounded n
  5. 0005specialize all_bad_prime_even_two_square_sufficiency_bounded n
  6. 0006apply all_bad_prime_even_two_square_sufficiency_bounded
  7. 0007specialize le_refl n
  8. 0008exact le_refl
  9. 0009exact hnonzero
  10. 0010exact hparity