TS003T · theorem body

three_mod_four_prime_two_square_norm_valuation_even_bounded

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

Bounded natural induction proves that a three-modulo-four prime has even valuation in every nonzero represented norm below the bound.

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

∀ B. ∀ p. ∀ a. ∀ b. ∀ e. Le(a · a + b · b,B) → Prime(p) → Mod4Three(p) → ¬a · a + b · b = 0 → PowerValuation(p,a · a + b · b,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

PD0001 Le PD0004 Prime PD0012 Mod4Three PD0046 PowerValuation

In local proof propositions

PD0001 Le PD0002 Lt PD0046 PowerValuation
Exact expanded first-order statement
forall B p a b e. (exists ftsv_bound_gap. ftsv_bound_gap + (a * a + b * b) = B) -> ((~(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)) -> exists h. e = h + h

Proof neighborhood

Direct theorem prerequisites

le_zero · Stable closed eq_decidable · Stable closed TS003R three_mod_four_prime_nonzero_norm_positive_valuation_extracts TS003S prime_square_times_nonzero_strictly_increases le_trans · Stable closed le_of_succ_le_succ · Stable closed power_valuation_exists · Alpha closed prime_nonzero · Stable closed power_valuation_value_eq_transport · Alpha closed TS003Q prime_power_valuation_square_factor_preserves_evenness

Direct theorem dependents

TS003U three_mod_four_prime_two_square_norm_valuation_even

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

115 script commands · 26 reading checkpoints · 10 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 (3)
three mod four prime nonzero norm positive valuation extractsprime square times nonzero strictly increasesprime power valuation square factor preserves evenness
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro p
  3. L4
    intro a
  4. L5
    intro b
  5. L6
    intro e
  6. L7
    intro hbound
  7. L8
    intro hprime
  8. L9
    intro hthree
  9. L10
    intro hnonzero
  10. L11
    intro hvaluation
03Separate the logical casesL12–12

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

  1. L12
    exfalso
04Use earlier factsL13–16

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

  1. L13
    apply hnonzero
  2. L14
    specialize le_zero (a * a + b * b)
  3. L15
    apply le_zero
  4. L16
    exact hbound
05Fix variables and assumptionsL17–25

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

  1. L17
    intro p
  2. L18
    intro a
  3. L19
    intro b
  4. L20
    intro e
  5. L21
    intro hbound
  6. L22
    intro hprime
  7. L23
    intro hthree
  8. L24
    intro hnonzero
  9. L25
    intro hvaluation
06Establish hcasesL26–29

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hcases : e = 0 \/ ~(e = 0)
  2. L27
    specialize eq_decidable e
  3. L28
    specialize eq_decidable 0
  4. L29
    exact eq_decidable
07Separate the logical casesL30–30

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

  1. L30
    cases hcases
08Construct an explicit witnessL31–31

Supply the displayed value, then prove that it has the required property.

  1. L31
    exists 0
09Calculate and transport equalitiesL32–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite hcases_left
  2. L33
    simp
10Establish hextractionL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply three mod four prime nonzero norm positive valuation extracts.

  1. L34
    have hextraction : 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)))))
  2. L35
    specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts p
  3. L36
    specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts a
  4. L37
    specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts b
  5. L38
    specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts e
  6. L39
    apply three_mod_four_prime_nonzero_norm_positive_valuation_extracts
  7. L40
    exact hprime
  8. L41
    exact hthree
  9. L42
    exact hnonzero
  10. L43
    exact hvaluation
11Use earlier factsL44–44

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

  1. L44
    exact hcases_right
12Separate the logical casesL45–49

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

  1. L45
    cases hextraction
  2. L46
    cases hextraction_witness
  3. L47
    cases hextraction_witness_witness
  4. L48
    cases hextraction_witness_witness_right
  5. L49
    cases hextraction_witness_witness_right_right
13Establish hstrictL50–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime square times nonzero strictly increases.

  1. L50
    have hstrict : Lt(x · x + x1 · x1,p · p · (x · x + x1 · x1))Definitions: Lt(x · x + x1 · x1,p · p · (x · x + x1 · x1))Original native command in the exact edition
  2. L51
    specialize prime_square_times_nonzero_strictly_increases p
  3. L52
    specialize prime_square_times_nonzero_strictly_increases (x * x + x1 * x1)
  4. L53
    apply prime_square_times_nonzero_strictly_increases
  5. L54
    exact hprime
  6. L55
    exact hextraction_witness_witness_right_right_right
  7. L56
    rewrite <- hextraction_witness_witness_right_right_left at hstrict
14Establish hsuccessor_boundL57–63

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

  1. L57
    have hsuccessor_bound : Lt(x · x + x1 · x1,S B)Definitions: Lt(x · x + x1 · x1,S B)Original native command in the exact edition
  2. L58
    specialize le_trans (S (x * x + x1 * x1))
  3. L59
    specialize le_trans (a * a + b * b)
  4. L60
    specialize le_trans (S B)
  5. L61
    apply le_trans
  6. L62
    exact hstrict
  7. L63
    exact hbound
15Establish hquotient_boundL64–68

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

  1. L64
    have hquotient_bound : Le(x · x + x1 · x1,B)Definitions: Le(x · x + x1 · x1,B)Original native command in the exact edition
  2. L65
    specialize le_of_succ_le_succ (x * x + x1 * x1)
  3. L66
    specialize le_of_succ_le_succ B
  4. L67
    apply le_of_succ_le_succ
  5. L68
    exact hsuccessor_bound
16Establish hquotient_valuationL69–70

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

  1. L69
    have hquotient_valuation : ∃ f. PowerValuation(p,x · x + x1 · x1,f)Definitions: PowerValuation(p,x · x + x1 · x1,f)Original native command in the exact edition
  2. L70
    apply power_valuation_exists
17Separate the logical casesL71–71

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

  1. L71
    cases hquotient_valuation
