TS003V · theorem body

three_mod_four_prime_represented_nonzero_valuation_even

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

Necessity direction: every prime congruent to three modulo four has an explicitly even valuation in any represented nonzero natural.

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. ∀ n. ∀ e. Prime(p) → Mod4Three(p) → ¬n = 0 → (∃ x. ∃ y. n = x · x + y · y) → PowerValuation(p,n,e) → ∃ x. e = x + x

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

PD0046 PowerValuation
Exact expanded first-order statement
forall p n 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) -> ~(n = 0) -> (exists ftsc_first_ftsv_represented_source ftsc_second_ftsv_represented_source. (n) = ftsc_first_ftsv_represented_source * ftsc_first_ftsv_represented_source + ftsc_second_ftsv_represented_source * ftsc_second_ftsv_represented_source) -> (((exists bpv_gap_ftsv_represented_valuation_exponent_bound. bpv_gap_ftsv_represented_valuation_exponent_bound + e = n) /\ (exists bpv_result_ftsv_represented_valuation_selected. ((exists ff_b_ftsv_represented_valuation_selected_power ff_c_ftsv_represented_valuation_selected_power. ((forall ff_i_ftsv_represented_valuation_selected_power_repeat. (exists ff_lt_ftsv_represented_valuation_selected_power_repeat_bound. ff_lt_ftsv_represented_valuation_selected_power_repeat_bound + S ff_i_ftsv_represented_valuation_selected_power_repeat = e) -> (((exists ff_h_ftsv_represented_valuation_selected_power_repeat_decoded. ff_h_ftsv_represented_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_represented_valuation_selected_power_repeat)) * ff_c_ftsv_represented_valuation_selected_power)) /\ exists ff_q_ftsv_represented_valuation_selected_power_repeat_decoded. ff_b_ftsv_represented_valuation_selected_power = ff_q_ftsv_represented_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsv_represented_valuation_selected_power_repeat)) * ff_c_ftsv_represented_valuation_selected_power) + (p)))) /\ (exists ff_u_ftsv_represented_valuation_selected_power_product ff_v_ftsv_represented_valuation_selected_power_product. ((((exists ff_h_ftsv_represented_valuation_selected_power_product_start. ff_h_ftsv_represented_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_represented_valuation_selected_power_product)) /\ exists ff_q_ftsv_represented_valuation_selected_power_product_start. ff_u_ftsv_represented_valuation_selected_power_product = ff_q_ftsv_represented_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsv_represented_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_represented_valuation_selected_power_product_terminal. ff_h_ftsv_represented_valuation_selected_power_product_terminal + S (bpv_result_ftsv_represented_valuation_selected) = S ((S (e)) * ff_v_ftsv_represented_valuation_selected_power_product)) /\ exists ff_q_ftsv_represented_valuation_selected_power_product_terminal. ff_u_ftsv_represented_valuation_selected_power_product = ff_q_ftsv_represented_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_ftsv_represented_valuation_selected_power_product) + (bpv_result_ftsv_represented_valuation_selected))) /\ forall ff_i_ftsv_represented_valuation_selected_power_product. (exists ff_lt_ftsv_represented_valuation_selected_power_product_bound. ff_lt_ftsv_represented_valuation_selected_power_product_bound + S ff_i_ftsv_represented_valuation_selected_power_product = e) -> exists ff_p_ftsv_represented_valuation_selected_power_product ff_r_ftsv_represented_valuation_selected_power_product ff_s_ftsv_represented_valuation_selected_power_product. ((((exists ff_h_ftsv_represented_valuation_selected_power_product_factor. ff_h_ftsv_represented_valuation_selected_power_product_factor + S (ff_p_ftsv_represented_valuation_selected_power_product) = S ((S (ff_i_ftsv_represented_valuation_selected_power_product)) * ff_c_ftsv_represented_valuation_selected_power)) /\ exists ff_q_ftsv_represented_valuation_selected_power_product_factor. ff_b_ftsv_represented_valuation_selected_power = ff_q_ftsv_represented_valuation_selected_power_product_factor * S ((S (ff_i_ftsv_represented_valuation_selected_power_product)) * ff_c_ftsv_represented_valuation_selected_power) + (ff_p_ftsv_represented_valuation_selected_power_product))) /\ ((((exists ff_h_ftsv_represented_valuation_selected_power_product_partial. ff_h_ftsv_represented_valuation_selected_power_product_partial + S (ff_r_ftsv_represented_valuation_selected_power_product) = S ((S (ff_i_ftsv_represented_valuation_selected_power_product)) * ff_v_ftsv_represented_valuation_selected_power_product)) /\ exists ff_q_ftsv_represented_valuation_selected_power_product_partial. ff_u_ftsv_represented_valuation_selected_power_product = ff_q_ftsv_represented_valuation_selected_power_product_partial * S ((S (ff_i_ftsv_represented_valuation_selected_power_product)) * ff_v_ftsv_represented_valuation_selected_power_product) + (ff_r_ftsv_represented_valuation_selected_power_product))) /\ ((((exists ff_h_ftsv_represented_valuation_selected_power_product_successor. ff_h_ftsv_represented_valuation_selected_power_product_successor + S (ff_s_ftsv_represented_valuation_selected_power_product) = S ((S (S ff_i_ftsv_represented_valuation_selected_power_product)) * ff_v_ftsv_represented_valuation_selected_power_product)) /\ exists ff_q_ftsv_represented_valuation_selected_power_product_successor. ff_u_ftsv_represented_valuation_selected_power_product = ff_q_ftsv_represented_valuation_selected_power_product_successor * S ((S (S ff_i_ftsv_represented_valuation_selected_power_product)) * ff_v_ftsv_represented_valuation_selected_power_product) + (ff_s_ftsv_represented_valuation_selected_power_product))) /\ ff_s_ftsv_represented_valuation_selected_power_product = ff_r_ftsv_represented_valuation_selected_power_product * ff_p_ftsv_represented_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_represented_valuation_selected_divides. n = bpv_result_ftsv_represented_valuation_selected * bpv_factor_ftsv_represented_valuation_selected_divides)))) /\ forall bpv_candidate_ftsv_represented_valuation. (exists bpv_gap_ftsv_represented_valuation_candidate_bound. bpv_gap_ftsv_represented_valuation_candidate_bound + bpv_candidate_ftsv_represented_valuation = n) -> (exists bpv_result_ftsv_represented_valuation_candidate. ((exists ff_b_ftsv_represented_valuation_candidate_power ff_c_ftsv_represented_valuation_candidate_power. ((forall ff_i_ftsv_represented_valuation_candidate_power_repeat. (exists ff_lt_ftsv_represented_valuation_candidate_power_repeat_bound. ff_lt_ftsv_represented_valuation_candidate_power_repeat_bound + S ff_i_ftsv_represented_valuation_candidate_power_repeat = bpv_candidate_ftsv_represented_valuation) -> (((exists ff_h_ftsv_represented_valuation_candidate_power_repeat_decoded. ff_h_ftsv_represented_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_represented_valuation_candidate_power_repeat)) * ff_c_ftsv_represented_valuation_candidate_power)) /\ exists ff_q_ftsv_represented_valuation_candidate_power_repeat_decoded. ff_b_ftsv_represented_valuation_candidate_power = ff_q_ftsv_represented_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_represented_valuation_candidate_power_repeat)) * ff_c_ftsv_represented_valuation_candidate_power) + (p)))) /\ (exists ff_u_ftsv_represented_valuation_candidate_power_product ff_v_ftsv_represented_valuation_candidate_power_product. ((((exists ff_h_ftsv_represented_valuation_candidate_power_product_start. ff_h_ftsv_represented_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_represented_valuation_candidate_power_product)) /\ exists ff_q_ftsv_represented_valuation_candidate_power_product_start. ff_u_ftsv_represented_valuation_candidate_power_product = ff_q_ftsv_represented_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_represented_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_represented_valuation_candidate_power_product_terminal. ff_h_ftsv_represented_valuation_candidate_power_product_terminal + S (bpv_result_ftsv_represented_valuation_candidate) = S ((S (bpv_candidate_ftsv_represented_valuation)) * ff_v_ftsv_represented_valuation_candidate_power_product)) /\ exists ff_q_ftsv_represented_valuation_candidate_power_product_terminal. ff_u_ftsv_represented_valuation_candidate_power_product = ff_q_ftsv_represented_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_represented_valuation)) * ff_v_ftsv_represented_valuation_candidate_power_product) + (bpv_result_ftsv_represented_valuation_candidate))) /\ forall ff_i_ftsv_represented_valuation_candidate_power_product. (exists ff_lt_ftsv_represented_valuation_candidate_power_product_bound. ff_lt_ftsv_represented_valuation_candidate_power_product_bound + S ff_i_ftsv_represented_valuation_candidate_power_product = bpv_candidate_ftsv_represented_valuation) -> exists ff_p_ftsv_represented_valuation_candidate_power_product ff_r_ftsv_represented_valuation_candidate_power_product ff_s_ftsv_represented_valuation_candidate_power_product. ((((exists ff_h_ftsv_represented_valuation_candidate_power_product_factor. ff_h_ftsv_represented_valuation_candidate_power_product_factor + S (ff_p_ftsv_represented_valuation_candidate_power_product) = S ((S (ff_i_ftsv_represented_valuation_candidate_power_product)) * ff_c_ftsv_represented_valuation_candidate_power)) /\ exists ff_q_ftsv_represented_valuation_candidate_power_product_factor. ff_b_ftsv_represented_valuation_candidate_power = ff_q_ftsv_represented_valuation_candidate_power_product_factor * S ((S (ff_i_ftsv_represented_valuation_candidate_power_product)) * ff_c_ftsv_represented_valuation_candidate_power) + (ff_p_ftsv_represented_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsv_represented_valuation_candidate_power_product_partial. ff_h_ftsv_represented_valuation_candidate_power_product_partial + S (ff_r_ftsv_represented_valuation_candidate_power_product) = S ((S (ff_i_ftsv_represented_valuation_candidate_power_product)) * ff_v_ftsv_represented_valuation_candidate_power_product)) /\ exists ff_q_ftsv_represented_valuation_candidate_power_product_partial. ff_u_ftsv_represented_valuation_candidate_power_product = ff_q_ftsv_represented_valuation_candidate_power_product_partial * S ((S (ff_i_ftsv_represented_valuation_candidate_power_product)) * ff_v_ftsv_represented_valuation_candidate_power_product) + (ff_r_ftsv_represented_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsv_represented_valuation_candidate_power_product_successor. ff_h_ftsv_represented_valuation_candidate_power_product_successor + S (ff_s_ftsv_represented_valuation_candidate_power_product) = S ((S (S ff_i_ftsv_represented_valuation_candidate_power_product)) * ff_v_ftsv_represented_valuation_candidate_power_product)) /\ exists ff_q_ftsv_represented_valuation_candidate_power_product_successor. ff_u_ftsv_represented_valuation_candidate_power_product = ff_q_ftsv_represented_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsv_represented_valuation_candidate_power_product)) * ff_v_ftsv_represented_valuation_candidate_power_product) + (ff_s_ftsv_represented_valuation_candidate_power_product))) /\ ff_s_ftsv_represented_valuation_candidate_power_product = ff_r_ftsv_represented_valuation_candidate_power_product * ff_p_ftsv_represented_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_represented_valuation_candidate_divides. n = bpv_result_ftsv_represented_valuation_candidate * bpv_factor_ftsv_represented_valuation_candidate_divides))) -> (exists bpv_gap_ftsv_represented_valuation_maximal. bpv_gap_ftsv_represented_valuation_maximal + bpv_candidate_ftsv_represented_valuation = e)) -> exists h. e = h + h

