PA00D7 · theorem

odd_prime_gauss_eisenstein_orientation_data_exists

Alpha v34 checked-use theorem · independently closed; not Stable

One odd prime orientation has complete Gauss classification and a congruent exact Eisenstein quotient sum.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ h. ∀ a. p = 2 · h + 1 → Odd(a) → Prime(p) → ¬Dvd(p,a) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. (∀ u. ∀ v. Lt(u,h) → BetaAt(x,y,u,v) → v = a · (1 + u)) ∧ (DivisionPrefix(p,x,y,z,n,m,k,h) ∧ (Sum(z,n,h,j) ∧ ((QRes(p,a) → Even(i)) ∧ (Even(i) → QRes(p,a)) ∧ ((¬QRes(p,a) → Odd(i)) ∧ (Odd(i) → ¬QRes(p,a))) ∧ ModEq(2,i,j))))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0009 Even PD0010 Odd PD0013 BetaAt PD0015 Sum PD0021 QRes PD0040 DivisionPrefix

16 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0009 Even PD0010 Odd PD0013 BetaAt PD0015 Sum PD0017 BitCount PD0018 Range PD0021 QRes PD0040 DivisionPrefix

24 occurrences

Exact expanded native-PA statement
forall p h a. p = 2 * h + 1 -> (exists gs_odd_ged_orientation_odd. a = 2 * gs_odd_ged_orientation_odd + 1) -> ((~(p = 1) /\ forall gsp_prime_left_ged_orientation_prime gsp_prime_right_ged_orientation_prime. p = gsp_prime_left_ged_orientation_prime * gsp_prime_right_ged_orientation_prime -> gsp_prime_left_ged_orientation_prime = 1 \/ gsp_prime_right_ged_orientation_prime = 1)) -> (~(exists gsp_divisor_factor_ged_orientation_nondivisor. a = p * gsp_divisor_factor_ged_orientation_nondivisor)) -> (exists tb tc qb qc rb rc e Q. ((forall esd_index_ged_orientation_scaled esd_value_ged_orientation_scaled. (exists esd_gap_ged_orientation_scaled. esd_gap_ged_orientation_scaled + S esd_index_ged_orientation_scaled = h) -> (((exists ff_h_esd_ged_orientation_scaled_decoded. ff_h_esd_ged_orientation_scaled_decoded + S (esd_value_ged_orientation_scaled) = S ((S (esd_index_ged_orientation_scaled)) * tc)) /\ exists ff_q_esd_ged_orientation_scaled_decoded. tb = ff_q_esd_ged_orientation_scaled_decoded * S ((S (esd_index_ged_orientation_scaled)) * tc) + (esd_value_ged_orientation_scaled))) -> esd_value_ged_orientation_scaled = a * (1 + esd_index_ged_orientation_scaled)) /\ ((forall fdp_index_ged_orientation_division. (exists gsp_lt_gap_ged_orientation_division_index_bound. gsp_lt_gap_ged_orientation_division_index_bound + S fdp_index_ged_orientation_division = h) -> exists fdp_value_ged_orientation_division fdp_quotient_ged_orientation_division fdp_remainder_ged_orientation_division. (((exists ff_h_fdp_ged_orientation_division_source. ff_h_fdp_ged_orientation_division_source + S (fdp_value_ged_orientation_division) = S ((S (fdp_index_ged_orientation_division)) * tc)) /\ exists ff_q_fdp_ged_orientation_division_source. tb = ff_q_fdp_ged_orientation_division_source * S ((S (fdp_index_ged_orientation_division)) * tc) + (fdp_value_ged_orientation_division))) /\ ((((exists ff_h_fdp_ged_orientation_division_quotient_entry. ff_h_fdp_ged_orientation_division_quotient_entry + S (fdp_quotient_ged_orientation_division) = S ((S (fdp_index_ged_orientation_division)) * qc)) /\ exists ff_q_fdp_ged_orientation_division_quotient_entry. qb = ff_q_fdp_ged_orientation_division_quotient_entry * S ((S (fdp_index_ged_orientation_division)) * qc) + (fdp_quotient_ged_orientation_division))) /\ ((((exists ff_h_fdp_ged_orientation_division_remainder_entry. ff_h_fdp_ged_orientation_division_remainder_entry + S (fdp_remainder_ged_orientation_division) = S ((S (fdp_index_ged_orientation_division)) * rc)) /\ exists ff_q_fdp_ged_orientation_division_remainder_entry. rb = ff_q_fdp_ged_orientation_division_remainder_entry * S ((S (fdp_index_ged_orientation_division)) * rc) + (fdp_remainder_ged_orientation_division))) /\ (fdp_value_ged_orientation_division = p * fdp_quotient_ged_orientation_division + fdp_remainder_ged_orientation_division /\ (exists gsp_lt_gap_ged_orientation_division_remainder_bound. gsp_lt_gap_ged_orientation_division_remainder_bound + S fdp_remainder_ged_orientation_division = p))))) /\ ((exists ff_u_ged_orientation_sum ff_v_ged_orientation_sum. ((((exists ff_h_ged_orientation_sum_start. ff_h_ged_orientation_sum_start + S (0) = S ((S (0)) * ff_v_ged_orientation_sum)) /\ exists ff_q_ged_orientation_sum_start. ff_u_ged_orientation_sum = ff_q_ged_orientation_sum_start * S ((S (0)) * ff_v_ged_orientation_sum) + (0))) /\ ((((exists ff_h_ged_orientation_sum_terminal. ff_h_ged_orientation_sum_terminal + S (Q) = S ((S (h)) * ff_v_ged_orientation_sum)) /\ exists ff_q_ged_orientation_sum_terminal. ff_u_ged_orientation_sum = ff_q_ged_orientation_sum_terminal * S ((S (h)) * ff_v_ged_orientation_sum) + (Q))) /\ forall ff_i_ged_orientation_sum. (exists ff_lt_ged_orientation_sum_bound. ff_lt_ged_orientation_sum_bound + S ff_i_ged_orientation_sum = h) -> exists ff_a_ged_orientation_sum ff_r_ged_orientation_sum ff_s_ged_orientation_sum. ((((exists ff_h_ged_orientation_sum_summand. ff_h_ged_orientation_sum_summand + S (ff_a_ged_orientation_sum) = S ((S (ff_i_ged_orientation_sum)) * qc)) /\ exists ff_q_ged_orientation_sum_summand. qb = ff_q_ged_orientation_sum_summand * S ((S (ff_i_ged_orientation_sum)) * qc) + (ff_a_ged_orientation_sum))) /\ ((((exists ff_h_ged_orientation_sum_partial. ff_h_ged_orientation_sum_partial + S (ff_r_ged_orientation_sum) = S ((S (ff_i_ged_orientation_sum)) * ff_v_ged_orientation_sum)) /\ exists ff_q_ged_orientation_sum_partial. ff_u_ged_orientation_sum = ff_q_ged_orientation_sum_partial * S ((S (ff_i_ged_orientation_sum)) * ff_v_ged_orientation_sum) + (ff_r_ged_orientation_sum))) /\ ((((exists ff_h_ged_orientation_sum_successor. ff_h_ged_orientation_sum_successor + S (ff_s_ged_orientation_sum) = S ((S (S ff_i_ged_orientation_sum)) * ff_v_ged_orientation_sum)) /\ exists ff_q_ged_orientation_sum_successor. ff_u_ged_orientation_sum = ff_q_ged_orientation_sum_successor * S ((S (S ff_i_ged_orientation_sum)) * ff_v_ged_orientation_sum) + (ff_s_ged_orientation_sum))) /\ ff_s_ged_orientation_sum = ff_r_ged_orientation_sum + ff_a_ged_orientation_sum)))))) /\ (((((((exists qr_x_ged_orientation_classification_qres. exists qr_u_ged_orientation_classification_qres qr_v_ged_orientation_classification_qres. qr_x_ged_orientation_classification_qres * qr_x_ged_orientation_classification_qres + p * qr_u_ged_orientation_classification_qres = a + p * qr_v_ged_orientation_classification_qres) -> (exists gs_even_ged_orientation_classification_even. e = 2 * gs_even_ged_orientation_classification_even)) /\ ((exists gs_even_ged_orientation_classification_even. e = 2 * gs_even_ged_orientation_classification_even) -> (exists qr_x_ged_orientation_classification_qres. exists qr_u_ged_orientation_classification_qres qr_v_ged_orientation_classification_qres. qr_x_ged_orientation_classification_qres * qr_x_ged_orientation_classification_qres + p * qr_u_ged_orientation_classification_qres = a + p * qr_v_ged_orientation_classification_qres)))) /\ (((~(exists qr_x_ged_orientation_classification_qres. exists qr_u_ged_orientation_classification_qres qr_v_ged_orientation_classification_qres. qr_x_ged_orientation_classification_qres * qr_x_ged_orientation_classification_qres + p * qr_u_ged_orientation_classification_qres = a + p * qr_v_ged_orientation_classification_qres) -> (exists gs_odd_ged_orientation_classification_odd. e = 2 * gs_odd_ged_orientation_classification_odd + 1)) /\ ((exists gs_odd_ged_orientation_classification_odd. e = 2 * gs_odd_ged_orientation_classification_odd + 1) -> ~(exists qr_x_ged_orientation_classification_qres. exists qr_u_ged_orientation_classification_qres qr_v_ged_orientation_classification_qres. qr_x_ged_orientation_classification_qres * qr_x_ged_orientation_classification_qres + p * qr_u_ged_orientation_classification_qres = a + p * qr_v_ged_orientation_classification_qres)))))) /\ (exists fspm_u_ged_orientation_count_mod_sum fspm_v_ged_orientation_count_mod_sum. (e) + 2 * fspm_u_ged_orientation_count_mod_sum = (Q) + 2 * fspm_v_ged_orientation_count_mod_sum))))))