18Establish hquotient_evenL72–81

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

  1. L72
    have hquotient_even : exists h. x2 = h + h
  2. L73
    specialize IH p
  3. L74
    specialize IH x
  4. L75
    specialize IH x1
  5. L76
    specialize IH x2
  6. L77
    apply IH
  7. L78
    exact hquotient_bound
  8. L79
    exact hprime
  9. L80
    exact hthree
  10. L81
    exact hextraction_witness_witness_right_right_right
19Use earlier factsL82–82

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

  1. L82
    exact hquotient_valuation_witness
20Separate the logical casesL83–83

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

  1. L83
    cases hquotient_even
21Establish hprime_valuationL84–85

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

  1. L84
    have hprime_valuation : ∃ r. PowerValuation(p,p,r)Definitions: PowerValuation(p,p,r)Original native command in the exact edition
  2. L85
    apply power_valuation_exists
22Separate the logical casesL86–86

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

  1. L86
    cases hprime_valuation
23Establish hpnonzeroL87–92

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

  1. L87
    have hpnonzero : ~(p = 0)
  2. L88
    specialize prime_nonzero p
  3. L89
    intro hpzero
  4. L90
    apply prime_nonzero
  5. L91
    exact hprime
  6. L92
    exact hpzero
24Establish hproduct_valuationL93–102

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

  1. L93
    have hproduct_valuation : PowerValuation(p,p · p · (x · x + x1 · x1),e)Definitions: PowerValuation(p,p · p · (x · x + x1 · x1),e)Original native command in the exact edition
  2. L94
    specialize power_valuation_value_eq_transport p
  3. L95
    specialize power_valuation_value_eq_transport (a * a + b * b)
  4. L96
    specialize power_valuation_value_eq_transport ((p * p) * (x * x + x1 * x1))
  5. L97
    specialize power_valuation_value_eq_transport e
  6. L98
    apply power_valuation_value_eq_transport
  7. L99
    exact hextraction_witness_witness_right_right_left
  8. L100
    exact hvaluation
  9. L101
    specialize prime_power_valuation_square_factor_preserves_evenness p
  10. L102
    specialize prime_power_valuation_square_factor_preserves_evenness p
25Use earlier factsL103–112

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

  1. L103
    specialize prime_power_valuation_square_factor_preserves_evenness (x * x + x1 * x1)
  2. L104
    specialize prime_power_valuation_square_factor_preserves_evenness x4
  3. L105
    specialize prime_power_valuation_square_factor_preserves_evenness x2
  4. L106
    specialize prime_power_valuation_square_factor_preserves_evenness e
  5. L107
    specialize prime_power_valuation_square_factor_preserves_evenness x3
  6. L108
    apply prime_power_valuation_square_factor_preserves_evenness
  7. L109
    exact hprime
  8. L110
    exact hpnonzero
  9. L111
    exact hextraction_witness_witness_right_right_right
  10. L112
    exact hprime_valuation_witness
26Use earlier factsL113–115

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

  1. L113
    exact hquotient_valuation_witness
  2. L114
    exact hproduct_valuation
  3. L115
    exact hquotient_even_witness

Library-wide reading audit