Proof neighborhood

Direct theorem prerequisites

power_valuation_value_eq_transport · Alpha closed TS003U three_mod_four_prime_two_square_norm_valuation_even

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

33 script commands · 5 reading checkpoints · 2 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 two square norm valuation even
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro e
  4. L4
    intro hprime
  5. L5
    intro hthree
  6. L6
    intro hnonzero
  7. L7
    intro hrepresented
  8. L8
    intro hvaluation
02Separate the logical casesL9–10

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

  1. L9
    cases hrepresented
  2. L10
    cases hrepresented_witness
03Establish hnorm_nonzeroL11–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hnonzero.

  1. L11
    have hnorm_nonzero : ~(x * x + x1 * x1 = 0)
  2. L12
    intro hzero
  3. L13
    apply hnonzero
  4. L14
    trans x * x + x1 * x1
  5. L15
    exact hrepresented_witness_witness
  6. L16
    exact hzero
04Establish hnorm_valuationL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation value eq transport.

  1. L17
    have hnorm_valuation : PowerValuation(p,x · x + x1 · x1,e)Definitions: PowerValuation(p,x · x + x1 · x1,e)Original native command in the exact edition
  2. L18
    specialize power_valuation_value_eq_transport p
  3. L19
    specialize power_valuation_value_eq_transport n
  4. L20
    specialize power_valuation_value_eq_transport (x * x + x1 * x1)
  5. L21
    specialize power_valuation_value_eq_transport e
  6. L22
    apply power_valuation_value_eq_transport
  7. L23
    exact hrepresented_witness_witness
  8. L24
    exact hvaluation
  9. L25
    specialize three_mod_four_prime_two_square_norm_valuation_even p
  10. L26
    specialize three_mod_four_prime_two_square_norm_valuation_even x
