PA00C1

prime_scaled_half_quotient_sum_exists

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

The quotient code additionally carries its native finite floor sum.

Exact expanded PA statement

forall p h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall frp_prime_left_eisenstein_division_prime frp_prime_right_eisenstein_division_prime. p = frp_prime_left_eisenstein_division_prime * frp_prime_right_eisenstein_division_prime -> frp_prime_left_eisenstein_division_prime = 1 \/ frp_prime_right_eisenstein_division_prime = 1)) -> (forall gsp_range_index_eisenstein_scaled_half_range. (exists gsp_lt_gap_eisenstein_scaled_half_range_range_bound. gsp_lt_gap_eisenstein_scaled_half_range_range_bound + S gsp_range_index_eisenstein_scaled_half_range = h) -> (((exists gsp_beta_height_eisenstein_scaled_half_range_range_entry. gsp_beta_height_eisenstein_scaled_half_range_range_entry + S (1 + gsp_range_index_eisenstein_scaled_half_range) = S ((S (gsp_range_index_eisenstein_scaled_half_range)) * c)) /\ exists gsp_beta_quotient_eisenstein_scaled_half_range_range_entry. b = gsp_beta_quotient_eisenstein_scaled_half_range_range_entry * S ((S (gsp_range_index_eisenstein_scaled_half_range)) * c) + (1 + gsp_range_index_eisenstein_scaled_half_range)))) -> (exists tb tc qb qc rb rc Q. ((forall esd_index_eisenstein_scaled_exact esd_value_eisenstein_scaled_exact. (exists esd_gap_eisenstein_scaled_exact. esd_gap_eisenstein_scaled_exact + S esd_index_eisenstein_scaled_exact = h) -> (((exists ff_h_esd_eisenstein_scaled_exact_decoded. ff_h_esd_eisenstein_scaled_exact_decoded + S (esd_value_eisenstein_scaled_exact) = S ((S (esd_index_eisenstein_scaled_exact)) * tc)) /\ exists ff_q_esd_eisenstein_scaled_exact_decoded. tb = ff_q_esd_eisenstein_scaled_exact_decoded * S ((S (esd_index_eisenstein_scaled_exact)) * tc) + (esd_value_eisenstein_scaled_exact))) -> esd_value_eisenstein_scaled_exact = a * (1 + esd_index_eisenstein_scaled_exact)) /\ ((forall fdp_index_eisenstein_division_prefix. (exists gsp_lt_gap_eisenstein_division_prefix_index_bound. gsp_lt_gap_eisenstein_division_prefix_index_bound + S fdp_index_eisenstein_division_prefix = h) -> exists fdp_value_eisenstein_division_prefix fdp_quotient_eisenstein_division_prefix fdp_remainder_eisenstein_division_prefix. (((exists ff_h_fdp_eisenstein_division_prefix_source. ff_h_fdp_eisenstein_division_prefix_source + S (fdp_value_eisenstein_division_prefix) = S ((S (fdp_index_eisenstein_division_prefix)) * tc)) /\ exists ff_q_fdp_eisenstein_division_prefix_source. tb = ff_q_fdp_eisenstein_division_prefix_source * S ((S (fdp_index_eisenstein_division_prefix)) * tc) + (fdp_value_eisenstein_division_prefix))) /\ ((((exists ff_h_fdp_eisenstein_division_prefix_quotient_entry. ff_h_fdp_eisenstein_division_prefix_quotient_entry + S (fdp_quotient_eisenstein_division_prefix) = S ((S (fdp_index_eisenstein_division_prefix)) * qc)) /\ exists ff_q_fdp_eisenstein_division_prefix_quotient_entry. qb = ff_q_fdp_eisenstein_division_prefix_quotient_entry * S ((S (fdp_index_eisenstein_division_prefix)) * qc) + (fdp_quotient_eisenstein_division_prefix))) /\ ((((exists ff_h_fdp_eisenstein_division_prefix_remainder_entry. ff_h_fdp_eisenstein_division_prefix_remainder_entry + S (fdp_remainder_eisenstein_division_prefix) = S ((S (fdp_index_eisenstein_division_prefix)) * rc)) /\ exists ff_q_fdp_eisenstein_division_prefix_remainder_entry. rb = ff_q_fdp_eisenstein_division_prefix_remainder_entry * S ((S (fdp_index_eisenstein_division_prefix)) * rc) + (fdp_remainder_eisenstein_division_prefix))) /\ (fdp_value_eisenstein_division_prefix = p * fdp_quotient_eisenstein_division_prefix + fdp_remainder_eisenstein_division_prefix /\ (exists gsp_lt_gap_eisenstein_division_prefix_remainder_bound. gsp_lt_gap_eisenstein_division_prefix_remainder_bound + S fdp_remainder_eisenstein_division_prefix = p))))) /\ (exists ff_u_eisenstein_quotient_sum ff_v_eisenstein_quotient_sum. ((((exists ff_h_eisenstein_quotient_sum_start. ff_h_eisenstein_quotient_sum_start + S (0) = S ((S (0)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_start. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_start * S ((S (0)) * ff_v_eisenstein_quotient_sum) + (0))) /\ ((((exists ff_h_eisenstein_quotient_sum_terminal. ff_h_eisenstein_quotient_sum_terminal + S (Q) = S ((S (h)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_terminal. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_terminal * S ((S (h)) * ff_v_eisenstein_quotient_sum) + (Q))) /\ forall ff_i_eisenstein_quotient_sum. (exists ff_lt_eisenstein_quotient_sum_bound. ff_lt_eisenstein_quotient_sum_bound + S ff_i_eisenstein_quotient_sum = h) -> exists ff_a_eisenstein_quotient_sum ff_r_eisenstein_quotient_sum ff_s_eisenstein_quotient_sum. ((((exists ff_h_eisenstein_quotient_sum_summand. ff_h_eisenstein_quotient_sum_summand + S (ff_a_eisenstein_quotient_sum) = S ((S (ff_i_eisenstein_quotient_sum)) * qc)) /\ exists ff_q_eisenstein_quotient_sum_summand. qb = ff_q_eisenstein_quotient_sum_summand * S ((S (ff_i_eisenstein_quotient_sum)) * qc) + (ff_a_eisenstein_quotient_sum))) /\ ((((exists ff_h_eisenstein_quotient_sum_partial. ff_h_eisenstein_quotient_sum_partial + S (ff_r_eisenstein_quotient_sum) = S ((S (ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_partial. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_partial * S ((S (ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum) + (ff_r_eisenstein_quotient_sum))) /\ ((((exists ff_h_eisenstein_quotient_sum_successor. ff_h_eisenstein_quotient_sum_successor + S (ff_s_eisenstein_quotient_sum) = S ((S (S ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_successor. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_successor * S ((S (S ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum) + (ff_s_eisenstein_quotient_sum))) /\ ff_s_eisenstein_quotient_sum = ff_r_eisenstein_quotient_sum + ff_a_eisenstein_quotient_sum)))))))))

Structural proof guide

Generated structural guide

The quotient code additionally carries its native finite floor sum.

Use the direct prerequisites prime_scaled_half_division_prefix_exists, beta_sum_exists as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (2).

Referenced ingredients

PA00C0 prime_scaled_half_division_prefix_exists PA003H beta_sum_exists

Proof neighborhood

Direct dependencies

PA00C0 prime_scaled_half_division_prefix_exists PA003H beta_sum_exists

Direct dependents

PA00D7 odd_prime_gauss_eisenstein_orientation_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 b
  5. 0005intro c
  6. 0006intro hpodd
  7. 0007intro hprime
  8. 0008intro hhalf
  9. 0009have hdivision : exists tb tc qb qc rb rc. ((forall esd_index_eisenstein_local_package_scaled esd_value_eisenstein_local_package_scaled. (exists esd_gap_eisenstein_local_package_scaled. esd_gap_eisenstein_local_package_scaled + S esd_index_eisenstein_local_package_scaled = h) -> (((exists ff_h_esd_eisenstein_local_package_scaled_decoded. ff_h_esd_eisenstein_local_package_scaled_decoded + S (esd_value_eisenstein_local_package_scaled) = S ((S (esd_index_eisenstein_local_package_scaled)) * tc)) /\ exists ff_q_esd_eisenstein_local_package_scaled_decoded. tb = ff_q_esd_eisenstein_local_package_scaled_decoded * S ((S (esd_index_eisenstein_local_package_scaled)) * tc) + (esd_value_eisenstein_local_package_scaled))) -> esd_value_eisenstein_local_package_scaled = a * (1 + esd_index_eisenstein_local_package_scaled)) /\ (forall fdp_index_eisenstein_local_package_division. (exists gsp_lt_gap_eisenstein_local_package_division_index_bound. gsp_lt_gap_eisenstein_local_package_division_index_bound + S fdp_index_eisenstein_local_package_division = h) -> exists fdp_value_eisenstein_local_package_division fdp_quotient_eisenstein_local_package_division fdp_remainder_eisenstein_local_package_division. (((exists ff_h_fdp_eisenstein_local_package_division_source. ff_h_fdp_eisenstein_local_package_division_source + S (fdp_value_eisenstein_local_package_division) = S ((S (fdp_index_eisenstein_local_package_division)) * tc)) /\ exists ff_q_fdp_eisenstein_local_package_division_source. tb = ff_q_fdp_eisenstein_local_package_division_source * S ((S (fdp_index_eisenstein_local_package_division)) * tc) + (fdp_value_eisenstein_local_package_division))) /\ ((((exists ff_h_fdp_eisenstein_local_package_division_quotient_entry. ff_h_fdp_eisenstein_local_package_division_quotient_entry + S (fdp_quotient_eisenstein_local_package_division) = S ((S (fdp_index_eisenstein_local_package_division)) * qc)) /\ exists ff_q_fdp_eisenstein_local_package_division_quotient_entry. qb = ff_q_fdp_eisenstein_local_package_division_quotient_entry * S ((S (fdp_index_eisenstein_local_package_division)) * qc) + (fdp_quotient_eisenstein_local_package_division))) /\ ((((exists ff_h_fdp_eisenstein_local_package_division_remainder_entry. ff_h_fdp_eisenstein_local_package_division_remainder_entry + S (fdp_remainder_eisenstein_local_package_division) = S ((S (fdp_index_eisenstein_local_package_division)) * rc)) /\ exists ff_q_fdp_eisenstein_local_package_division_remainder_entry. rb = ff_q_fdp_eisenstein_local_package_division_remainder_entry * S ((S (fdp_index_eisenstein_local_package_division)) * rc) + (fdp_remainder_eisenstein_local_package_division))) /\ (fdp_value_eisenstein_local_package_division = p * fdp_quotient_eisenstein_local_package_division + fdp_remainder_eisenstein_local_package_division /\ (exists gsp_lt_gap_eisenstein_local_package_division_remainder_bound. gsp_lt_gap_eisenstein_local_package_division_remainder_bound + S fdp_remainder_eisenstein_local_package_division = p))))))
  10. 0010specialize prime_scaled_half_division_prefix_exists p
  11. 0011specialize prime_scaled_half_division_prefix_exists h
  12. 0012specialize prime_scaled_half_division_prefix_exists a
  13. 0013specialize prime_scaled_half_division_prefix_exists b
  14. 0014specialize prime_scaled_half_division_prefix_exists c
  15. 0015apply prime_scaled_half_division_prefix_exists
  16. 0016exact hpodd
  17. 0017exact hprime
  18. 0018exact hhalf
  19. 0019cases hdivision
  20. 0020cases hdivision_witness
  21. 0021cases hdivision_witness_witness
  22. 0022cases hdivision_witness_witness_witness
  23. 0023cases hdivision_witness_witness_witness_witness
  24. 0024cases hdivision_witness_witness_witness_witness_witness
  25. 0025cases hdivision_witness_witness_witness_witness_witness_witness
  26. 0026have hsum_exists : exists Q. (exists ff_u_eisenstein_local_sum_exists ff_v_eisenstein_local_sum_exists. ((((exists ff_h_eisenstein_local_sum_exists_start. ff_h_eisenstein_local_sum_exists_start + S (0) = S ((S (0)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_start. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_start * S ((S (0)) * ff_v_eisenstein_local_sum_exists) + (0))) /\ ((((exists ff_h_eisenstein_local_sum_exists_terminal. ff_h_eisenstein_local_sum_exists_terminal + S (Q) = S ((S (h)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_terminal. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_terminal * S ((S (h)) * ff_v_eisenstein_local_sum_exists) + (Q))) /\ forall ff_i_eisenstein_local_sum_exists. (exists ff_lt_eisenstein_local_sum_exists_bound. ff_lt_eisenstein_local_sum_exists_bound + S ff_i_eisenstein_local_sum_exists = h) -> exists ff_a_eisenstein_local_sum_exists ff_r_eisenstein_local_sum_exists ff_s_eisenstein_local_sum_exists. ((((exists ff_h_eisenstein_local_sum_exists_summand. ff_h_eisenstein_local_sum_exists_summand + S (ff_a_eisenstein_local_sum_exists) = S ((S (ff_i_eisenstein_local_sum_exists)) * x3)) /\ exists ff_q_eisenstein_local_sum_exists_summand. x2 = ff_q_eisenstein_local_sum_exists_summand * S ((S (ff_i_eisenstein_local_sum_exists)) * x3) + (ff_a_eisenstein_local_sum_exists))) /\ ((((exists ff_h_eisenstein_local_sum_exists_partial. ff_h_eisenstein_local_sum_exists_partial + S (ff_r_eisenstein_local_sum_exists) = S ((S (ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_partial. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_partial * S ((S (ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists) + (ff_r_eisenstein_local_sum_exists))) /\ ((((exists ff_h_eisenstein_local_sum_exists_successor. ff_h_eisenstein_local_sum_exists_successor + S (ff_s_eisenstein_local_sum_exists) = S ((S (S ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_successor. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_successor * S ((S (S ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists) + (ff_s_eisenstein_local_sum_exists))) /\ ff_s_eisenstein_local_sum_exists = ff_r_eisenstein_local_sum_exists + ff_a_eisenstein_local_sum_exists))))))
  27. 0027specialize beta_sum_exists x2
  28. 0028specialize beta_sum_exists x3
  29. 0029specialize beta_sum_exists h
  30. 0030exact beta_sum_exists
  31. 0031cases hsum_exists
  32. 0032exists x
  33. 0033exists x1
  34. 0034exists x2
  35. 0035exists x3
  36. 0036exists x4
  37. 0037exists x5
  38. 0038exists x6
  39. 0039split
  40. 0040exact hdivision_witness_witness_witness_witness_witness_witness_left
  41. 0041split
  42. 0042exact hdivision_witness_witness_witness_witness_witness_witness_right
  43. 0043exact hsum_exists_witness