TS003R · theorem body

three_mod_four_prime_nonzero_norm_positive_valuation_extracts

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

A positive valuation of a nonzero represented norm at a three-modulo-four prime yields an exact nonzero represented prime-square quotient.

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

∀ p. ∀ a. ∀ b. ∀ e. Prime(p) → Mod4Three(p) → ¬a · a + b · b = 0 → PowerValuation(p,a · a + b · b,e) → ¬e = 0 → ∃ x. ∃ y. a = p · x ∧ (b = p · y ∧ (a · a + b · b = p · p · (x · x + y · y) ∧ ¬x · x + y · y = 0))

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

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

Proof neighborhood

Direct theorem prerequisites

power_valuation_nonzero_exponent_divides_base · Alpha closed TS003O three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient

Direct theorem dependents

TS003T three_mod_four_prime_two_square_norm_valuation_even_bounded

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

24 script commands · 3 reading checkpoints · 1 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)
three mod four prime nonzero two square norm extracts nonzero quotient
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro e
  5. L5
    intro hprime
  6. L6
    intro hthree
  7. L7
    intro hnonzero
  8. L8
    intro hvaluation
  9. L9
    intro hexponent
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.

  1. L10
    have hdivides : Dvd(p,a · a + b · b)Definitions: Dvd(p,a · a + b · b)Original native command in the exact edition
  2. L11
    specialize power_valuation_nonzero_exponent_divides_base p
  3. L12
    specialize power_valuation_nonzero_exponent_divides_base (a * a + b * b)
  4. L13
    specialize power_valuation_nonzero_exponent_divides_base e
  5. L14
    apply power_valuation_nonzero_exponent_divides_base
  6. L15
    exact hvaluation
  7. L16
    exact hexponent
  8. L17
    specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient p
  9. L18
    specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient a
  10. L19
    specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient b
03Use earlier factsL20–24

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

  1. L20
    apply three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient
  2. L21
    exact hprime
  3. L22
    exact hthree
  4. L23
    exact hnonzero
  5. L24
    exact hdivides

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro e
  5. 0005intro hprime
  6. 0006intro hthree
  7. 0007intro hnonzero
  8. 0008intro hvaluation
  9. 0009intro hexponent
  10. 0010have hdivides : Dvd(p,a · a + b · b)
    Exact native replay linehave hdivides : exists ftcn_factor_ftsv_norm_divides. (a * a + b * b) = (p) * ftcn_factor_ftsv_norm_divides
  11. 0011specialize power_valuation_nonzero_exponent_divides_base p
  12. 0012specialize power_valuation_nonzero_exponent_divides_base (a * a + b * b)
  13. 0013specialize power_valuation_nonzero_exponent_divides_base e
  14. 0014apply power_valuation_nonzero_exponent_divides_base
  15. 0015exact hvaluation
  16. 0016exact hexponent
  17. 0017specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient p
  18. 0018specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient a
  19. 0019specialize three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient b
  20. 0020apply three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotient
  21. 0021exact hprime
  22. 0022exact hthree
  23. 0023exact hnonzero
  24. 0024exact hdivides