SL0007

bounded_gauss_lemma_complete

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A canonical Gauss reflection count is even exactly for residues and odd exactly for nonresidues.

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 h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall esi_prime_left_glb_prime esi_prime_right_glb_prime. p = esi_prime_left_glb_prime * esi_prime_right_glb_prime -> esi_prime_left_glb_prime = 1 \/ esi_prime_right_glb_prime = 1)) -> (exists wpo_gap_glb_a_positive. wpo_gap_glb_a_positive + S (0) = a) -> (exists wpo_gap_glb_a_lt_p. wpo_gap_glb_a_lt_p + S (a) = p) -> (forall gsp_range_index_glb_half_range. (exists gsp_lt_gap_glb_half_range_range_bound. gsp_lt_gap_glb_half_range_range_bound + S gsp_range_index_glb_half_range = h) -> (((exists gsp_beta_height_glb_half_range_range_entry. gsp_beta_height_glb_half_range_range_entry + S (1 + gsp_range_index_glb_half_range) = S ((S (gsp_range_index_glb_half_range)) * c)) /\ exists gsp_beta_quotient_glb_half_range_range_entry. b = gsp_beta_quotient_glb_half_range_range_entry * S ((S (gsp_range_index_glb_half_range)) * c) + (1 + gsp_range_index_glb_half_range)))) -> (exists e. ((exists mb mc sb sc. ((forall gsp_index_glb_signed_prefix. (exists gsp_lt_gap_glb_signed_prefix_index_bound. gsp_lt_gap_glb_signed_prefix_index_bound + S gsp_index_glb_signed_prefix = h) -> (exists gsp_value_glb_signed_prefix_entry gsp_magnitude_glb_signed_prefix_entry gsp_sign_glb_signed_prefix_entry. (((exists ff_h_gsp_glb_signed_prefix_entry_source. ff_h_gsp_glb_signed_prefix_entry_source + S (gsp_value_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * c)) /\ exists ff_q_gsp_glb_signed_prefix_entry_source. b = ff_q_gsp_glb_signed_prefix_entry_source * S ((S (gsp_index_glb_signed_prefix)) * c) + (gsp_value_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_magnitude. ff_h_gsp_glb_signed_prefix_entry_magnitude + S (gsp_magnitude_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * mc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_magnitude. mb = ff_q_gsp_glb_signed_prefix_entry_magnitude * S ((S (gsp_index_glb_signed_prefix)) * mc) + (gsp_magnitude_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_sign. ff_h_gsp_glb_signed_prefix_entry_sign + S (gsp_sign_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * sc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_sign. sb = ff_q_gsp_glb_signed_prefix_entry_sign * S ((S (gsp_index_glb_signed_prefix)) * sc) + (gsp_sign_glb_signed_prefix_entry))) /\ ((exists gsp_lt_gap_glb_signed_prefix_entry_positive. gsp_lt_gap_glb_signed_prefix_entry_positive + S 0 = gsp_magnitude_glb_signed_prefix_entry) /\ ((exists gsp_le_gap_glb_signed_prefix_entry_bounded. gsp_le_gap_glb_signed_prefix_entry_bounded + gsp_magnitude_glb_signed_prefix_entry = h) /\ ((gsp_sign_glb_signed_prefix_entry = 0 \/ gsp_sign_glb_signed_prefix_entry = 1) /\ (((gsp_sign_glb_signed_prefix_entry = 0 /\ (exists gsp_mod_left_glb_signed_prefix_entry_lower gsp_mod_right_glb_signed_prefix_entry_lower. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_lower = (gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_lower)) \/ (gsp_sign_glb_signed_prefix_entry = 1 /\ (exists gsp_mod_left_glb_signed_prefix_entry_reflected gsp_mod_right_glb_signed_prefix_entry_reflected. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_reflected))))))))))) /\ (((exists ff_u_glb_count_sum ff_v_glb_count_sum. ((((exists ff_h_glb_count_sum_start. ff_h_glb_count_sum_start + S (0) = S ((S (0)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_start. ff_u_glb_count_sum = ff_q_glb_count_sum_start * S ((S (0)) * ff_v_glb_count_sum) + (0))) /\ ((((exists ff_h_glb_count_sum_terminal. ff_h_glb_count_sum_terminal + S (e) = S ((S (h)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_terminal. ff_u_glb_count_sum = ff_q_glb_count_sum_terminal * S ((S (h)) * ff_v_glb_count_sum) + (e))) /\ forall ff_i_glb_count_sum. (exists ff_lt_glb_count_sum_bound. ff_lt_glb_count_sum_bound + S ff_i_glb_count_sum = h) -> exists ff_a_glb_count_sum ff_r_glb_count_sum ff_s_glb_count_sum. ((((exists ff_h_glb_count_sum_summand. ff_h_glb_count_sum_summand + S (ff_a_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * sc)) /\ exists ff_q_glb_count_sum_summand. sb = ff_q_glb_count_sum_summand * S ((S (ff_i_glb_count_sum)) * sc) + (ff_a_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_partial. ff_h_glb_count_sum_partial + S (ff_r_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_partial. ff_u_glb_count_sum = ff_q_glb_count_sum_partial * S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_r_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_successor. ff_h_glb_count_sum_successor + S (ff_s_glb_count_sum) = S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_successor. ff_u_glb_count_sum = ff_q_glb_count_sum_successor * S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_s_glb_count_sum))) /\ ff_s_glb_count_sum = ff_r_glb_count_sum + ff_a_glb_count_sum)))))) /\ (forall ff_i_glb_count_bits. (exists ff_lt_glb_count_bits_bound. ff_lt_glb_count_bits_bound + S ff_i_glb_count_bits = h) -> exists ff_bit_glb_count_bits. ((((exists ff_h_glb_count_bits_decoded. ff_h_glb_count_bits_decoded + S (ff_bit_glb_count_bits) = S ((S (ff_i_glb_count_bits)) * sc)) /\ exists ff_q_glb_count_bits_decoded. sb = ff_q_glb_count_bits_decoded * S ((S (ff_i_glb_count_bits)) * sc) + (ff_bit_glb_count_bits))) /\ (ff_bit_glb_count_bits = 0 \/ ff_bit_glb_count_bits = 1))))))) /\ (((((exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_even_glb_even. e = 2 * gs_even_glb_even)) /\ ((exists gs_even_glb_even. e = 2 * gs_even_glb_even) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)))) /\ (((~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_odd_glb_odd. e = 2 * gs_odd_glb_odd + 1)) /\ ((exists gs_odd_glb_odd. e = 2 * gs_odd_glb_odd + 1) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)))))))

Constructive proof overview

Generated structural guide

A canonical Gauss reflection count is even exactly for residues and odd exactly for nonresidues.

The unchanged tactic script uses 11 declared prerequisites and contains 204 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

lt_irrefl_expanded Stable theorem; checked-use authorized bounded_nonzero_not_divides Alpha theorem; checked-use authorized gauss_lemma_power_congruence_exists Alpha theorem; checked-use authorized pow_predecessor_parity_mod Stable theorem; checked-use authorized SL0000 bounded_euler_criterion_complete parity_cases Stable theorem; checked-use authorized odd_prime_one_not_mod_predecessor Alpha theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

SL000Q quadratic_supplement_two_half_complete

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

204 script commands · 54 reading checkpoints · 24 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)
bounded euler criterion complete

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–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro hpodd
  7. L7
    intro hprime
  8. L8
    intro hpositive
  9. L9
    intro halt
  10. L10
    intro hhalf
02Establish hpsuccL11–14

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

  1. L11
    have hpsucc : p = S (2 * h)
  2. L12
    trans 2 * h + 1
  3. L13
    exact hpodd
  4. L14
    simp
03Establish hdoubleL15–20

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

  1. L15
    have hdouble : h + h = 2 * h
  2. L16
    trans h * 2
  3. L17
    simp [zero_add]
  4. L18
    specialize mul_comm h
  5. L19
    specialize mul_comm 2
  6. L20
    apply mul_comm
04Establish ha0L21–26

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

  1. L21
    have ha0 : ~(a = 0)
  2. L22
    intro haeq
  3. L23
    specialize lt_irrefl_expanded 0
  4. L24
    apply lt_irrefl_expanded
  5. L25
    rewrite haeq at hpositive
  6. L26
    exact hpositive
05Establish hnotdivL27–34

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

  1. L27
    have hnotdiv : ~(exists frm_factor_glb_nondivisor. a = p * frm_factor_glb_nondivisor)
  2. L28
    intro hdiv
  3. L29
    specialize bounded_nonzero_not_divides p
  4. L30
    specialize bounded_nonzero_not_divides a
  5. L31
    apply bounded_nonzero_not_divides
  6. L32
    exact ha0
  7. L33
    exact halt
  8. L34
    exact hdiv
06Establish hgaussL35–44

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

  1. L35
    have hgauss : ∃ e. ∃ A. ∃ R. Pow(a,h,A) ∧ (Pow(2 · h,e,R) ∧ ((∃ x. ∃ y. ∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ k. ∃ i. ∃ j. BetaAt(b,c,m,k) ∧ (BetaAt(x,y,m,i) ∧ (BetaAt(z,n,m,j) ∧ (Lt(0,i) ∧ (Le(i,h) ∧ ((j = 0 ∨ j = 1) ∧ (j = 0 ∧ ModEq(p,a · k,i) ∨ j = 1 ∧ ModEq(p,a · k,2 · h · i)))))))) ∧ BitCount(z,n,h,e)) ∧ ModEq(p,A,R)))Definitions: LeLtModEqBetaAtBitCountPow
  2. L36
    specialize gauss_lemma_power_congruence_exists p
  3. L37
    specialize gauss_lemma_power_congruence_exists h
  4. L38
    specialize gauss_lemma_power_congruence_exists a
  5. L39
    specialize gauss_lemma_power_congruence_exists b
  6. L40
    specialize gauss_lemma_power_congruence_exists c
  7. L41
    apply gauss_lemma_power_congruence_exists
  8. L42
    exact hpodd
  9. L43
    exact hprime
  10. L44
    exact hnotdiv
07Use earlier factsL45–45

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

  1. L45
    exact hhalf
08Separate the logical casesL46–51

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

  1. L46
    cases hgauss
  2. L47
    cases hgauss_witness
  3. L48
    cases hgauss_witness_witness
  4. L49
    cases hgauss_witness_witness_witness
  5. L50
    cases hgauss_witness_witness_witness_right
  6. L51
    cases hgauss_witness_witness_witness_right_right
09Establish heulerL52–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded euler criterion complete.

  1. L52
    have heuler : (QRes(p,a) → ModEq(p,x1,1)) ∧ (ModEq(p,x1,1) → QRes(p,a)) ∧ ((¬QRes(p,a) → ModEq(p,x1,2 · h)) ∧ (ModEq(p,x1,2 · h) → ¬QRes(p,a)))Definitions: ModEqQRes
  2. L53
    specialize bounded_euler_criterion_complete p
  3. L54
    specialize bounded_euler_criterion_complete a
  4. L55
    specialize bounded_euler_criterion_complete (2 * h)
  5. L56
    specialize bounded_euler_criterion_complete h
  6. L57
    specialize bounded_euler_criterion_complete x1
  7. L58
    apply bounded_euler_criterion_complete
  8. L59
    exact hpsucc
  9. L60
    exact hprime
  10. L61
    exact ha0
10Use earlier factsL62–62

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

  1. L62
    exact halt
11Calculate and transport equalitiesL63–63

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

  1. L63
    symm
12Use earlier factsL64–65

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

  1. L64
    exact hdouble
  2. L65
    exact hgauss_witness_witness_witness_left
13Separate the logical casesL66–68

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

  1. L66
    cases heuler
  2. L67
    cases heuler_left
  3. L68
    cases heuler_right
14Establish hbridgeL69–76

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow predecessor parity mod.

  1. L69
    have hbridge : (((exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one)) /\ ((exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> (exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor)))
  2. L70
    specialize pow_predecessor_parity_mod p
  3. L71
    specialize pow_predecessor_parity_mod (2 * h)
  4. L72
    specialize pow_predecessor_parity_mod x
  5. L73
    specialize pow_predecessor_parity_mod x2
  6. L74
    apply pow_predecessor_parity_mod
  7. L75
    exact hpsucc
  8. L76
    exact hgauss_witness_witness_witness_right_left
15Separate the logical casesL77–77

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

  1. L77
    cases hbridge
16Establish hseparationL78–87

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

  1. L78
    have hseparation : ~(exists wpp_mod_left_glb_one_mod_predecessor wpp_mod_right_glb_one_mod_predecessor. (1) + p * wpp_mod_left_glb_one_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_one_mod_predecessor)
  2. L79
    intro hcollision
  3. L80
    specialize odd_prime_one_not_mod_predecessor p
  4. L81
    specialize odd_prime_one_not_mod_predecessor (2 * h)
  5. L82
    specialize odd_prime_one_not_mod_predecessor h
  6. L83
    apply odd_prime_one_not_mod_predecessor
  7. L84
    exact hpsucc
  8. L85
    exact hprime
  9. L86
    symm
  10. L87
    exact hdouble
17Use earlier factsL88–88

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

  1. L88
    exact hcollision
18Establish hqres_evenL89–91

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

  1. L89
    have hqres_even : (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even)
  2. L90
    intro hqres
  3. L91
    specialize parity_cases x
19Separate the logical casesL92–93

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

  1. L92
    cases parity_cases
  2. L93
    cases parity_cases_witness
20Construct an explicit witnessL94–94

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

  1. L94
    exists x3
21Use earlier factsL95–95

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

  1. L95
    exact parity_cases_witness_left
22Separate the logical casesL96–96

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

  1. L96
    exfalso
23Use earlier factsL97–97

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

  1. L97
    apply hseparation
24Establish hAoneL98–100

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

  1. L98
    have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  2. L99
    apply heuler_left_left
  3. L100
    exact hqres
25Establish honeAL101–106

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

  1. L101
    have honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
  2. L102
    specialize mod_eq_symm p
  3. L103
    specialize mod_eq_symm x1
  4. L104
    specialize mod_eq_symm 1
  5. L105
    apply mod_eq_symm
  6. L106
    exact hAone
26Establish honeRL107–114

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

  1. L107
    have honeR : exists wpp_mod_left_glb_local_one_mod_r wpp_mod_right_glb_local_one_mod_r. (1) + p * wpp_mod_left_glb_local_one_mod_r = (x2) + p * wpp_mod_right_glb_local_one_mod_r
  2. L108
    specialize mod_eq_trans p
  3. L109
    specialize mod_eq_trans 1
  4. L110
    specialize mod_eq_trans x1
  5. L111
    specialize mod_eq_trans x2
  6. L112
    apply mod_eq_trans
  7. L113
    exact honeA
  8. L114
    exact hgauss_witness_witness_witness_right_right_right
27Establish hRpredL115–116

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

  1. L115
    have hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
  2. L116
    apply hbridge_right
28Construct an explicit witnessL117–117

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

  1. L117
    exists x3
29Use earlier factsL118–125

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

  1. L118
    exact parity_cases_witness_right
  2. L119
    specialize mod_eq_trans p
  3. L120
    specialize mod_eq_trans 1
  4. L121
    specialize mod_eq_trans x2
  5. L122
    specialize mod_eq_trans (2 * h)
  6. L123
    apply mod_eq_trans
  7. L124
    exact honeR
  8. L125
    exact hRpred
30Establish heven_qresL126–127

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

  1. L126
    have heven_qres : (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
  2. L127
    intro heven
31Establish hRoneL128–130

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

  1. L128
    have hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
  2. L129
    apply hbridge_left
  3. L130
    exact heven
32Establish hAoneL131–140

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

  1. L131
    have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  2. L132
    specialize mod_eq_trans p
  3. L133
    specialize mod_eq_trans x1
  4. L134
    specialize mod_eq_trans x2
  5. L135
    specialize mod_eq_trans 1
  6. L136
    apply mod_eq_trans
  7. L137
    exact hgauss_witness_witness_witness_right_right_right
  8. L138
    exact hRone
  9. L139
    apply heuler_left_right
  10. L140
    exact hAone
33Establish hnonres_oddL141–143

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

  1. L141
    have hnonres_odd : ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1)
  2. L142
    intro hnonres
  3. L143
    specialize parity_cases x
34Separate the logical casesL144–146

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

  1. L144
    cases parity_cases
  2. L145
    cases parity_cases_witness
  3. L146
    exfalso
35Use earlier factsL147–147

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

  1. L147
    apply hseparation
36Establish hRoneL148–149

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

  1. L148
    have hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
  2. L149
    apply hbridge_left
37Construct an explicit witnessL150–150

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

  1. L150
    exists x3
38Use earlier factsL151–151

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

  1. L151
    exact parity_cases_witness_left
39Establish hAoneL152–159

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

  1. L152
    have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  2. L153
    specialize mod_eq_trans p
  3. L154
    specialize mod_eq_trans x1
  4. L155
    specialize mod_eq_trans x2
  5. L156
    specialize mod_eq_trans 1
  6. L157
    apply mod_eq_trans
  7. L158
    exact hgauss_witness_witness_witness_right_right_right
  8. L159
    exact hRone
40Establish honeAL160–165

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

  1. L160
    have honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
  2. L161
    specialize mod_eq_symm p
  3. L162
    specialize mod_eq_symm x1
  4. L163
    specialize mod_eq_symm 1
  5. L164
    apply mod_eq_symm
  6. L165
    exact hAone
41Establish hApredL166–175

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

  1. L166
    have hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
  2. L167
    apply heuler_right_left
  3. L168
    exact hnonres
  4. L169
    specialize mod_eq_trans p
  5. L170
    specialize mod_eq_trans 1
  6. L171
    specialize mod_eq_trans x1
  7. L172
    specialize mod_eq_trans (2 * h)
  8. L173
    apply mod_eq_trans
  9. L174
    exact honeA
  10. L175
    exact hApred
42Construct an explicit witnessL176–176

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

  1. L176
    exists x3
43Use earlier factsL177–177

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

  1. L177
    exact parity_cases_witness_right
44Establish hodd_nonresL178–179

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

  1. L178
    have hodd_nonres : (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
  2. L179
    intro hodd
45Establish hRpredL180–182

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

  1. L180
    have hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
  2. L181
    apply hbridge_right
  3. L182
    exact hodd
46Establish hApredL183–192

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

  1. L183
    have hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
  2. L184
    specialize mod_eq_trans p
  3. L185
    specialize mod_eq_trans x1
  4. L186
    specialize mod_eq_trans x2
  5. L187
    specialize mod_eq_trans (2 * h)
  6. L188
    apply mod_eq_trans
  7. L189
    exact hgauss_witness_witness_witness_right_right_right
  8. L190
    exact hRpred
  9. L191
    intro hqres
  10. L192
    apply heuler_right_right
47Use earlier factsL193–194

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

  1. L193
    exact hApred
  2. L194
    exact hqres
48Construct an explicit witnessL195–195

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

  1. L195
    exists x
49Separate the logical casesL196–196

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

  1. L196
    split
50Use earlier factsL197–197

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

  1. L197
    exact hgauss_witness_witness_witness_right_right_left
51Separate the logical casesL198–199

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

  1. L198
    split
  2. L199
    split
52Use earlier factsL200–201

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

  1. L200
    exact hqres_even
  2. L201
    exact heven_qres
53Separate the logical casesL202–202

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

  1. L202
    split
54Use earlier factsL203–204

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

  1. L203
    exact hnonres_odd
  2. L204
    exact hodd_nonres

Library-wide reading audit

Original exact command ledger · 204 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpodd
  7. 0007intro hprime
  8. 0008intro hpositive
  9. 0009intro halt
  10. 0010intro hhalf
  11. 0011have hpsucc : p = S (2 * h)
  12. 0012trans 2 * h + 1
  13. 0013exact hpodd
  14. 0014simp
  15. 0015have hdouble : h + h = 2 * h
  16. 0016trans h * 2
  17. 0017simp [zero_add]
  18. 0018specialize mul_comm h
  19. 0019specialize mul_comm 2
  20. 0020apply mul_comm
  21. 0021have ha0 : ~(a = 0)
  22. 0022intro haeq
  23. 0023specialize lt_irrefl_expanded 0
  24. 0024apply lt_irrefl_expanded
  25. 0025rewrite haeq at hpositive
  26. 0026exact hpositive
  27. 0027have hnotdiv : ~(exists frm_factor_glb_nondivisor. a = p * frm_factor_glb_nondivisor)
  28. 0028intro hdiv
  29. 0029specialize bounded_nonzero_not_divides p
  30. 0030specialize bounded_nonzero_not_divides a
  31. 0031apply bounded_nonzero_not_divides
  32. 0032exact ha0
  33. 0033exact halt
  34. 0034exact hdiv
  35. 0035have hgauss : exists e A R. ((exists ff_b_glb_multiplier_power ff_c_glb_multiplier_power. ((forall ff_i_glb_multiplier_power_repeat. (exists ff_lt_glb_multiplier_power_repeat_bound. ff_lt_glb_multiplier_power_repeat_bound + S ff_i_glb_multiplier_power_repeat = h) -> (((exists ff_h_glb_multiplier_power_repeat_decoded. ff_h_glb_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_glb_multiplier_power_repeat)) * ff_c_glb_multiplier_power)) /\ exists ff_q_glb_multiplier_power_repeat_decoded. ff_b_glb_multiplier_power = ff_q_glb_multiplier_power_repeat_decoded * S ((S (ff_i_glb_multiplier_power_repeat)) * ff_c_glb_multiplier_power) + (a)))) /\ (exists ff_u_glb_multiplier_power_product ff_v_glb_multiplier_power_product. ((((exists ff_h_glb_multiplier_power_product_start. ff_h_glb_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_start. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_start * S ((S (0)) * ff_v_glb_multiplier_power_product) + (1))) /\ ((((exists ff_h_glb_multiplier_power_product_terminal. ff_h_glb_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_terminal. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_terminal * S ((S (h)) * ff_v_glb_multiplier_power_product) + (A))) /\ forall ff_i_glb_multiplier_power_product. (exists ff_lt_glb_multiplier_power_product_bound. ff_lt_glb_multiplier_power_product_bound + S ff_i_glb_multiplier_power_product = h) -> exists ff_p_glb_multiplier_power_product ff_r_glb_multiplier_power_product ff_s_glb_multiplier_power_product. ((((exists ff_h_glb_multiplier_power_product_factor. ff_h_glb_multiplier_power_product_factor + S (ff_p_glb_multiplier_power_product) = S ((S (ff_i_glb_multiplier_power_product)) * ff_c_glb_multiplier_power)) /\ exists ff_q_glb_multiplier_power_product_factor. ff_b_glb_multiplier_power = ff_q_glb_multiplier_power_product_factor * S ((S (ff_i_glb_multiplier_power_product)) * ff_c_glb_multiplier_power) + (ff_p_glb_multiplier_power_product))) /\ ((((exists ff_h_glb_multiplier_power_product_partial. ff_h_glb_multiplier_power_product_partial + S (ff_r_glb_multiplier_power_product) = S ((S (ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_partial. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_partial * S ((S (ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product) + (ff_r_glb_multiplier_power_product))) /\ ((((exists ff_h_glb_multiplier_power_product_successor. ff_h_glb_multiplier_power_product_successor + S (ff_s_glb_multiplier_power_product) = S ((S (S ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_successor. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_successor * S ((S (S ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product) + (ff_s_glb_multiplier_power_product))) /\ ff_s_glb_multiplier_power_product = ff_r_glb_multiplier_power_product * ff_p_glb_multiplier_power_product)))))))) /\ ((exists ff_b_glb_sign_power_expanded ff_c_glb_sign_power_expanded. ((forall ff_i_glb_sign_power_expanded_repeat. (exists ff_lt_glb_sign_power_expanded_repeat_bound. ff_lt_glb_sign_power_expanded_repeat_bound + S ff_i_glb_sign_power_expanded_repeat = e) -> (((exists ff_h_glb_sign_power_expanded_repeat_decoded. ff_h_glb_sign_power_expanded_repeat_decoded + S ((2 * h)) = S ((S (ff_i_glb_sign_power_expanded_repeat)) * ff_c_glb_sign_power_expanded)) /\ exists ff_q_glb_sign_power_expanded_repeat_decoded. ff_b_glb_sign_power_expanded = ff_q_glb_sign_power_expanded_repeat_decoded * S ((S (ff_i_glb_sign_power_expanded_repeat)) * ff_c_glb_sign_power_expanded) + ((2 * h))))) /\ (exists ff_u_glb_sign_power_expanded_product ff_v_glb_sign_power_expanded_product. ((((exists ff_h_glb_sign_power_expanded_product_start. ff_h_glb_sign_power_expanded_product_start + S (1) = S ((S (0)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_start. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_start * S ((S (0)) * ff_v_glb_sign_power_expanded_product) + (1))) /\ ((((exists ff_h_glb_sign_power_expanded_product_terminal. ff_h_glb_sign_power_expanded_product_terminal + S (R) = S ((S (e)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_terminal. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_terminal * S ((S (e)) * ff_v_glb_sign_power_expanded_product) + (R))) /\ forall ff_i_glb_sign_power_expanded_product. (exists ff_lt_glb_sign_power_expanded_product_bound. ff_lt_glb_sign_power_expanded_product_bound + S ff_i_glb_sign_power_expanded_product = e) -> exists ff_p_glb_sign_power_expanded_product ff_r_glb_sign_power_expanded_product ff_s_glb_sign_power_expanded_product. ((((exists ff_h_glb_sign_power_expanded_product_factor. ff_h_glb_sign_power_expanded_product_factor + S (ff_p_glb_sign_power_expanded_product) = S ((S (ff_i_glb_sign_power_expanded_product)) * ff_c_glb_sign_power_expanded)) /\ exists ff_q_glb_sign_power_expanded_product_factor. ff_b_glb_sign_power_expanded = ff_q_glb_sign_power_expanded_product_factor * S ((S (ff_i_glb_sign_power_expanded_product)) * ff_c_glb_sign_power_expanded) + (ff_p_glb_sign_power_expanded_product))) /\ ((((exists ff_h_glb_sign_power_expanded_product_partial. ff_h_glb_sign_power_expanded_product_partial + S (ff_r_glb_sign_power_expanded_product) = S ((S (ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_partial. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_partial * S ((S (ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product) + (ff_r_glb_sign_power_expanded_product))) /\ ((((exists ff_h_glb_sign_power_expanded_product_successor. ff_h_glb_sign_power_expanded_product_successor + S (ff_s_glb_sign_power_expanded_product) = S ((S (S ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_successor. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_successor * S ((S (S ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product) + (ff_s_glb_sign_power_expanded_product))) /\ ff_s_glb_sign_power_expanded_product = ff_r_glb_sign_power_expanded_product * ff_p_glb_sign_power_expanded_product)))))))) /\ ((exists mb mc sb sc. ((forall gsp_index_glb_signed_prefix. (exists gsp_lt_gap_glb_signed_prefix_index_bound. gsp_lt_gap_glb_signed_prefix_index_bound + S gsp_index_glb_signed_prefix = h) -> (exists gsp_value_glb_signed_prefix_entry gsp_magnitude_glb_signed_prefix_entry gsp_sign_glb_signed_prefix_entry. (((exists ff_h_gsp_glb_signed_prefix_entry_source. ff_h_gsp_glb_signed_prefix_entry_source + S (gsp_value_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * c)) /\ exists ff_q_gsp_glb_signed_prefix_entry_source. b = ff_q_gsp_glb_signed_prefix_entry_source * S ((S (gsp_index_glb_signed_prefix)) * c) + (gsp_value_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_magnitude. ff_h_gsp_glb_signed_prefix_entry_magnitude + S (gsp_magnitude_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * mc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_magnitude. mb = ff_q_gsp_glb_signed_prefix_entry_magnitude * S ((S (gsp_index_glb_signed_prefix)) * mc) + (gsp_magnitude_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_sign. ff_h_gsp_glb_signed_prefix_entry_sign + S (gsp_sign_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * sc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_sign. sb = ff_q_gsp_glb_signed_prefix_entry_sign * S ((S (gsp_index_glb_signed_prefix)) * sc) + (gsp_sign_glb_signed_prefix_entry))) /\ ((exists gsp_lt_gap_glb_signed_prefix_entry_positive. gsp_lt_gap_glb_signed_prefix_entry_positive + S 0 = gsp_magnitude_glb_signed_prefix_entry) /\ ((exists gsp_le_gap_glb_signed_prefix_entry_bounded. gsp_le_gap_glb_signed_prefix_entry_bounded + gsp_magnitude_glb_signed_prefix_entry = h) /\ ((gsp_sign_glb_signed_prefix_entry = 0 \/ gsp_sign_glb_signed_prefix_entry = 1) /\ (((gsp_sign_glb_signed_prefix_entry = 0 /\ (exists gsp_mod_left_glb_signed_prefix_entry_lower gsp_mod_right_glb_signed_prefix_entry_lower. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_lower = (gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_lower)) \/ (gsp_sign_glb_signed_prefix_entry = 1 /\ (exists gsp_mod_left_glb_signed_prefix_entry_reflected gsp_mod_right_glb_signed_prefix_entry_reflected. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_reflected))))))))))) /\ (((exists ff_u_glb_count_sum ff_v_glb_count_sum. ((((exists ff_h_glb_count_sum_start. ff_h_glb_count_sum_start + S (0) = S ((S (0)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_start. ff_u_glb_count_sum = ff_q_glb_count_sum_start * S ((S (0)) * ff_v_glb_count_sum) + (0))) /\ ((((exists ff_h_glb_count_sum_terminal. ff_h_glb_count_sum_terminal + S (e) = S ((S (h)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_terminal. ff_u_glb_count_sum = ff_q_glb_count_sum_terminal * S ((S (h)) * ff_v_glb_count_sum) + (e))) /\ forall ff_i_glb_count_sum. (exists ff_lt_glb_count_sum_bound. ff_lt_glb_count_sum_bound + S ff_i_glb_count_sum = h) -> exists ff_a_glb_count_sum ff_r_glb_count_sum ff_s_glb_count_sum. ((((exists ff_h_glb_count_sum_summand. ff_h_glb_count_sum_summand + S (ff_a_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * sc)) /\ exists ff_q_glb_count_sum_summand. sb = ff_q_glb_count_sum_summand * S ((S (ff_i_glb_count_sum)) * sc) + (ff_a_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_partial. ff_h_glb_count_sum_partial + S (ff_r_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_partial. ff_u_glb_count_sum = ff_q_glb_count_sum_partial * S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_r_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_successor. ff_h_glb_count_sum_successor + S (ff_s_glb_count_sum) = S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_successor. ff_u_glb_count_sum = ff_q_glb_count_sum_successor * S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_s_glb_count_sum))) /\ ff_s_glb_count_sum = ff_r_glb_count_sum + ff_a_glb_count_sum)))))) /\ (forall ff_i_glb_count_bits. (exists ff_lt_glb_count_bits_bound. ff_lt_glb_count_bits_bound + S ff_i_glb_count_bits = h) -> exists ff_bit_glb_count_bits. ((((exists ff_h_glb_count_bits_decoded. ff_h_glb_count_bits_decoded + S (ff_bit_glb_count_bits) = S ((S (ff_i_glb_count_bits)) * sc)) /\ exists ff_q_glb_count_bits_decoded. sb = ff_q_glb_count_bits_decoded * S ((S (ff_i_glb_count_bits)) * sc) + (ff_bit_glb_count_bits))) /\ (ff_bit_glb_count_bits = 0 \/ ff_bit_glb_count_bits = 1))))))) /\ (exists wpp_mod_left_glb_a_mod_r wpp_mod_right_glb_a_mod_r. (A) + p * wpp_mod_left_glb_a_mod_r = (R) + p * wpp_mod_right_glb_a_mod_r))))
  36. 0036specialize gauss_lemma_power_congruence_exists p
  37. 0037specialize gauss_lemma_power_congruence_exists h
  38. 0038specialize gauss_lemma_power_congruence_exists a
  39. 0039specialize gauss_lemma_power_congruence_exists b
  40. 0040specialize gauss_lemma_power_congruence_exists c
  41. 0041apply gauss_lemma_power_congruence_exists
  42. 0042exact hpodd
  43. 0043exact hprime
  44. 0044exact hnotdiv
  45. 0045exact hhalf
  46. 0046cases hgauss
  47. 0047cases hgauss_witness
  48. 0048cases hgauss_witness_witness
  49. 0049cases hgauss_witness_witness_witness
  50. 0050cases hgauss_witness_witness_witness_right
  51. 0051cases hgauss_witness_witness_witness_right_right
  52. 0052have heuler : (((((exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one)) /\ ((exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)))) /\ ((~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor)) /\ ((exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres))))
  53. 0053specialize bounded_euler_criterion_complete p
  54. 0054specialize bounded_euler_criterion_complete a
  55. 0055specialize bounded_euler_criterion_complete (2 * h)
  56. 0056specialize bounded_euler_criterion_complete h
  57. 0057specialize bounded_euler_criterion_complete x1
  58. 0058apply bounded_euler_criterion_complete
  59. 0059exact hpsucc
  60. 0060exact hprime
  61. 0061exact ha0
  62. 0062exact halt
  63. 0063symm
  64. 0064exact hdouble
  65. 0065exact hgauss_witness_witness_witness_left
  66. 0066cases heuler
  67. 0067cases heuler_left
  68. 0068cases heuler_right
  69. 0069have hbridge : (((exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one)) /\ ((exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> (exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor)))
  70. 0070specialize pow_predecessor_parity_mod p
  71. 0071specialize pow_predecessor_parity_mod (2 * h)
  72. 0072specialize pow_predecessor_parity_mod x
  73. 0073specialize pow_predecessor_parity_mod x2
  74. 0074apply pow_predecessor_parity_mod
  75. 0075exact hpsucc
  76. 0076exact hgauss_witness_witness_witness_right_left
  77. 0077cases hbridge
  78. 0078have hseparation : ~(exists wpp_mod_left_glb_one_mod_predecessor wpp_mod_right_glb_one_mod_predecessor. (1) + p * wpp_mod_left_glb_one_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_one_mod_predecessor)
  79. 0079intro hcollision
  80. 0080specialize odd_prime_one_not_mod_predecessor p
  81. 0081specialize odd_prime_one_not_mod_predecessor (2 * h)
  82. 0082specialize odd_prime_one_not_mod_predecessor h
  83. 0083apply odd_prime_one_not_mod_predecessor
  84. 0084exact hpsucc
  85. 0085exact hprime
  86. 0086symm
  87. 0087exact hdouble
  88. 0088exact hcollision
  89. 0089have hqres_even : (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even)
  90. 0090intro hqres
  91. 0091specialize parity_cases x
  92. 0092cases parity_cases
  93. 0093cases parity_cases_witness
  94. 0094exists x3
  95. 0095exact parity_cases_witness_left
  96. 0096exfalso
  97. 0097apply hseparation
  98. 0098have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  99. 0099apply heuler_left_left
  100. 0100exact hqres
  101. 0101have honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
  102. 0102specialize mod_eq_symm p
  103. 0103specialize mod_eq_symm x1
  104. 0104specialize mod_eq_symm 1
  105. 0105apply mod_eq_symm
  106. 0106exact hAone
  107. 0107have honeR : exists wpp_mod_left_glb_local_one_mod_r wpp_mod_right_glb_local_one_mod_r. (1) + p * wpp_mod_left_glb_local_one_mod_r = (x2) + p * wpp_mod_right_glb_local_one_mod_r
  108. 0108specialize mod_eq_trans p
  109. 0109specialize mod_eq_trans 1
  110. 0110specialize mod_eq_trans x1
  111. 0111specialize mod_eq_trans x2
  112. 0112apply mod_eq_trans
  113. 0113exact honeA
  114. 0114exact hgauss_witness_witness_witness_right_right_right
  115. 0115have hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
  116. 0116apply hbridge_right
  117. 0117exists x3
  118. 0118exact parity_cases_witness_right
  119. 0119specialize mod_eq_trans p
  120. 0120specialize mod_eq_trans 1
  121. 0121specialize mod_eq_trans x2
  122. 0122specialize mod_eq_trans (2 * h)
  123. 0123apply mod_eq_trans
  124. 0124exact honeR
  125. 0125exact hRpred
  126. 0126have heven_qres : (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
  127. 0127intro heven
  128. 0128have hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
  129. 0129apply hbridge_left
  130. 0130exact heven
  131. 0131have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  132. 0132specialize mod_eq_trans p
  133. 0133specialize mod_eq_trans x1
  134. 0134specialize mod_eq_trans x2
  135. 0135specialize mod_eq_trans 1
  136. 0136apply mod_eq_trans
  137. 0137exact hgauss_witness_witness_witness_right_right_right
  138. 0138exact hRone
  139. 0139apply heuler_left_right
  140. 0140exact hAone
  141. 0141have hnonres_odd : ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1)
  142. 0142intro hnonres
  143. 0143specialize parity_cases x
  144. 0144cases parity_cases
  145. 0145cases parity_cases_witness
  146. 0146exfalso
  147. 0147apply hseparation
  148. 0148have hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
  149. 0149apply hbridge_left
  150. 0150exists x3
  151. 0151exact parity_cases_witness_left
  152. 0152have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  153. 0153specialize mod_eq_trans p
  154. 0154specialize mod_eq_trans x1
  155. 0155specialize mod_eq_trans x2
  156. 0156specialize mod_eq_trans 1
  157. 0157apply mod_eq_trans
  158. 0158exact hgauss_witness_witness_witness_right_right_right
  159. 0159exact hRone
  160. 0160have honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
  161. 0161specialize mod_eq_symm p
  162. 0162specialize mod_eq_symm x1
  163. 0163specialize mod_eq_symm 1
  164. 0164apply mod_eq_symm
  165. 0165exact hAone
  166. 0166have hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
  167. 0167apply heuler_right_left
  168. 0168exact hnonres
  169. 0169specialize mod_eq_trans p
  170. 0170specialize mod_eq_trans 1
  171. 0171specialize mod_eq_trans x1
  172. 0172specialize mod_eq_trans (2 * h)
  173. 0173apply mod_eq_trans
  174. 0174exact honeA
  175. 0175exact hApred
  176. 0176exists x3
  177. 0177exact parity_cases_witness_right
  178. 0178have hodd_nonres : (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
  179. 0179intro hodd
  180. 0180have hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
  181. 0181apply hbridge_right
  182. 0182exact hodd
  183. 0183have hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
  184. 0184specialize mod_eq_trans p
  185. 0185specialize mod_eq_trans x1
  186. 0186specialize mod_eq_trans x2
  187. 0187specialize mod_eq_trans (2 * h)
  188. 0188apply mod_eq_trans
  189. 0189exact hgauss_witness_witness_witness_right_right_right
  190. 0190exact hRpred
  191. 0191intro hqres
  192. 0192apply heuler_right_right
  193. 0193exact hApred
  194. 0194exact hqres
  195. 0195exists x
  196. 0196split
  197. 0197exact hgauss_witness_witness_witness_right_right_left
  198. 0198split
  199. 0199split
  200. 0200exact hqres_even
  201. 0201exact heven_qres
  202. 0202split
  203. 0203exact hnonres_odd
  204. 0204exact hodd_nonres