TS003V

three_mod_four_prime_represented_nonzero_valuation_even

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 33 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_value_eq_transport Alpha theorem; checked-use authorized TS003U three_mod_four_prime_two_square_norm_valuation_even

Direct dependents

TS003E nonzero_two_square_iff_even_three_mod_four_prime_valuations

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

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.

Named ingredients (1)
three mod four prime two square norm valuation even

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 : BoundedPowerValuation(p,x · x + x1 · x1,x · x + x1 · x1,e)Definitions: BoundedPowerValuation
  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 exact 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 : ((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