05Use earlier factsL27–33

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

  1. L27
    specialize three_mod_four_prime_two_square_norm_valuation_even x1
  2. L28
    specialize three_mod_four_prime_two_square_norm_valuation_even e
  3. L29
    apply three_mod_four_prime_two_square_norm_valuation_even
  4. L30
    exact hprime
  5. L31
    exact hthree
  6. L32
    exact hnorm_nonzero
  7. L33
    exact hnorm_valuation

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro e
  4. 0004intro hprime
  5. 0005intro hthree
  6. 0006intro hnonzero
  7. 0007intro hrepresented
  8. 0008intro hvaluation
  9. 0009cases hrepresented
  10. 0010cases hrepresented_witness
  11. 0011have hnorm_nonzero : ~(x * x + x1 * x1 = 0)
  12. 0012intro hzero
  13. 0013apply hnonzero
  14. 0014trans x * x + x1 * x1
  15. 0015exact hrepresented_witness_witness
  16. 0016exact hzero
  17. 0017have hnorm_valuation : PowerValuation(p,x · x + x1 · x1,e)
    Exact native replay linehave hnorm_valuation : ((exists bpv_gap_ftsv_represented_norm_exponent_bound. bpv_gap_ftsv_represented_norm_exponent_bound + e = (x * x + x1 * x1)) /\ (exists bpv_result_ftsv_represented_norm_selected. ((exists ff_b_ftsv_represented_norm_selected_power ff_c_ftsv_represented_norm_selected_power. ((forall ff_i_ftsv_represented_norm_selected_power_repeat. (exists ff_lt_ftsv_represented_norm_selected_power_repeat_bound. ff_lt_ftsv_represented_norm_selected_power_repeat_bound + S ff_i_ftsv_represented_norm_selected_power_repeat = e) -> (((exists ff_h_ftsv_represented_norm_selected_power_repeat_decoded. ff_h_ftsv_represented_norm_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_represented_norm_selected_power_repeat)) * ff_c_ftsv_represented_norm_selected_power)) /\ exists ff_q_ftsv_represented_norm_selected_power_repeat_decoded. ff_b_ftsv_represented_norm_selected_power = ff_q_ftsv_represented_norm_selected_power_repeat_decoded * S ((S (ff_i_ftsv_represented_norm_selected_power_repeat)) * ff_c_ftsv_represented_norm_selected_power) + (p)))) /\ (exists ff_u_ftsv_represented_norm_selected_power_product ff_v_ftsv_represented_norm_selected_power_product. ((((exists ff_h_ftsv_represented_norm_selected_power_product_start. ff_h_ftsv_represented_norm_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_represented_norm_selected_power_product)) /\ exists ff_q_ftsv_represented_norm_selected_power_product_start. ff_u_ftsv_represented_norm_selected_power_product = ff_q_ftsv_represented_norm_selected_power_product_start * S ((S (0)) * ff_v_ftsv_represented_norm_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_represented_norm_selected_power_product_terminal. ff_h_ftsv_represented_norm_selected_power_product_terminal + S (bpv_result_ftsv_represented_norm_selected) = S ((S (e)) * ff_v_ftsv_represented_norm_selected_power_product)) /\ exists ff_q_ftsv_represented_norm_selected_power_product_terminal. ff_u_ftsv_represented_norm_selected_power_product = ff_q_ftsv_represented_norm_selected_power_product_terminal * S ((S (e)) * ff_v_ftsv_represented_norm_selected_power_product) + (bpv_result_ftsv_represented_norm_selected))) /\ forall ff_i_ftsv_represented_norm_selected_power_product. (exists ff_lt_ftsv_represented_norm_selected_power_product_bound. ff_lt_ftsv_represented_norm_selected_power_product_bound + S ff_i_ftsv_represented_norm_selected_power_product = e) -> exists ff_p_ftsv_represented_norm_selected_power_product ff_r_ftsv_represented_norm_selected_power_product ff_s_ftsv_represented_norm_selected_power_product. ((((exists ff_h_ftsv_represented_norm_selected_power_product_factor. ff_h_ftsv_represented_norm_selected_power_product_factor + S (ff_p_ftsv_represented_norm_selected_power_product) = S ((S (ff_i_ftsv_represented_norm_selected_power_product)) * ff_c_ftsv_represented_norm_selected_power)) /\ exists ff_q_ftsv_represented_norm_selected_power_product_factor. ff_b_ftsv_represented_norm_selected_power = ff_q_ftsv_represented_norm_selected_power_product_factor * S ((S (ff_i_ftsv_represented_norm_selected_power_product)) * ff_c_ftsv_represented_norm_selected_power) + (ff_p_ftsv_represented_norm_selected_power_product))) /\ ((((exists ff_h_ftsv_represented_norm_selected_power_product_partial. ff_h_ftsv_represented_norm_selected_power_product_partial + S (ff_r_ftsv_represented_norm_selected_power_product) = S ((S (ff_i_ftsv_represented_norm_selected_power_product)) * ff_v_ftsv_represented_norm_selected_power_product)) /\ exists ff_q_ftsv_represented_norm_selected_power_product_partial. ff_u_ftsv_represented_norm_selected_power_product = ff_q_ftsv_represented_norm_selected_power_product_partial * S ((S (ff_i_ftsv_represented_norm_selected_power_product)) * ff_v_ftsv_represented_norm_selected_power_product) + (ff_r_ftsv_represented_norm_selected_power_product))) /\ ((((exists ff_h_ftsv_represented_norm_selected_power_product_successor. ff_h_ftsv_represented_norm_selected_power_product_successor + S (ff_s_ftsv_represented_norm_selected_power_product) = S ((S (S ff_i_ftsv_represented_norm_selected_power_product)) * ff_v_ftsv_represented_norm_selected_power_product)) /\ exists ff_q_ftsv_represented_norm_selected_power_product_successor. ff_u_ftsv_represented_norm_selected_power_product = ff_q_ftsv_represented_norm_selected_power_product_successor * S ((S (S ff_i_ftsv_represented_norm_selected_power_product)) * ff_v_ftsv_represented_norm_selected_power_product) + (ff_s_ftsv_represented_norm_selected_power_product))) /\ ff_s_ftsv_represented_norm_selected_power_product = ff_r_ftsv_represented_norm_selected_power_product * ff_p_ftsv_represented_norm_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_represented_norm_selected_divides. (x * x + x1 * x1) = bpv_result_ftsv_represented_norm_selected * bpv_factor_ftsv_represented_norm_selected_divides)))) /\ forall bpv_candidate_ftsv_represented_norm. (exists bpv_gap_ftsv_represented_norm_candidate_bound. bpv_gap_ftsv_represented_norm_candidate_bound + bpv_candidate_ftsv_represented_norm = (x * x + x1 * x1)) -> (exists bpv_result_ftsv_represented_norm_candidate. ((exists ff_b_ftsv_represented_norm_candidate_power ff_c_ftsv_represented_norm_candidate_power. ((forall ff_i_ftsv_represented_norm_candidate_power_repeat. (exists ff_lt_ftsv_represented_norm_candidate_power_repeat_bound. ff_lt_ftsv_represented_norm_candidate_power_repeat_bound + S ff_i_ftsv_represented_norm_candidate_power_repeat = bpv_candidate_ftsv_represented_norm) -> (((exists ff_h_ftsv_represented_norm_candidate_power_repeat_decoded. ff_h_ftsv_represented_norm_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_represented_norm_candidate_power_repeat)) * ff_c_ftsv_represented_norm_candidate_power)) /\ exists ff_q_ftsv_represented_norm_candidate_power_repeat_decoded. ff_b_ftsv_represented_norm_candidate_power = ff_q_ftsv_represented_norm_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_represented_norm_candidate_power_repeat)) * ff_c_ftsv_represented_norm_candidate_power) + (p)))) /\ (exists ff_u_ftsv_represented_norm_candidate_power_product ff_v_ftsv_represented_norm_candidate_power_product. ((((exists ff_h_ftsv_represented_norm_candidate_power_product_start. ff_h_ftsv_represented_norm_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_represented_norm_candidate_power_product)) /\ exists ff_q_ftsv_represented_norm_candidate_power_product_start. ff_u_ftsv_represented_norm_candidate_power_product = ff_q_ftsv_represented_norm_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_represented_norm_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_represented_norm_candidate_power_product_terminal. ff_h_ftsv_represented_norm_candidate_power_product_terminal + S (bpv_result_ftsv_represented_norm_candidate) = S ((S (bpv_candidate_ftsv_represented_norm)) * ff_v_ftsv_represented_norm_candidate_power_product)) /\ exists ff_q_ftsv_represented_norm_candidate_power_product_terminal. ff_u_ftsv_represented_norm_candidate_power_product = ff_q_ftsv_represented_norm_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_represented_norm)) * ff_v_ftsv_represented_norm_candidate_power_product) + (bpv_result_ftsv_represented_norm_candidate))) /\ forall ff_i_ftsv_represented_norm_candidate_power_product. (exists ff_lt_ftsv_represented_norm_candidate_power_product_bound. ff_lt_ftsv_represented_norm_candidate_power_product_bound + S ff_i_ftsv_represented_norm_candidate_power_product = bpv_candidate_ftsv_represented_norm) -> exists ff_p_ftsv_represented_norm_candidate_power_product ff_r_ftsv_represented_norm_candidate_power_product ff_s_ftsv_represented_norm_candidate_power_product. ((((exists ff_h_ftsv_represented_norm_candidate_power_product_factor. ff_h_ftsv_represented_norm_candidate_power_product_factor + S (ff_p_ftsv_represented_norm_candidate_power_product) = S ((S (ff_i_ftsv_represented_norm_candidate_power_product)) * ff_c_ftsv_represented_norm_candidate_power)) /\ exists ff_q_ftsv_represented_norm_candidate_power_product_factor. ff_b_ftsv_represented_norm_candidate_power = ff_q_ftsv_represented_norm_candidate_power_product_factor * S ((S (ff_i_ftsv_represented_norm_candidate_power_product)) * ff_c_ftsv_represented_norm_candidate_power) + (ff_p_ftsv_represented_norm_candidate_power_product))) /\ ((((exists ff_h_ftsv_represented_norm_candidate_power_product_partial. ff_h_ftsv_represented_norm_candidate_power_product_partial + S (ff_r_ftsv_represented_norm_candidate_power_product) = S ((S (ff_i_ftsv_represented_norm_candidate_power_product)) * ff_v_ftsv_represented_norm_candidate_power_product)) /\ exists ff_q_ftsv_represented_norm_candidate_power_product_partial. ff_u_ftsv_represented_norm_candidate_power_product = ff_q_ftsv_represented_norm_candidate_power_product_partial * S ((S (ff_i_ftsv_represented_norm_candidate_power_product)) * ff_v_ftsv_represented_norm_candidate_power_product) + (ff_r_ftsv_represented_norm_candidate_power_product))) /\ ((((exists ff_h_ftsv_represented_norm_candidate_power_product_successor. ff_h_ftsv_represented_norm_candidate_power_product_successor + S (ff_s_ftsv_represented_norm_candidate_power_product) = S ((S (S ff_i_ftsv_represented_norm_candidate_power_product)) * ff_v_ftsv_represented_norm_candidate_power_product)) /\ exists ff_q_ftsv_represented_norm_candidate_power_product_successor. ff_u_ftsv_represented_norm_candidate_power_product = ff_q_ftsv_represented_norm_candidate_power_product_successor * S ((S (S ff_i_ftsv_represented_norm_candidate_power_product)) * ff_v_ftsv_represented_norm_candidate_power_product) + (ff_s_ftsv_represented_norm_candidate_power_product))) /\ ff_s_ftsv_represented_norm_candidate_power_product = ff_r_ftsv_represented_norm_candidate_power_product * ff_p_ftsv_represented_norm_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_represented_norm_candidate_divides. (x * x + x1 * x1) = bpv_result_ftsv_represented_norm_candidate * bpv_factor_ftsv_represented_norm_candidate_divides))) -> (exists bpv_gap_ftsv_represented_norm_maximal. bpv_gap_ftsv_represented_norm_maximal + bpv_candidate_ftsv_represented_norm = e)
  18. 0018specialize power_valuation_value_eq_transport p
  19. 0019specialize power_valuation_value_eq_transport n
  20. 0020specialize power_valuation_value_eq_transport (x * x + x1 * x1)
  21. 0021specialize power_valuation_value_eq_transport e
  22. 0022apply power_valuation_value_eq_transport
  23. 0023exact hrepresented_witness_witness
  24. 0024exact hvaluation
  25. 0025specialize three_mod_four_prime_two_square_norm_valuation_even p
  26. 0026specialize three_mod_four_prime_two_square_norm_valuation_even x
  27. 0027specialize three_mod_four_prime_two_square_norm_valuation_even x1
  28. 0028specialize three_mod_four_prime_two_square_norm_valuation_even e
  29. 0029apply three_mod_four_prime_two_square_norm_valuation_even
  30. 0030exact hprime
  31. 0031exact hthree
  32. 0032exact hnorm_nonzero
  33. 0033exact hnorm_valuation