Original defined command ledger · 115 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro p
  4. 0004intro a
  5. 0005intro b
  6. 0006intro e
  7. 0007intro hbound
  8. 0008intro hprime
  9. 0009intro hthree
  10. 0010intro hnonzero
  11. 0011intro hvaluation
  12. 0012exfalso
  13. 0013apply hnonzero
  14. 0014specialize le_zero (a * a + b * b)
  15. 0015apply le_zero
  16. 0016exact hbound
  17. 0017intro p
  18. 0018intro a
  19. 0019intro b
  20. 0020intro e
  21. 0021intro hbound
  22. 0022intro hprime
  23. 0023intro hthree
  24. 0024intro hnonzero
  25. 0025intro hvaluation
  26. 0026have hcases : e = 0 \/ ~(e = 0)
  27. 0027specialize eq_decidable e
  28. 0028specialize eq_decidable 0
  29. 0029exact eq_decidable
  30. 0030cases hcases
  31. 0031exists 0
  32. 0032rewrite hcases_left
  33. 0033simp
  34. 0034have hextraction : 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)))))
  35. 0035specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts p
  36. 0036specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts a
  37. 0037specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts b
  38. 0038specialize three_mod_four_prime_nonzero_norm_positive_valuation_extracts e
  39. 0039apply three_mod_four_prime_nonzero_norm_positive_valuation_extracts
  40. 0040exact hprime
  41. 0041exact hthree
  42. 0042exact hnonzero
  43. 0043exact hvaluation
  44. 0044exact hcases_right
  45. 0045cases hextraction
  46. 0046cases hextraction_witness
  47. 0047cases hextraction_witness_witness
  48. 0048cases hextraction_witness_witness_right
  49. 0049cases hextraction_witness_witness_right_right
  50. 0050have hstrict : Lt(x · x + x1 · x1,p · p · (x · x + x1 · x1))
    Exact native replay linehave hstrict : exists k. k + S (x * x + x1 * x1) = (p * p) * (x * x + x1 * x1)
  51. 0051specialize prime_square_times_nonzero_strictly_increases p
  52. 0052specialize prime_square_times_nonzero_strictly_increases (x * x + x1 * x1)
  53. 0053apply prime_square_times_nonzero_strictly_increases
  54. 0054exact hprime
  55. 0055exact hextraction_witness_witness_right_right_right
  56. 0056rewrite <- hextraction_witness_witness_right_right_left at hstrict
  57. 0057have hsuccessor_bound : Lt(x · x + x1 · x1,S B)
    Exact native replay linehave hsuccessor_bound : exists k. k + S (x * x + x1 * x1) = S B
  58. 0058specialize le_trans (S (x * x + x1 * x1))
  59. 0059specialize le_trans (a * a + b * b)
  60. 0060specialize le_trans (S B)
  61. 0061apply le_trans
  62. 0062exact hstrict
  63. 0063exact hbound
  64. 0064have hquotient_bound : Le(x · x + x1 · x1,B)
    Exact native replay linehave hquotient_bound : exists k. k + (x * x + x1 * x1) = B
  65. 0065specialize le_of_succ_le_succ (x * x + x1 * x1)
  66. 0066specialize le_of_succ_le_succ B
  67. 0067apply le_of_succ_le_succ
  68. 0068exact hsuccessor_bound
  69. 0069have hquotient_valuation : ∃ f. PowerValuation(p,x · x + x1 · x1,f)
    Exact native replay linehave hquotient_valuation : exists f. (((exists bpv_gap_ftsv_induction_quotient_exponent_bound. bpv_gap_ftsv_induction_quotient_exponent_bound + f = (x * x + x1 * x1)) /\ (exists bpv_result_ftsv_induction_quotient_selected. ((exists ff_b_ftsv_induction_quotient_selected_power ff_c_ftsv_induction_quotient_selected_power. ((forall ff_i_ftsv_induction_quotient_selected_power_repeat. (exists ff_lt_ftsv_induction_quotient_selected_power_repeat_bound. ff_lt_ftsv_induction_quotient_selected_power_repeat_bound + S ff_i_ftsv_induction_quotient_selected_power_repeat = f) -> (((exists ff_h_ftsv_induction_quotient_selected_power_repeat_decoded. ff_h_ftsv_induction_quotient_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_induction_quotient_selected_power_repeat)) * ff_c_ftsv_induction_quotient_selected_power)) /\ exists ff_q_ftsv_induction_quotient_selected_power_repeat_decoded. ff_b_ftsv_induction_quotient_selected_power = ff_q_ftsv_induction_quotient_selected_power_repeat_decoded * S ((S (ff_i_ftsv_induction_quotient_selected_power_repeat)) * ff_c_ftsv_induction_quotient_selected_power) + (p)))) /\ (exists ff_u_ftsv_induction_quotient_selected_power_product ff_v_ftsv_induction_quotient_selected_power_product. ((((exists ff_h_ftsv_induction_quotient_selected_power_product_start. ff_h_ftsv_induction_quotient_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_induction_quotient_selected_power_product)) /\ exists ff_q_ftsv_induction_quotient_selected_power_product_start. ff_u_ftsv_induction_quotient_selected_power_product = ff_q_ftsv_induction_quotient_selected_power_product_start * S ((S (0)) * ff_v_ftsv_induction_quotient_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_induction_quotient_selected_power_product_terminal. ff_h_ftsv_induction_quotient_selected_power_product_terminal + S (bpv_result_ftsv_induction_quotient_selected) = S ((S (f)) * ff_v_ftsv_induction_quotient_selected_power_product)) /\ exists ff_q_ftsv_induction_quotient_selected_power_product_terminal. ff_u_ftsv_induction_quotient_selected_power_product = ff_q_ftsv_induction_quotient_selected_power_product_terminal * S ((S (f)) * ff_v_ftsv_induction_quotient_selected_power_product) + (bpv_result_ftsv_induction_quotient_selected))) /\ forall ff_i_ftsv_induction_quotient_selected_power_product. (exists ff_lt_ftsv_induction_quotient_selected_power_product_bound. ff_lt_ftsv_induction_quotient_selected_power_product_bound + S ff_i_ftsv_induction_quotient_selected_power_product = f) -> exists ff_p_ftsv_induction_quotient_selected_power_product ff_r_ftsv_induction_quotient_selected_power_product ff_s_ftsv_induction_quotient_selected_power_product. ((((exists ff_h_ftsv_induction_quotient_selected_power_product_factor. ff_h_ftsv_induction_quotient_selected_power_product_factor + S (ff_p_ftsv_induction_quotient_selected_power_product) = S ((S (ff_i_ftsv_induction_quotient_selected_power_product)) * ff_c_ftsv_induction_quotient_selected_power)) /\ exists ff_q_ftsv_induction_quotient_selected_power_product_factor. ff_b_ftsv_induction_quotient_selected_power = ff_q_ftsv_induction_quotient_selected_power_product_factor * S ((S (ff_i_ftsv_induction_quotient_selected_power_product)) * ff_c_ftsv_induction_quotient_selected_power) + (ff_p_ftsv_induction_quotient_selected_power_product))) /\ ((((exists ff_h_ftsv_induction_quotient_selected_power_product_partial. ff_h_ftsv_induction_quotient_selected_power_product_partial + S (ff_r_ftsv_induction_quotient_selected_power_product) = S ((S (ff_i_ftsv_induction_quotient_selected_power_product)) * ff_v_ftsv_induction_quotient_selected_power_product)) /\ exists ff_q_ftsv_induction_quotient_selected_power_product_partial. ff_u_ftsv_induction_quotient_selected_power_product = ff_q_ftsv_induction_quotient_selected_power_product_partial * S ((S (ff_i_ftsv_induction_quotient_selected_power_product)) * ff_v_ftsv_induction_quotient_selected_power_product) + (ff_r_ftsv_induction_quotient_selected_power_product))) /\ ((((exists ff_h_ftsv_induction_quotient_selected_power_product_successor. ff_h_ftsv_induction_quotient_selected_power_product_successor + S (ff_s_ftsv_induction_quotient_selected_power_product) = S ((S (S ff_i_ftsv_induction_quotient_selected_power_product)) * ff_v_ftsv_induction_quotient_selected_power_product)) /\ exists ff_q_ftsv_induction_quotient_selected_power_product_successor. ff_u_ftsv_induction_quotient_selected_power_product = ff_q_ftsv_induction_quotient_selected_power_product_successor * S ((S (S ff_i_ftsv_induction_quotient_selected_power_product)) * ff_v_ftsv_induction_quotient_selected_power_product) + (ff_s_ftsv_induction_quotient_selected_power_product))) /\ ff_s_ftsv_induction_quotient_selected_power_product = ff_r_ftsv_induction_quotient_selected_power_product * ff_p_ftsv_induction_quotient_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_induction_quotient_selected_divides. (x * x + x1 * x1) = bpv_result_ftsv_induction_quotient_selected * bpv_factor_ftsv_induction_quotient_selected_divides)))) /\ forall bpv_candidate_ftsv_induction_quotient. (exists bpv_gap_ftsv_induction_quotient_candidate_bound. bpv_gap_ftsv_induction_quotient_candidate_bound + bpv_candidate_ftsv_induction_quotient = (x * x + x1 * x1)) -> (exists bpv_result_ftsv_induction_quotient_candidate. ((exists ff_b_ftsv_induction_quotient_candidate_power ff_c_ftsv_induction_quotient_candidate_power. ((forall ff_i_ftsv_induction_quotient_candidate_power_repeat. (exists ff_lt_ftsv_induction_quotient_candidate_power_repeat_bound. ff_lt_ftsv_induction_quotient_candidate_power_repeat_bound + S ff_i_ftsv_induction_quotient_candidate_power_repeat = bpv_candidate_ftsv_induction_quotient) -> (((exists ff_h_ftsv_induction_quotient_candidate_power_repeat_decoded. ff_h_ftsv_induction_quotient_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_induction_quotient_candidate_power_repeat)) * ff_c_ftsv_induction_quotient_candidate_power)) /\ exists ff_q_ftsv_induction_quotient_candidate_power_repeat_decoded. ff_b_ftsv_induction_quotient_candidate_power = ff_q_ftsv_induction_quotient_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_induction_quotient_candidate_power_repeat)) * ff_c_ftsv_induction_quotient_candidate_power) + (p)))) /\ (exists ff_u_ftsv_induction_quotient_candidate_power_product ff_v_ftsv_induction_quotient_candidate_power_product. ((((exists ff_h_ftsv_induction_quotient_candidate_power_product_start. ff_h_ftsv_induction_quotient_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_induction_quotient_candidate_power_product)) /\ exists ff_q_ftsv_induction_quotient_candidate_power_product_start. ff_u_ftsv_induction_quotient_candidate_power_product = ff_q_ftsv_induction_quotient_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_induction_quotient_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_induction_quotient_candidate_power_product_terminal. ff_h_ftsv_induction_quotient_candidate_power_product_terminal + S (bpv_result_ftsv_induction_quotient_candidate) = S ((S (bpv_candidate_ftsv_induction_quotient)) * ff_v_ftsv_induction_quotient_candidate_power_product)) /\ exists ff_q_ftsv_induction_quotient_candidate_power_product_terminal. ff_u_ftsv_induction_quotient_candidate_power_product = ff_q_ftsv_induction_quotient_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_induction_quotient)) * ff_v_ftsv_induction_quotient_candidate_power_product) + (bpv_result_ftsv_induction_quotient_candidate))) /\ forall ff_i_ftsv_induction_quotient_candidate_power_product. (exists ff_lt_ftsv_induction_quotient_candidate_power_product_bound. ff_lt_ftsv_induction_quotient_candidate_power_product_bound + S ff_i_ftsv_induction_quotient_candidate_power_product = bpv_candidate_ftsv_induction_quotient) -> exists ff_p_ftsv_induction_quotient_candidate_power_product ff_r_ftsv_induction_quotient_candidate_power_product ff_s_ftsv_induction_quotient_candidate_power_product. ((((exists ff_h_ftsv_induction_quotient_candidate_power_product_factor. ff_h_ftsv_induction_quotient_candidate_power_product_factor + S (ff_p_ftsv_induction_quotient_candidate_power_product) = S ((S (ff_i_ftsv_induction_quotient_candidate_power_product)) * ff_c_ftsv_induction_quotient_candidate_power)) /\ exists ff_q_ftsv_induction_quotient_candidate_power_product_factor. ff_b_ftsv_induction_quotient_candidate_power = ff_q_ftsv_induction_quotient_candidate_power_product_factor * S ((S (ff_i_ftsv_induction_quotient_candidate_power_product)) * ff_c_ftsv_induction_quotient_candidate_power) + (ff_p_ftsv_induction_quotient_candidate_power_product))) /\ ((((exists ff_h_ftsv_induction_quotient_candidate_power_product_partial. ff_h_ftsv_induction_quotient_candidate_power_product_partial + S (ff_r_ftsv_induction_quotient_candidate_power_product) = S ((S (ff_i_ftsv_induction_quotient_candidate_power_product)) * ff_v_ftsv_induction_quotient_candidate_power_product)) /\ exists ff_q_ftsv_induction_quotient_candidate_power_product_partial. ff_u_ftsv_induction_quotient_candidate_power_product = ff_q_ftsv_induction_quotient_candidate_power_product_partial * S ((S (ff_i_ftsv_induction_quotient_candidate_power_product)) * ff_v_ftsv_induction_quotient_candidate_power_product) + (ff_r_ftsv_induction_quotient_candidate_power_product))) /\ ((((exists ff_h_ftsv_induction_quotient_candidate_power_product_successor. ff_h_ftsv_induction_quotient_candidate_power_product_successor + S (ff_s_ftsv_induction_quotient_candidate_power_product) = S ((S (S ff_i_ftsv_induction_quotient_candidate_power_product)) * ff_v_ftsv_induction_quotient_candidate_power_product)) /\ exists ff_q_ftsv_induction_quotient_candidate_power_product_successor. ff_u_ftsv_induction_quotient_candidate_power_product = ff_q_ftsv_induction_quotient_candidate_power_product_successor * S ((S (S ff_i_ftsv_induction_quotient_candidate_power_product)) * ff_v_ftsv_induction_quotient_candidate_power_product) + (ff_s_ftsv_induction_quotient_candidate_power_product))) /\ ff_s_ftsv_induction_quotient_candidate_power_product = ff_r_ftsv_induction_quotient_candidate_power_product * ff_p_ftsv_induction_quotient_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_induction_quotient_candidate_divides. (x * x + x1 * x1) = bpv_result_ftsv_induction_quotient_candidate * bpv_factor_ftsv_induction_quotient_candidate_divides))) -> (exists bpv_gap_ftsv_induction_quotient_maximal. bpv_gap_ftsv_induction_quotient_maximal + bpv_candidate_ftsv_induction_quotient = f))
  70. 0070apply power_valuation_exists
  71. 0071cases hquotient_valuation
  72. 0072have hquotient_even : exists h. x2 = h + h
  73. 0073specialize IH p
  74. 0074specialize IH x
  75. 0075specialize IH x1
  76. 0076specialize IH x2
  77. 0077apply IH
  78. 0078exact hquotient_bound
  79. 0079exact hprime
  80. 0080exact hthree
  81. 0081exact hextraction_witness_witness_right_right_right
  82. 0082exact hquotient_valuation_witness
  83. 0083cases hquotient_even
  84. 0084have hprime_valuation : ∃ r. PowerValuation(p,p,r)
    Exact native replay linehave hprime_valuation : exists r. (((exists bpv_gap_ftsv_induction_prime_exponent_bound. bpv_gap_ftsv_induction_prime_exponent_bound + r = p) /\ (exists bpv_result_ftsv_induction_prime_selected. ((exists ff_b_ftsv_induction_prime_selected_power ff_c_ftsv_induction_prime_selected_power. ((forall ff_i_ftsv_induction_prime_selected_power_repeat. (exists ff_lt_ftsv_induction_prime_selected_power_repeat_bound. ff_lt_ftsv_induction_prime_selected_power_repeat_bound + S ff_i_ftsv_induction_prime_selected_power_repeat = r) -> (((exists ff_h_ftsv_induction_prime_selected_power_repeat_decoded. ff_h_ftsv_induction_prime_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_induction_prime_selected_power_repeat)) * ff_c_ftsv_induction_prime_selected_power)) /\ exists ff_q_ftsv_induction_prime_selected_power_repeat_decoded. ff_b_ftsv_induction_prime_selected_power = ff_q_ftsv_induction_prime_selected_power_repeat_decoded * S ((S (ff_i_ftsv_induction_prime_selected_power_repeat)) * ff_c_ftsv_induction_prime_selected_power) + (p)))) /\ (exists ff_u_ftsv_induction_prime_selected_power_product ff_v_ftsv_induction_prime_selected_power_product. ((((exists ff_h_ftsv_induction_prime_selected_power_product_start. ff_h_ftsv_induction_prime_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_induction_prime_selected_power_product)) /\ exists ff_q_ftsv_induction_prime_selected_power_product_start. ff_u_ftsv_induction_prime_selected_power_product = ff_q_ftsv_induction_prime_selected_power_product_start * S ((S (0)) * ff_v_ftsv_induction_prime_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_induction_prime_selected_power_product_terminal. ff_h_ftsv_induction_prime_selected_power_product_terminal + S (bpv_result_ftsv_induction_prime_selected) = S ((S (r)) * ff_v_ftsv_induction_prime_selected_power_product)) /\ exists ff_q_ftsv_induction_prime_selected_power_product_terminal. ff_u_ftsv_induction_prime_selected_power_product = ff_q_ftsv_induction_prime_selected_power_product_terminal * S ((S (r)) * ff_v_ftsv_induction_prime_selected_power_product) + (bpv_result_ftsv_induction_prime_selected))) /\ forall ff_i_ftsv_induction_prime_selected_power_product. (exists ff_lt_ftsv_induction_prime_selected_power_product_bound. ff_lt_ftsv_induction_prime_selected_power_product_bound + S ff_i_ftsv_induction_prime_selected_power_product = r) -> exists ff_p_ftsv_induction_prime_selected_power_product ff_r_ftsv_induction_prime_selected_power_product ff_s_ftsv_induction_prime_selected_power_product. ((((exists ff_h_ftsv_induction_prime_selected_power_product_factor. ff_h_ftsv_induction_prime_selected_power_product_factor + S (ff_p_ftsv_induction_prime_selected_power_product) = S ((S (ff_i_ftsv_induction_prime_selected_power_product)) * ff_c_ftsv_induction_prime_selected_power)) /\ exists ff_q_ftsv_induction_prime_selected_power_product_factor. ff_b_ftsv_induction_prime_selected_power = ff_q_ftsv_induction_prime_selected_power_product_factor * S ((S (ff_i_ftsv_induction_prime_selected_power_product)) * ff_c_ftsv_induction_prime_selected_power) + (ff_p_ftsv_induction_prime_selected_power_product))) /\ ((((exists ff_h_ftsv_induction_prime_selected_power_product_partial. ff_h_ftsv_induction_prime_selected_power_product_partial + S (ff_r_ftsv_induction_prime_selected_power_product) = S ((S (ff_i_ftsv_induction_prime_selected_power_product)) * ff_v_ftsv_induction_prime_selected_power_product)) /\ exists ff_q_ftsv_induction_prime_selected_power_product_partial. ff_u_ftsv_induction_prime_selected_power_product = ff_q_ftsv_induction_prime_selected_power_product_partial * S ((S (ff_i_ftsv_induction_prime_selected_power_product)) * ff_v_ftsv_induction_prime_selected_power_product) + (ff_r_ftsv_induction_prime_selected_power_product))) /\ ((((exists ff_h_ftsv_induction_prime_selected_power_product_successor. ff_h_ftsv_induction_prime_selected_power_product_successor + S (ff_s_ftsv_induction_prime_selected_power_product) = S ((S (S ff_i_ftsv_induction_prime_selected_power_product)) * ff_v_ftsv_induction_prime_selected_power_product)) /\ exists ff_q_ftsv_induction_prime_selected_power_product_successor. ff_u_ftsv_induction_prime_selected_power_product = ff_q_ftsv_induction_prime_selected_power_product_successor * S ((S (S ff_i_ftsv_induction_prime_selected_power_product)) * ff_v_ftsv_induction_prime_selected_power_product) + (ff_s_ftsv_induction_prime_selected_power_product))) /\ ff_s_ftsv_induction_prime_selected_power_product = ff_r_ftsv_induction_prime_selected_power_product * ff_p_ftsv_induction_prime_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_induction_prime_selected_divides. p = bpv_result_ftsv_induction_prime_selected * bpv_factor_ftsv_induction_prime_selected_divides)))) /\ forall bpv_candidate_ftsv_induction_prime. (exists bpv_gap_ftsv_induction_prime_candidate_bound. bpv_gap_ftsv_induction_prime_candidate_bound + bpv_candidate_ftsv_induction_prime = p) -> (exists bpv_result_ftsv_induction_prime_candidate. ((exists ff_b_ftsv_induction_prime_candidate_power ff_c_ftsv_induction_prime_candidate_power. ((forall ff_i_ftsv_induction_prime_candidate_power_repeat. (exists ff_lt_ftsv_induction_prime_candidate_power_repeat_bound. ff_lt_ftsv_induction_prime_candidate_power_repeat_bound + S ff_i_ftsv_induction_prime_candidate_power_repeat = bpv_candidate_ftsv_induction_prime) -> (((exists ff_h_ftsv_induction_prime_candidate_power_repeat_decoded. ff_h_ftsv_induction_prime_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_induction_prime_candidate_power_repeat)) * ff_c_ftsv_induction_prime_candidate_power)) /\ exists ff_q_ftsv_induction_prime_candidate_power_repeat_decoded. ff_b_ftsv_induction_prime_candidate_power = ff_q_ftsv_induction_prime_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_induction_prime_candidate_power_repeat)) * ff_c_ftsv_induction_prime_candidate_power) + (p)))) /\ (exists ff_u_ftsv_induction_prime_candidate_power_product ff_v_ftsv_induction_prime_candidate_power_product. ((((exists ff_h_ftsv_induction_prime_candidate_power_product_start. ff_h_ftsv_induction_prime_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_induction_prime_candidate_power_product)) /\ exists ff_q_ftsv_induction_prime_candidate_power_product_start. ff_u_ftsv_induction_prime_candidate_power_product = ff_q_ftsv_induction_prime_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_induction_prime_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_induction_prime_candidate_power_product_terminal. ff_h_ftsv_induction_prime_candidate_power_product_terminal + S (bpv_result_ftsv_induction_prime_candidate) = S ((S (bpv_candidate_ftsv_induction_prime)) * ff_v_ftsv_induction_prime_candidate_power_product)) /\ exists ff_q_ftsv_induction_prime_candidate_power_product_terminal. ff_u_ftsv_induction_prime_candidate_power_product = ff_q_ftsv_induction_prime_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_induction_prime)) * ff_v_ftsv_induction_prime_candidate_power_product) + (bpv_result_ftsv_induction_prime_candidate))) /\ forall ff_i_ftsv_induction_prime_candidate_power_product. (exists ff_lt_ftsv_induction_prime_candidate_power_product_bound. ff_lt_ftsv_induction_prime_candidate_power_product_bound + S ff_i_ftsv_induction_prime_candidate_power_product = bpv_candidate_ftsv_induction_prime) -> exists ff_p_ftsv_induction_prime_candidate_power_product ff_r_ftsv_induction_prime_candidate_power_product ff_s_ftsv_induction_prime_candidate_power_product. ((((exists ff_h_ftsv_induction_prime_candidate_power_product_factor. ff_h_ftsv_induction_prime_candidate_power_product_factor + S (ff_p_ftsv_induction_prime_candidate_power_product) = S ((S (ff_i_ftsv_induction_prime_candidate_power_product)) * ff_c_ftsv_induction_prime_candidate_power)) /\ exists ff_q_ftsv_induction_prime_candidate_power_product_factor. ff_b_ftsv_induction_prime_candidate_power = ff_q_ftsv_induction_prime_candidate_power_product_factor * S ((S (ff_i_ftsv_induction_prime_candidate_power_product)) * ff_c_ftsv_induction_prime_candidate_power) + (ff_p_ftsv_induction_prime_candidate_power_product))) /\ ((((exists ff_h_ftsv_induction_prime_candidate_power_product_partial. ff_h_ftsv_induction_prime_candidate_power_product_partial + S (ff_r_ftsv_induction_prime_candidate_power_product) = S ((S (ff_i_ftsv_induction_prime_candidate_power_product)) * ff_v_ftsv_induction_prime_candidate_power_product)) /\ exists ff_q_ftsv_induction_prime_candidate_power_product_partial. ff_u_ftsv_induction_prime_candidate_power_product = ff_q_ftsv_induction_prime_candidate_power_product_partial * S ((S (ff_i_ftsv_induction_prime_candidate_power_product)) * ff_v_ftsv_induction_prime_candidate_power_product) + (ff_r_ftsv_induction_prime_candidate_power_product))) /\ ((((exists ff_h_ftsv_induction_prime_candidate_power_product_successor. ff_h_ftsv_induction_prime_candidate_power_product_successor + S (ff_s_ftsv_induction_prime_candidate_power_product) = S ((S (S ff_i_ftsv_induction_prime_candidate_power_product)) * ff_v_ftsv_induction_prime_candidate_power_product)) /\ exists ff_q_ftsv_induction_prime_candidate_power_product_successor. ff_u_ftsv_induction_prime_candidate_power_product = ff_q_ftsv_induction_prime_candidate_power_product_successor * S ((S (S ff_i_ftsv_induction_prime_candidate_power_product)) * ff_v_ftsv_induction_prime_candidate_power_product) + (ff_s_ftsv_induction_prime_candidate_power_product))) /\ ff_s_ftsv_induction_prime_candidate_power_product = ff_r_ftsv_induction_prime_candidate_power_product * ff_p_ftsv_induction_prime_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_induction_prime_candidate_divides. p = bpv_result_ftsv_induction_prime_candidate * bpv_factor_ftsv_induction_prime_candidate_divides))) -> (exists bpv_gap_ftsv_induction_prime_maximal. bpv_gap_ftsv_induction_prime_maximal + bpv_candidate_ftsv_induction_prime = r))
  85. 0085apply power_valuation_exists
  86. 0086cases hprime_valuation
  87. 0087have hpnonzero : ~(p = 0)
  88. 0088specialize prime_nonzero p
  89. 0089intro hpzero
  90. 0090apply prime_nonzero
  91. 0091exact hprime
  92. 0092exact hpzero
  93. 0093have hproduct_valuation : PowerValuation(p,p · p · (x · x + x1 · x1),e)
    Exact native replay linehave hproduct_valuation : ((exists bpv_gap_ftsv_induction_product_exponent_bound. bpv_gap_ftsv_induction_product_exponent_bound + e = ((p * p) * (x * x + x1 * x1))) /\ (exists bpv_result_ftsv_induction_product_selected. ((exists ff_b_ftsv_induction_product_selected_power ff_c_ftsv_induction_product_selected_power. ((forall ff_i_ftsv_induction_product_selected_power_repeat. (exists ff_lt_ftsv_induction_product_selected_power_repeat_bound. ff_lt_ftsv_induction_product_selected_power_repeat_bound + S ff_i_ftsv_induction_product_selected_power_repeat = e) -> (((exists ff_h_ftsv_induction_product_selected_power_repeat_decoded. ff_h_ftsv_induction_product_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_induction_product_selected_power_repeat)) * ff_c_ftsv_induction_product_selected_power)) /\ exists ff_q_ftsv_induction_product_selected_power_repeat_decoded. ff_b_ftsv_induction_product_selected_power = ff_q_ftsv_induction_product_selected_power_repeat_decoded * S ((S (ff_i_ftsv_induction_product_selected_power_repeat)) * ff_c_ftsv_induction_product_selected_power) + (p)))) /\ (exists ff_u_ftsv_induction_product_selected_power_product ff_v_ftsv_induction_product_selected_power_product. ((((exists ff_h_ftsv_induction_product_selected_power_product_start. ff_h_ftsv_induction_product_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_induction_product_selected_power_product)) /\ exists ff_q_ftsv_induction_product_selected_power_product_start. ff_u_ftsv_induction_product_selected_power_product = ff_q_ftsv_induction_product_selected_power_product_start * S ((S (0)) * ff_v_ftsv_induction_product_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_induction_product_selected_power_product_terminal. ff_h_ftsv_induction_product_selected_power_product_terminal + S (bpv_result_ftsv_induction_product_selected) = S ((S (e)) * ff_v_ftsv_induction_product_selected_power_product)) /\ exists ff_q_ftsv_induction_product_selected_power_product_terminal. ff_u_ftsv_induction_product_selected_power_product = ff_q_ftsv_induction_product_selected_power_product_terminal * S ((S (e)) * ff_v_ftsv_induction_product_selected_power_product) + (bpv_result_ftsv_induction_product_selected))) /\ forall ff_i_ftsv_induction_product_selected_power_product. (exists ff_lt_ftsv_induction_product_selected_power_product_bound. ff_lt_ftsv_induction_product_selected_power_product_bound + S ff_i_ftsv_induction_product_selected_power_product = e) -> exists ff_p_ftsv_induction_product_selected_power_product ff_r_ftsv_induction_product_selected_power_product ff_s_ftsv_induction_product_selected_power_product. ((((exists ff_h_ftsv_induction_product_selected_power_product_factor. ff_h_ftsv_induction_product_selected_power_product_factor + S (ff_p_ftsv_induction_product_selected_power_product) = S ((S (ff_i_ftsv_induction_product_selected_power_product)) * ff_c_ftsv_induction_product_selected_power)) /\ exists ff_q_ftsv_induction_product_selected_power_product_factor. ff_b_ftsv_induction_product_selected_power = ff_q_ftsv_induction_product_selected_power_product_factor * S ((S (ff_i_ftsv_induction_product_selected_power_product)) * ff_c_ftsv_induction_product_selected_power) + (ff_p_ftsv_induction_product_selected_power_product))) /\ ((((exists ff_h_ftsv_induction_product_selected_power_product_partial. ff_h_ftsv_induction_product_selected_power_product_partial + S (ff_r_ftsv_induction_product_selected_power_product) = S ((S (ff_i_ftsv_induction_product_selected_power_product)) * ff_v_ftsv_induction_product_selected_power_product)) /\ exists ff_q_ftsv_induction_product_selected_power_product_partial. ff_u_ftsv_induction_product_selected_power_product = ff_q_ftsv_induction_product_selected_power_product_partial * S ((S (ff_i_ftsv_induction_product_selected_power_product)) * ff_v_ftsv_induction_product_selected_power_product) + (ff_r_ftsv_induction_product_selected_power_product))) /\ ((((exists ff_h_ftsv_induction_product_selected_power_product_successor. ff_h_ftsv_induction_product_selected_power_product_successor + S (ff_s_ftsv_induction_product_selected_power_product) = S ((S (S ff_i_ftsv_induction_product_selected_power_product)) * ff_v_ftsv_induction_product_selected_power_product)) /\ exists ff_q_ftsv_induction_product_selected_power_product_successor. ff_u_ftsv_induction_product_selected_power_product = ff_q_ftsv_induction_product_selected_power_product_successor * S ((S (S ff_i_ftsv_induction_product_selected_power_product)) * ff_v_ftsv_induction_product_selected_power_product) + (ff_s_ftsv_induction_product_selected_power_product))) /\ ff_s_ftsv_induction_product_selected_power_product = ff_r_ftsv_induction_product_selected_power_product * ff_p_ftsv_induction_product_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_induction_product_selected_divides. ((p * p) * (x * x + x1 * x1)) = bpv_result_ftsv_induction_product_selected * bpv_factor_ftsv_induction_product_selected_divides)))) /\ forall bpv_candidate_ftsv_induction_product. (exists bpv_gap_ftsv_induction_product_candidate_bound. bpv_gap_ftsv_induction_product_candidate_bound + bpv_candidate_ftsv_induction_product = ((p * p) * (x * x + x1 * x1))) -> (exists bpv_result_ftsv_induction_product_candidate. ((exists ff_b_ftsv_induction_product_candidate_power ff_c_ftsv_induction_product_candidate_power. ((forall ff_i_ftsv_induction_product_candidate_power_repeat. (exists ff_lt_ftsv_induction_product_candidate_power_repeat_bound. ff_lt_ftsv_induction_product_candidate_power_repeat_bound + S ff_i_ftsv_induction_product_candidate_power_repeat = bpv_candidate_ftsv_induction_product) -> (((exists ff_h_ftsv_induction_product_candidate_power_repeat_decoded. ff_h_ftsv_induction_product_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_induction_product_candidate_power_repeat)) * ff_c_ftsv_induction_product_candidate_power)) /\ exists ff_q_ftsv_induction_product_candidate_power_repeat_decoded. ff_b_ftsv_induction_product_candidate_power = ff_q_ftsv_induction_product_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_induction_product_candidate_power_repeat)) * ff_c_ftsv_induction_product_candidate_power) + (p)))) /\ (exists ff_u_ftsv_induction_product_candidate_power_product ff_v_ftsv_induction_product_candidate_power_product. ((((exists ff_h_ftsv_induction_product_candidate_power_product_start. ff_h_ftsv_induction_product_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_induction_product_candidate_power_product)) /\ exists ff_q_ftsv_induction_product_candidate_power_product_start. ff_u_ftsv_induction_product_candidate_power_product = ff_q_ftsv_induction_product_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_induction_product_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_induction_product_candidate_power_product_terminal. ff_h_ftsv_induction_product_candidate_power_product_terminal + S (bpv_result_ftsv_induction_product_candidate) = S ((S (bpv_candidate_ftsv_induction_product)) * ff_v_ftsv_induction_product_candidate_power_product)) /\ exists ff_q_ftsv_induction_product_candidate_power_product_terminal. ff_u_ftsv_induction_product_candidate_power_product = ff_q_ftsv_induction_product_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_induction_product)) * ff_v_ftsv_induction_product_candidate_power_product) + (bpv_result_ftsv_induction_product_candidate))) /\ forall ff_i_ftsv_induction_product_candidate_power_product. (exists ff_lt_ftsv_induction_product_candidate_power_product_bound. ff_lt_ftsv_induction_product_candidate_power_product_bound + S ff_i_ftsv_induction_product_candidate_power_product = bpv_candidate_ftsv_induction_product) -> exists ff_p_ftsv_induction_product_candidate_power_product ff_r_ftsv_induction_product_candidate_power_product ff_s_ftsv_induction_product_candidate_power_product. ((((exists ff_h_ftsv_induction_product_candidate_power_product_factor. ff_h_ftsv_induction_product_candidate_power_product_factor + S (ff_p_ftsv_induction_product_candidate_power_product) = S ((S (ff_i_ftsv_induction_product_candidate_power_product)) * ff_c_ftsv_induction_product_candidate_power)) /\ exists ff_q_ftsv_induction_product_candidate_power_product_factor. ff_b_ftsv_induction_product_candidate_power = ff_q_ftsv_induction_product_candidate_power_product_factor * S ((S (ff_i_ftsv_induction_product_candidate_power_product)) * ff_c_ftsv_induction_product_candidate_power) + (ff_p_ftsv_induction_product_candidate_power_product))) /\ ((((exists ff_h_ftsv_induction_product_candidate_power_product_partial. ff_h_ftsv_induction_product_candidate_power_product_partial + S (ff_r_ftsv_induction_product_candidate_power_product) = S ((S (ff_i_ftsv_induction_product_candidate_power_product)) * ff_v_ftsv_induction_product_candidate_power_product)) /\ exists ff_q_ftsv_induction_product_candidate_power_product_partial. ff_u_ftsv_induction_product_candidate_power_product = ff_q_ftsv_induction_product_candidate_power_product_partial * S ((S (ff_i_ftsv_induction_product_candidate_power_product)) * ff_v_ftsv_induction_product_candidate_power_product) + (ff_r_ftsv_induction_product_candidate_power_product))) /\ ((((exists ff_h_ftsv_induction_product_candidate_power_product_successor. ff_h_ftsv_induction_product_candidate_power_product_successor + S (ff_s_ftsv_induction_product_candidate_power_product) = S ((S (S ff_i_ftsv_induction_product_candidate_power_product)) * ff_v_ftsv_induction_product_candidate_power_product)) /\ exists ff_q_ftsv_induction_product_candidate_power_product_successor. ff_u_ftsv_induction_product_candidate_power_product = ff_q_ftsv_induction_product_candidate_power_product_successor * S ((S (S ff_i_ftsv_induction_product_candidate_power_product)) * ff_v_ftsv_induction_product_candidate_power_product) + (ff_s_ftsv_induction_product_candidate_power_product))) /\ ff_s_ftsv_induction_product_candidate_power_product = ff_r_ftsv_induction_product_candidate_power_product * ff_p_ftsv_induction_product_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_induction_product_candidate_divides. ((p * p) * (x * x + x1 * x1)) = bpv_result_ftsv_induction_product_candidate * bpv_factor_ftsv_induction_product_candidate_divides))) -> (exists bpv_gap_ftsv_induction_product_maximal. bpv_gap_ftsv_induction_product_maximal + bpv_candidate_ftsv_induction_product = e)
  94. 0094specialize power_valuation_value_eq_transport p
  95. 0095specialize power_valuation_value_eq_transport (a * a + b * b)
  96. 0096specialize power_valuation_value_eq_transport ((p * p) * (x * x + x1 * x1))
  97. 0097specialize power_valuation_value_eq_transport e
  98. 0098apply power_valuation_value_eq_transport
  99. 0099exact hextraction_witness_witness_right_right_left
  100. 0100exact hvaluation
  101. 0101specialize prime_power_valuation_square_factor_preserves_evenness p
  102. 0102specialize prime_power_valuation_square_factor_preserves_evenness p
  103. 0103specialize prime_power_valuation_square_factor_preserves_evenness (x * x + x1 * x1)
  104. 0104specialize prime_power_valuation_square_factor_preserves_evenness x4
  105. 0105specialize prime_power_valuation_square_factor_preserves_evenness x2
  106. 0106specialize prime_power_valuation_square_factor_preserves_evenness e
  107. 0107specialize prime_power_valuation_square_factor_preserves_evenness x3
  108. 0108apply prime_power_valuation_square_factor_preserves_evenness
  109. 0109exact hprime
  110. 0110exact hpnonzero
  111. 0111exact hextraction_witness_witness_right_right_right
  112. 0112exact hprime_valuation_witness
  113. 0113exact hquotient_valuation_witness
  114. 0114exact hproduct_valuation
  115. 0115exact hquotient_even_witness