Proof neighborhood

Direct theorem prerequisites

PA0030 beta_range_exists PA00BV arbitrary_gauss_lemma_complete PA00C1 prime_scaled_half_quotient_sum_exists PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA003L mod_eq_symm

Direct theorem dependents

PA00FG distinct_odd_primes_gauss_eisenstein_data_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

102 script commands · 21 reading checkpoints · 5 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 (5)
beta range existsarbitrary gauss lemma completeprime scaled half quotient sum existsgauss eisenstein sign count mod quotient summod eq symm
01Fix variables and assumptionsL1–7

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 hpodd
  5. L5
    intro haodd
  6. L6
    intro hprime
  7. L7
    intro hnotdiv
02Establish hhalf_existsL8–11

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

  1. L8
    have hhalf_exists : ∃ b. ∃ c. Range(b,c,1,h)Definitions: Range(b,c,1,h)Original native command in the exact edition
  2. L9
    specialize beta_range_exists 1
  3. L10
    specialize beta_range_exists h
  4. L11
    exact beta_range_exists
03Separate the logical casesL12–13

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

  1. L12
    cases hhalf_exists
  2. L13
    cases hhalf_exists_witness
04Establish hgaussL14–23

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

  1. L14
    have hgauss : ∃ e. (∃ y. ∃ z. ∃ n. ∃ m. (∀ k. Lt(k,h) → ∃ i. ∃ j. ∃ u. BetaAt(x,x1,k,i) ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(n,m,k,u) ∧ (Lt(0,j) ∧ (Le(j,h) ∧ ((u = 0 ∨ u = 1) ∧ (u = 0 ∧ ModEq(p,a · i,j) ∨ u = 1 ∧ ModEq(p,a · i,2 · h · j)))))))) ∧ BitCount(n,m,h,e)) ∧ ((QRes(p,a) → Even(e)) ∧ (Even(e) → QRes(p,a)) ∧ ((¬QRes(p,a) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,a))))Definitions: Lt(k,h)BetaAt(x,x1,k,i)BetaAt(y,z,k,j)BetaAt(n,m,k,u)Lt(0,j)Le(j,h)ModEq(p,a · i,j)ModEq(p,a · i,2 · h · j)BitCount(n,m,h,e)QRes(p,a)Even(e)Odd(e)Original native command in the exact edition
  2. L15
    specialize arbitrary_gauss_lemma_complete p
  3. L16
    specialize arbitrary_gauss_lemma_complete h
  4. L17
    specialize arbitrary_gauss_lemma_complete a
  5. L18
    specialize arbitrary_gauss_lemma_complete x
  6. L19
    specialize arbitrary_gauss_lemma_complete x1
  7. L20
    apply arbitrary_gauss_lemma_complete
  8. L21
    exact hpodd
  9. L22
    exact hprime
  10. L23
    exact hnotdiv
