PA00D7

odd_prime_gauss_eisenstein_orientation_data_exists

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

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

Exact expanded 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))))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_range_exists, arbitrary_gauss_lemma_complete, prime_scaled_half_quotient_sum_exists, gauss_eisenstein_sign_count_mod_quotient_sum, mod_eq_symm as previously established PA formulas.

The proof proceeds by case analysis (18), intermediate claims (5).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA00FG distinct_odd_primes_gauss_eisenstein_data_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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 : 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 : 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 : 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 : 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 : 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