05Use earlier factsL24–24

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

  1. L24
    exact hhalf_exists_witness_witness
06Separate the logical casesL25–31

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

  1. L25
    cases hgauss
  2. L26
    cases hgauss_witness
  3. L27
    cases hgauss_witness_left
  4. L28
    cases hgauss_witness_left_witness
  5. L29
    cases hgauss_witness_left_witness_witness
  6. L30
    cases hgauss_witness_left_witness_witness_witness
  7. L31
    cases hgauss_witness_left_witness_witness_witness_witness
07Establish hquotientL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime scaled half quotient sum exists.

  1. L32
    have hquotient : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∃ Q. (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = a · (1 + x)) ∧ (DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h) ∧ Sum(qb,qc,h,Q))Definitions: Lt(x,h)BetaAt(tb,tc,x,y)DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h)Sum(qb,qc,h,Q)Original native command in the exact edition
  2. L33
    specialize prime_scaled_half_quotient_sum_exists p
  3. L34
    specialize prime_scaled_half_quotient_sum_exists h
  4. L35
    specialize prime_scaled_half_quotient_sum_exists a
  5. L36
    specialize prime_scaled_half_quotient_sum_exists x
  6. L37
    specialize prime_scaled_half_quotient_sum_exists x1
  7. L38
    apply prime_scaled_half_quotient_sum_exists
  8. L39
    exact hpodd
  9. L40
    exact hprime
  10. L41
    exact hhalf_exists_witness_witness
08Separate the logical casesL42–50

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

  1. L42
    cases hquotient
  2. L43
    cases hquotient_witness
  3. L44
    cases hquotient_witness_witness
  4. L45
    cases hquotient_witness_witness_witness
  5. L46
    cases hquotient_witness_witness_witness_witness
  6. L47
    cases hquotient_witness_witness_witness_witness_witness
  7. L48
    cases hquotient_witness_witness_witness_witness_witness_witness
  8. L49
    cases hquotient_witness_witness_witness_witness_witness_witness_witness
  9. L50
    cases hquotient_witness_witness_witness_witness_witness_witness_witness_right
09Establish hquotient_mod_countL51–60

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

  1. L51
    have hquotient_mod_count : ModEq(2,x13,x2)Definitions: ModEq(2,x13,x2)Original native command in the exact edition
  2. L52
    specialize gauss_eisenstein_sign_count_mod_quotient_sum p
  3. L53
    specialize gauss_eisenstein_sign_count_mod_quotient_sum h
  4. L54
    specialize gauss_eisenstein_sign_count_mod_quotient_sum a
  5. L55
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x
  6. L56
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x1
  7. L57
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x7
  8. L58
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x8
  9. L59
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x9
  10. L60
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x10
10Use earlier factsL61–70

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

  1. L61
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x11
  2. L62
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x12
  3. L63
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x3
  4. L64
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x4
  5. L65
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x5
  6. L66
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x6
  7. L67
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x13
  8. L68
    specialize gauss_eisenstein_sign_count_mod_quotient_sum x2
  9. L69
    apply gauss_eisenstein_sign_count_mod_quotient_sum
  10. L70
    exact hpodd
11Use earlier factsL71–79

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

  1. L71
    exact haodd
  2. L72
    exact hprime
  3. L73
    exact hnotdiv
  4. L74
    exact hhalf_exists_witness_witness
  5. L75
    exact hquotient_witness_witness_witness_witness_witness_witness_witness_left
  6. L76
    exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_left
  7. L77
    exact hgauss_witness_left_witness_witness_witness_witness_left
  8. L78
    exact hgauss_witness_left_witness_witness_witness_witness_right
  9. L79
    exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_right
12Establish hcount_mod_quotientL80–85

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

  1. L80
    have hcount_mod_quotient : ModEq(2,x2,x13)Definitions: ModEq(2,x2,x13)Original native command in the exact edition
  2. L81
    specialize mod_eq_symm 2
  3. L82
    specialize mod_eq_symm x13
  4. L83
    specialize mod_eq_symm x2
  5. L84
    apply mod_eq_symm
  6. L85
    exact hquotient_mod_count
13Construct an explicit witnessL86–93

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

  1. L86
    exists x7
  2. L87
    exists x8
  3. L88
    exists x9
  4. L89
    exists x10
  5. L90
    exists x11
  6. L91
    exists x12
  7. L92
    exists x2
  8. L93
    exists x13
14Separate the logical casesL94–94

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

  1. L94
    split
15Use earlier factsL95–95

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

  1. L95
    exact hquotient_witness_witness_witness_witness_witness_witness_witness_left
16Separate the logical casesL96–96

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

  1. L96
    split
17Use earlier factsL97–97

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

  1. L97
    exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_left
18Separate the logical casesL98–98

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

  1. L98
    split
19Use earlier factsL99–99

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

  1. L99
    exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_right
20Separate the logical casesL100–100

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

  1. L100
    split
21Use earlier factsL101–102

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

  1. L101
    exact hgauss_witness_right
  2. L102
    exact hcount_mod_quotient

Library-wide reading audit

Original defined command ledger · 102 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro hpodd
  5. 0005intro haodd
  6. 0006intro hprime
  7. 0007intro hnotdiv
  8. 0008have hhalf_exists : ∃ b. ∃ c. Range(b,c,1,h)
    Exact native replay linehave hhalf_exists : exists b c. (forall gsp_range_index_ged_orientation_half_exists. (exists gsp_lt_gap_ged_orientation_half_exists_range_bound. gsp_lt_gap_ged_orientation_half_exists_range_bound + S gsp_range_index_ged_orientation_half_exists = h) -> (((exists gsp_beta_height_ged_orientation_half_exists_range_entry. gsp_beta_height_ged_orientation_half_exists_range_entry + S (1 + gsp_range_index_ged_orientation_half_exists) = S ((S (gsp_range_index_ged_orientation_half_exists)) * c)) /\ exists gsp_beta_quotient_ged_orientation_half_exists_range_entry. b = gsp_beta_quotient_ged_orientation_half_exists_range_entry * S ((S (gsp_range_index_ged_orientation_half_exists)) * c) + (1 + gsp_range_index_ged_orientation_half_exists))))
  9. 0009specialize beta_range_exists 1
  10. 0010specialize beta_range_exists h
  11. 0011exact beta_range_exists
  12. 0012cases hhalf_exists
  13. 0013cases hhalf_exists_witness
  14. 0014have hgauss : ∃ e. (∃ y. ∃ z. ∃ n. ∃ m. (∀ k. Lt(k,h) → ∃ i. ∃ j. ∃ u. BetaAt(x,x1,k,i) ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(n,m,k,u) ∧ (Lt(0,j) ∧ (Le(j,h) ∧ ((u = 0 ∨ u = 1) ∧ (u = 0 ∧ ModEq(p,a · i,j) ∨ u = 1 ∧ ModEq(p,a · i,2 · h · j)))))))) ∧ BitCount(n,m,h,e)) ∧ ((QRes(p,a) → Even(e)) ∧ (Even(e) → QRes(p,a)) ∧ ((¬QRes(p,a) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,a))))
    Exact native replay linehave hgauss : exists e. ((exists mb mc sb sc. ((forall gsp_index_ged_orientation_hidden_signed. (exists gsp_lt_gap_ged_orientation_hidden_signed_index_bound. gsp_lt_gap_ged_orientation_hidden_signed_index_bound + S gsp_index_ged_orientation_hidden_signed = h) -> (exists gsp_value_ged_orientation_hidden_signed_entry gsp_magnitude_ged_orientation_hidden_signed_entry gsp_sign_ged_orientation_hidden_signed_entry. (((exists ff_h_gsp_ged_orientation_hidden_signed_entry_source. ff_h_gsp_ged_orientation_hidden_signed_entry_source + S (gsp_value_ged_orientation_hidden_signed_entry) = S ((S (gsp_index_ged_orientation_hidden_signed)) * x1)) /\ exists ff_q_gsp_ged_orientation_hidden_signed_entry_source. x = ff_q_gsp_ged_orientation_hidden_signed_entry_source * S ((S (gsp_index_ged_orientation_hidden_signed)) * x1) + (gsp_value_ged_orientation_hidden_signed_entry))) /\ ((((exists ff_h_gsp_ged_orientation_hidden_signed_entry_magnitude. ff_h_gsp_ged_orientation_hidden_signed_entry_magnitude + S (gsp_magnitude_ged_orientation_hidden_signed_entry) = S ((S (gsp_index_ged_orientation_hidden_signed)) * mc)) /\ exists ff_q_gsp_ged_orientation_hidden_signed_entry_magnitude. mb = ff_q_gsp_ged_orientation_hidden_signed_entry_magnitude * S ((S (gsp_index_ged_orientation_hidden_signed)) * mc) + (gsp_magnitude_ged_orientation_hidden_signed_entry))) /\ ((((exists ff_h_gsp_ged_orientation_hidden_signed_entry_sign. ff_h_gsp_ged_orientation_hidden_signed_entry_sign + S (gsp_sign_ged_orientation_hidden_signed_entry) = S ((S (gsp_index_ged_orientation_hidden_signed)) * sc)) /\ exists ff_q_gsp_ged_orientation_hidden_signed_entry_sign. sb = ff_q_gsp_ged_orientation_hidden_signed_entry_sign * S ((S (gsp_index_ged_orientation_hidden_signed)) * sc) + (gsp_sign_ged_orientation_hidden_signed_entry))) /\ ((exists gsp_lt_gap_ged_orientation_hidden_signed_entry_positive. gsp_lt_gap_ged_orientation_hidden_signed_entry_positive + S 0 = gsp_magnitude_ged_orientation_hidden_signed_entry) /\ ((exists gsp_le_gap_ged_orientation_hidden_signed_entry_bounded. gsp_le_gap_ged_orientation_hidden_signed_entry_bounded + gsp_magnitude_ged_orientation_hidden_signed_entry = h) /\ ((gsp_sign_ged_orientation_hidden_signed_entry = 0 \/ gsp_sign_ged_orientation_hidden_signed_entry = 1) /\ (((gsp_sign_ged_orientation_hidden_signed_entry = 0 /\ (exists gsp_mod_left_ged_orientation_hidden_signed_entry_lower gsp_mod_right_ged_orientation_hidden_signed_entry_lower. (a * gsp_value_ged_orientation_hidden_signed_entry) + p * gsp_mod_left_ged_orientation_hidden_signed_entry_lower = (gsp_magnitude_ged_orientation_hidden_signed_entry) + p * gsp_mod_right_ged_orientation_hidden_signed_entry_lower)) \/ (gsp_sign_ged_orientation_hidden_signed_entry = 1 /\ (exists gsp_mod_left_ged_orientation_hidden_signed_entry_reflected gsp_mod_right_ged_orientation_hidden_signed_entry_reflected. (a * gsp_value_ged_orientation_hidden_signed_entry) + p * gsp_mod_left_ged_orientation_hidden_signed_entry_reflected = ((2 * h) * gsp_magnitude_ged_orientation_hidden_signed_entry) + p * gsp_mod_right_ged_orientation_hidden_signed_entry_reflected))))))))))) /\ (((exists ff_u_ged_orientation_hidden_count_sum ff_v_ged_orientation_hidden_count_sum. ((((exists ff_h_ged_orientation_hidden_count_sum_start. ff_h_ged_orientation_hidden_count_sum_start + S (0) = S ((S (0)) * ff_v_ged_orientation_hidden_count_sum)) /\ exists ff_q_ged_orientation_hidden_count_sum_start. ff_u_ged_orientation_hidden_count_sum = ff_q_ged_orientation_hidden_count_sum_start * S ((S (0)) * ff_v_ged_orientation_hidden_count_sum) + (0))) /\ ((((exists ff_h_ged_orientation_hidden_count_sum_terminal. ff_h_ged_orientation_hidden_count_sum_terminal + S (e) = S ((S (h)) * ff_v_ged_orientation_hidden_count_sum)) /\ exists ff_q_ged_orientation_hidden_count_sum_terminal. ff_u_ged_orientation_hidden_count_sum = ff_q_ged_orientation_hidden_count_sum_terminal * S ((S (h)) * ff_v_ged_orientation_hidden_count_sum) + (e))) /\ forall ff_i_ged_orientation_hidden_count_sum. (exists ff_lt_ged_orientation_hidden_count_sum_bound. ff_lt_ged_orientation_hidden_count_sum_bound + S ff_i_ged_orientation_hidden_count_sum = h) -> exists ff_a_ged_orientation_hidden_count_sum ff_r_ged_orientation_hidden_count_sum ff_s_ged_orientation_hidden_count_sum. ((((exists ff_h_ged_orientation_hidden_count_sum_summand. ff_h_ged_orientation_hidden_count_sum_summand + S (ff_a_ged_orientation_hidden_count_sum) = S ((S (ff_i_ged_orientation_hidden_count_sum)) * sc)) /\ exists ff_q_ged_orientation_hidden_count_sum_summand. sb = ff_q_ged_orientation_hidden_count_sum_summand * S ((S (ff_i_ged_orientation_hidden_count_sum)) * sc) + (ff_a_ged_orientation_hidden_count_sum))) /\ ((((exists ff_h_ged_orientation_hidden_count_sum_partial. ff_h_ged_orientation_hidden_count_sum_partial + S (ff_r_ged_orientation_hidden_count_sum) = S ((S (ff_i_ged_orientation_hidden_count_sum)) * ff_v_ged_orientation_hidden_count_sum)) /\ exists ff_q_ged_orientation_hidden_count_sum_partial. ff_u_ged_orientation_hidden_count_sum = ff_q_ged_orientation_hidden_count_sum_partial * S ((S (ff_i_ged_orientation_hidden_count_sum)) * ff_v_ged_orientation_hidden_count_sum) + (ff_r_ged_orientation_hidden_count_sum))) /\ ((((exists ff_h_ged_orientation_hidden_count_sum_successor. ff_h_ged_orientation_hidden_count_sum_successor + S (ff_s_ged_orientation_hidden_count_sum) = S ((S (S ff_i_ged_orientation_hidden_count_sum)) * ff_v_ged_orientation_hidden_count_sum)) /\ exists ff_q_ged_orientation_hidden_count_sum_successor. ff_u_ged_orientation_hidden_count_sum = ff_q_ged_orientation_hidden_count_sum_successor * S ((S (S ff_i_ged_orientation_hidden_count_sum)) * ff_v_ged_orientation_hidden_count_sum) + (ff_s_ged_orientation_hidden_count_sum))) /\ ff_s_ged_orientation_hidden_count_sum = ff_r_ged_orientation_hidden_count_sum + ff_a_ged_orientation_hidden_count_sum)))))) /\ (forall ff_i_ged_orientation_hidden_count_bits. (exists ff_lt_ged_orientation_hidden_count_bits_bound. ff_lt_ged_orientation_hidden_count_bits_bound + S ff_i_ged_orientation_hidden_count_bits = h) -> exists ff_bit_ged_orientation_hidden_count_bits. ((((exists ff_h_ged_orientation_hidden_count_bits_decoded. ff_h_ged_orientation_hidden_count_bits_decoded + S (ff_bit_ged_orientation_hidden_count_bits) = S ((S (ff_i_ged_orientation_hidden_count_bits)) * sc)) /\ exists ff_q_ged_orientation_hidden_count_bits_decoded. sb = ff_q_ged_orientation_hidden_count_bits_decoded * S ((S (ff_i_ged_orientation_hidden_count_bits)) * sc) + (ff_bit_ged_orientation_hidden_count_bits))) /\ (ff_bit_ged_orientation_hidden_count_bits = 0 \/ ff_bit_ged_orientation_hidden_count_bits = 1))))))) /\ ((((((exists qr_x_ged_orientation_hidden_classification_qres. exists qr_u_ged_orientation_hidden_classification_qres qr_v_ged_orientation_hidden_classification_qres. qr_x_ged_orientation_hidden_classification_qres * qr_x_ged_orientation_hidden_classification_qres + p * qr_u_ged_orientation_hidden_classification_qres = a + p * qr_v_ged_orientation_hidden_classification_qres) -> (exists gs_even_ged_orientation_hidden_classification_even. e = 2 * gs_even_ged_orientation_hidden_classification_even)) /\ ((exists gs_even_ged_orientation_hidden_classification_even. e = 2 * gs_even_ged_orientation_hidden_classification_even) -> (exists qr_x_ged_orientation_hidden_classification_qres. exists qr_u_ged_orientation_hidden_classification_qres qr_v_ged_orientation_hidden_classification_qres. qr_x_ged_orientation_hidden_classification_qres * qr_x_ged_orientation_hidden_classification_qres + p * qr_u_ged_orientation_hidden_classification_qres = a + p * qr_v_ged_orientation_hidden_classification_qres)))) /\ (((~(exists qr_x_ged_orientation_hidden_classification_qres. exists qr_u_ged_orientation_hidden_classification_qres qr_v_ged_orientation_hidden_classification_qres. qr_x_ged_orientation_hidden_classification_qres * qr_x_ged_orientation_hidden_classification_qres + p * qr_u_ged_orientation_hidden_classification_qres = a + p * qr_v_ged_orientation_hidden_classification_qres) -> (exists gs_odd_ged_orientation_hidden_classification_odd. e = 2 * gs_odd_ged_orientation_hidden_classification_odd + 1)) /\ ((exists gs_odd_ged_orientation_hidden_classification_odd. e = 2 * gs_odd_ged_orientation_hidden_classification_odd + 1) -> ~(exists qr_x_ged_orientation_hidden_classification_qres. exists qr_u_ged_orientation_hidden_classification_qres qr_v_ged_orientation_hidden_classification_qres. qr_x_ged_orientation_hidden_classification_qres * qr_x_ged_orientation_hidden_classification_qres + p * qr_u_ged_orientation_hidden_classification_qres = a + p * qr_v_ged_orientation_hidden_classification_qres)))))))
  15. 0015specialize arbitrary_gauss_lemma_complete p
  16. 0016specialize arbitrary_gauss_lemma_complete h
  17. 0017specialize arbitrary_gauss_lemma_complete a
  18. 0018specialize arbitrary_gauss_lemma_complete x
  19. 0019specialize arbitrary_gauss_lemma_complete x1
  20. 0020apply arbitrary_gauss_lemma_complete
  21. 0021exact hpodd
  22. 0022exact hprime
  23. 0023exact hnotdiv
  24. 0024exact hhalf_exists_witness_witness
  25. 0025cases hgauss
  26. 0026cases hgauss_witness
  27. 0027cases hgauss_witness_left
  28. 0028cases hgauss_witness_left_witness
  29. 0029cases hgauss_witness_left_witness_witness
  30. 0030cases hgauss_witness_left_witness_witness_witness
  31. 0031cases hgauss_witness_left_witness_witness_witness_witness
  32. 0032have hquotient : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∃ Q. (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = a · (1 + x)) ∧ (DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h) ∧ Sum(qb,qc,h,Q))
    Exact native replay linehave hquotient : exists tb tc qb qc rb rc Q. ((forall esd_index_ged_orientation_hidden_scaled esd_value_ged_orientation_hidden_scaled. (exists esd_gap_ged_orientation_hidden_scaled. esd_gap_ged_orientation_hidden_scaled + S esd_index_ged_orientation_hidden_scaled = h) -> (((exists ff_h_esd_ged_orientation_hidden_scaled_decoded. ff_h_esd_ged_orientation_hidden_scaled_decoded + S (esd_value_ged_orientation_hidden_scaled) = S ((S (esd_index_ged_orientation_hidden_scaled)) * tc)) /\ exists ff_q_esd_ged_orientation_hidden_scaled_decoded. tb = ff_q_esd_ged_orientation_hidden_scaled_decoded * S ((S (esd_index_ged_orientation_hidden_scaled)) * tc) + (esd_value_ged_orientation_hidden_scaled))) -> esd_value_ged_orientation_hidden_scaled = a * (1 + esd_index_ged_orientation_hidden_scaled)) /\ ((forall fdp_index_ged_orientation_hidden_division. (exists gsp_lt_gap_ged_orientation_hidden_division_index_bound. gsp_lt_gap_ged_orientation_hidden_division_index_bound + S fdp_index_ged_orientation_hidden_division = h) -> exists fdp_value_ged_orientation_hidden_division fdp_quotient_ged_orientation_hidden_division fdp_remainder_ged_orientation_hidden_division. (((exists ff_h_fdp_ged_orientation_hidden_division_source. ff_h_fdp_ged_orientation_hidden_division_source + S (fdp_value_ged_orientation_hidden_division) = S ((S (fdp_index_ged_orientation_hidden_division)) * tc)) /\ exists ff_q_fdp_ged_orientation_hidden_division_source. tb = ff_q_fdp_ged_orientation_hidden_division_source * S ((S (fdp_index_ged_orientation_hidden_division)) * tc) + (fdp_value_ged_orientation_hidden_division))) /\ ((((exists ff_h_fdp_ged_orientation_hidden_division_quotient_entry. ff_h_fdp_ged_orientation_hidden_division_quotient_entry + S (fdp_quotient_ged_orientation_hidden_division) = S ((S (fdp_index_ged_orientation_hidden_division)) * qc)) /\ exists ff_q_fdp_ged_orientation_hidden_division_quotient_entry. qb = ff_q_fdp_ged_orientation_hidden_division_quotient_entry * S ((S (fdp_index_ged_orientation_hidden_division)) * qc) + (fdp_quotient_ged_orientation_hidden_division))) /\ ((((exists ff_h_fdp_ged_orientation_hidden_division_remainder_entry. ff_h_fdp_ged_orientation_hidden_division_remainder_entry + S (fdp_remainder_ged_orientation_hidden_division) = S ((S (fdp_index_ged_orientation_hidden_division)) * rc)) /\ exists ff_q_fdp_ged_orientation_hidden_division_remainder_entry. rb = ff_q_fdp_ged_orientation_hidden_division_remainder_entry * S ((S (fdp_index_ged_orientation_hidden_division)) * rc) + (fdp_remainder_ged_orientation_hidden_division))) /\ (fdp_value_ged_orientation_hidden_division = p * fdp_quotient_ged_orientation_hidden_division + fdp_remainder_ged_orientation_hidden_division /\ (exists gsp_lt_gap_ged_orientation_hidden_division_remainder_bound. gsp_lt_gap_ged_orientation_hidden_division_remainder_bound + S fdp_remainder_ged_orientation_hidden_division = p))))) /\ (exists ff_u_ged_orientation_hidden_sum ff_v_ged_orientation_hidden_sum. ((((exists ff_h_ged_orientation_hidden_sum_start. ff_h_ged_orientation_hidden_sum_start + S (0) = S ((S (0)) * ff_v_ged_orientation_hidden_sum)) /\ exists ff_q_ged_orientation_hidden_sum_start. ff_u_ged_orientation_hidden_sum = ff_q_ged_orientation_hidden_sum_start * S ((S (0)) * ff_v_ged_orientation_hidden_sum) + (0))) /\ ((((exists ff_h_ged_orientation_hidden_sum_terminal. ff_h_ged_orientation_hidden_sum_terminal + S (Q) = S ((S (h)) * ff_v_ged_orientation_hidden_sum)) /\ exists ff_q_ged_orientation_hidden_sum_terminal. ff_u_ged_orientation_hidden_sum = ff_q_ged_orientation_hidden_sum_terminal * S ((S (h)) * ff_v_ged_orientation_hidden_sum) + (Q))) /\ forall ff_i_ged_orientation_hidden_sum. (exists ff_lt_ged_orientation_hidden_sum_bound. ff_lt_ged_orientation_hidden_sum_bound + S ff_i_ged_orientation_hidden_sum = h) -> exists ff_a_ged_orientation_hidden_sum ff_r_ged_orientation_hidden_sum ff_s_ged_orientation_hidden_sum. ((((exists ff_h_ged_orientation_hidden_sum_summand. ff_h_ged_orientation_hidden_sum_summand + S (ff_a_ged_orientation_hidden_sum) = S ((S (ff_i_ged_orientation_hidden_sum)) * qc)) /\ exists ff_q_ged_orientation_hidden_sum_summand. qb = ff_q_ged_orientation_hidden_sum_summand * S ((S (ff_i_ged_orientation_hidden_sum)) * qc) + (ff_a_ged_orientation_hidden_sum))) /\ ((((exists ff_h_ged_orientation_hidden_sum_partial. ff_h_ged_orientation_hidden_sum_partial + S (ff_r_ged_orientation_hidden_sum) = S ((S (ff_i_ged_orientation_hidden_sum)) * ff_v_ged_orientation_hidden_sum)) /\ exists ff_q_ged_orientation_hidden_sum_partial. ff_u_ged_orientation_hidden_sum = ff_q_ged_orientation_hidden_sum_partial * S ((S (ff_i_ged_orientation_hidden_sum)) * ff_v_ged_orientation_hidden_sum) + (ff_r_ged_orientation_hidden_sum))) /\ ((((exists ff_h_ged_orientation_hidden_sum_successor. ff_h_ged_orientation_hidden_sum_successor + S (ff_s_ged_orientation_hidden_sum) = S ((S (S ff_i_ged_orientation_hidden_sum)) * ff_v_ged_orientation_hidden_sum)) /\ exists ff_q_ged_orientation_hidden_sum_successor. ff_u_ged_orientation_hidden_sum = ff_q_ged_orientation_hidden_sum_successor * S ((S (S ff_i_ged_orientation_hidden_sum)) * ff_v_ged_orientation_hidden_sum) + (ff_s_ged_orientation_hidden_sum))) /\ ff_s_ged_orientation_hidden_sum = ff_r_ged_orientation_hidden_sum + ff_a_ged_orientation_hidden_sum))))))))
  33. 0033specialize prime_scaled_half_quotient_sum_exists p
  34. 0034specialize prime_scaled_half_quotient_sum_exists h
  35. 0035specialize prime_scaled_half_quotient_sum_exists a
  36. 0036specialize prime_scaled_half_quotient_sum_exists x
  37. 0037specialize prime_scaled_half_quotient_sum_exists x1
  38. 0038apply prime_scaled_half_quotient_sum_exists
  39. 0039exact hpodd
  40. 0040exact hprime
  41. 0041exact hhalf_exists_witness_witness
  42. 0042cases hquotient
  43. 0043cases hquotient_witness
  44. 0044cases hquotient_witness_witness
  45. 0045cases hquotient_witness_witness_witness
  46. 0046cases hquotient_witness_witness_witness_witness
  47. 0047cases hquotient_witness_witness_witness_witness_witness
  48. 0048cases hquotient_witness_witness_witness_witness_witness_witness
  49. 0049cases hquotient_witness_witness_witness_witness_witness_witness_witness
  50. 0050cases hquotient_witness_witness_witness_witness_witness_witness_witness_right
  51. 0051have hquotient_mod_count : ModEq(2,x13,x2)
    Exact native replay linehave hquotient_mod_count : exists fspm_u_ged_orientation_hidden_quotient_mod_count fspm_v_ged_orientation_hidden_quotient_mod_count. (x13) + 2 * fspm_u_ged_orientation_hidden_quotient_mod_count = (x2) + 2 * fspm_v_ged_orientation_hidden_quotient_mod_count
  52. 0052specialize gauss_eisenstein_sign_count_mod_quotient_sum p
  53. 0053specialize gauss_eisenstein_sign_count_mod_quotient_sum h
  54. 0054specialize gauss_eisenstein_sign_count_mod_quotient_sum a
  55. 0055specialize gauss_eisenstein_sign_count_mod_quotient_sum x
  56. 0056specialize gauss_eisenstein_sign_count_mod_quotient_sum x1
  57. 0057specialize gauss_eisenstein_sign_count_mod_quotient_sum x7
  58. 0058specialize gauss_eisenstein_sign_count_mod_quotient_sum x8
  59. 0059specialize gauss_eisenstein_sign_count_mod_quotient_sum x9
  60. 0060specialize gauss_eisenstein_sign_count_mod_quotient_sum x10
  61. 0061specialize gauss_eisenstein_sign_count_mod_quotient_sum x11
  62. 0062specialize gauss_eisenstein_sign_count_mod_quotient_sum x12
  63. 0063specialize gauss_eisenstein_sign_count_mod_quotient_sum x3
  64. 0064specialize gauss_eisenstein_sign_count_mod_quotient_sum x4
  65. 0065specialize gauss_eisenstein_sign_count_mod_quotient_sum x5
  66. 0066specialize gauss_eisenstein_sign_count_mod_quotient_sum x6
  67. 0067specialize gauss_eisenstein_sign_count_mod_quotient_sum x13
  68. 0068specialize gauss_eisenstein_sign_count_mod_quotient_sum x2
  69. 0069apply gauss_eisenstein_sign_count_mod_quotient_sum
  70. 0070exact hpodd
  71. 0071exact haodd
  72. 0072exact hprime
  73. 0073exact hnotdiv
  74. 0074exact hhalf_exists_witness_witness
  75. 0075exact hquotient_witness_witness_witness_witness_witness_witness_witness_left
  76. 0076exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_left
  77. 0077exact hgauss_witness_left_witness_witness_witness_witness_left
  78. 0078exact hgauss_witness_left_witness_witness_witness_witness_right
  79. 0079exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_right
  80. 0080have hcount_mod_quotient : ModEq(2,x2,x13)
    Exact native replay linehave hcount_mod_quotient : exists fspm_u_ged_orientation_hidden_count_mod_quotient fspm_v_ged_orientation_hidden_count_mod_quotient. (x2) + 2 * fspm_u_ged_orientation_hidden_count_mod_quotient = (x13) + 2 * fspm_v_ged_orientation_hidden_count_mod_quotient
  81. 0081specialize mod_eq_symm 2
  82. 0082specialize mod_eq_symm x13
  83. 0083specialize mod_eq_symm x2
  84. 0084apply mod_eq_symm
  85. 0085exact hquotient_mod_count
  86. 0086exists x7
  87. 0087exists x8
  88. 0088exists x9
  89. 0089exists x10
  90. 0090exists x11
  91. 0091exists x12
  92. 0092exists x2
  93. 0093exists x13
  94. 0094split
  95. 0095exact hquotient_witness_witness_witness_witness_witness_witness_witness_left
  96. 0096split
  97. 0097exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_left
  98. 0098split
  99. 0099exact hquotient_witness_witness_witness_witness_witness_witness_witness_right_right
  100. 0100split
  101. 0101exact hgauss_witness_right
  102. 0102exact hcount_mod_quotient