PA00C0

prime_scaled_half_division_prefix_exists

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

An odd-prime half range has exact scaled quotient/remainder codes.

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. ((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)))))))

Structural proof guide

Generated structural guide

An odd-prime half range has exact scaled quotient/remainder codes.

Use the direct prerequisites beta_repeat_exists, beta_pointwise_mul_prefix_exists, beta_scaled_successor_prefix_from_pointwise, prime_nonzero, beta_division_prefix_exists as previously established PA formulas.

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

Referenced ingredients

PA0045 beta_repeat_exists PA007L beta_pointwise_mul_prefix_exists PA00BW beta_scaled_successor_prefix_from_pointwise PA0031 prime_nonzero PA00BY beta_division_prefix_exists

Proof neighborhood

Direct dependencies

PA0045 beta_repeat_exists PA007L beta_pointwise_mul_prefix_exists PA00BW beta_scaled_successor_prefix_from_pointwise PA0031 prime_nonzero PA00BY beta_division_prefix_exists

Direct dependents

PA00C1 prime_scaled_half_quotient_sum_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 hrepeat_exists : exists ab ac. (forall ff_i_eisenstein_repeat_exists. (exists ff_lt_eisenstein_repeat_exists_bound. ff_lt_eisenstein_repeat_exists_bound + S ff_i_eisenstein_repeat_exists = h) -> (((exists ff_h_eisenstein_repeat_exists_decoded. ff_h_eisenstein_repeat_exists_decoded + S (a) = S ((S (ff_i_eisenstein_repeat_exists)) * ac)) /\ exists ff_q_eisenstein_repeat_exists_decoded. ab = ff_q_eisenstein_repeat_exists_decoded * S ((S (ff_i_eisenstein_repeat_exists)) * ac) + (a))))
  10. 0010specialize beta_repeat_exists a
  11. 0011specialize beta_repeat_exists h
  12. 0012exact beta_repeat_exists
  13. 0013cases hrepeat_exists
  14. 0014cases hrepeat_exists_witness
  15. 0015have hpointwise_exists : exists tb tc. (forall fpmp_index_eisenstein_pointwise_exists fpmp_left_eisenstein_pointwise_exists fpmp_right_eisenstein_pointwise_exists fpmp_target_eisenstein_pointwise_exists. (exists fpmp_gap_eisenstein_pointwise_exists. fpmp_gap_eisenstein_pointwise_exists + S fpmp_index_eisenstein_pointwise_exists = h) -> (((exists ff_h_fpmp_eisenstein_pointwise_exists_left. ff_h_fpmp_eisenstein_pointwise_exists_left + S (fpmp_left_eisenstein_pointwise_exists) = S ((S (fpmp_index_eisenstein_pointwise_exists)) * x1)) /\ exists ff_q_fpmp_eisenstein_pointwise_exists_left. x = ff_q_fpmp_eisenstein_pointwise_exists_left * S ((S (fpmp_index_eisenstein_pointwise_exists)) * x1) + (fpmp_left_eisenstein_pointwise_exists))) -> (((exists ff_h_fpmp_eisenstein_pointwise_exists_right. ff_h_fpmp_eisenstein_pointwise_exists_right + S (fpmp_right_eisenstein_pointwise_exists) = S ((S (fpmp_index_eisenstein_pointwise_exists)) * c)) /\ exists ff_q_fpmp_eisenstein_pointwise_exists_right. b = ff_q_fpmp_eisenstein_pointwise_exists_right * S ((S (fpmp_index_eisenstein_pointwise_exists)) * c) + (fpmp_right_eisenstein_pointwise_exists))) -> (((exists ff_h_fpmp_eisenstein_pointwise_exists_target. ff_h_fpmp_eisenstein_pointwise_exists_target + S (fpmp_target_eisenstein_pointwise_exists) = S ((S (fpmp_index_eisenstein_pointwise_exists)) * tc)) /\ exists ff_q_fpmp_eisenstein_pointwise_exists_target. tb = ff_q_fpmp_eisenstein_pointwise_exists_target * S ((S (fpmp_index_eisenstein_pointwise_exists)) * tc) + (fpmp_target_eisenstein_pointwise_exists))) -> fpmp_target_eisenstein_pointwise_exists = fpmp_left_eisenstein_pointwise_exists * fpmp_right_eisenstein_pointwise_exists)
  16. 0016specialize beta_pointwise_mul_prefix_exists x
  17. 0017specialize beta_pointwise_mul_prefix_exists x1
  18. 0018specialize beta_pointwise_mul_prefix_exists b
  19. 0019specialize beta_pointwise_mul_prefix_exists c
  20. 0020specialize beta_pointwise_mul_prefix_exists h
  21. 0021exact beta_pointwise_mul_prefix_exists
  22. 0022cases hpointwise_exists
  23. 0023cases hpointwise_exists_witness
  24. 0024have hscaled : forall esd_index_eisenstein_local_exact esd_value_eisenstein_local_exact. (exists esd_gap_eisenstein_local_exact. esd_gap_eisenstein_local_exact + S esd_index_eisenstein_local_exact = h) -> (((exists ff_h_esd_eisenstein_local_exact_decoded. ff_h_esd_eisenstein_local_exact_decoded + S (esd_value_eisenstein_local_exact) = S ((S (esd_index_eisenstein_local_exact)) * x3)) /\ exists ff_q_esd_eisenstein_local_exact_decoded. x2 = ff_q_esd_eisenstein_local_exact_decoded * S ((S (esd_index_eisenstein_local_exact)) * x3) + (esd_value_eisenstein_local_exact))) -> esd_value_eisenstein_local_exact = a * (1 + esd_index_eisenstein_local_exact)
  25. 0025specialize beta_scaled_successor_prefix_from_pointwise a
  26. 0026specialize beta_scaled_successor_prefix_from_pointwise b
  27. 0027specialize beta_scaled_successor_prefix_from_pointwise c
  28. 0028specialize beta_scaled_successor_prefix_from_pointwise x
  29. 0029specialize beta_scaled_successor_prefix_from_pointwise x1
  30. 0030specialize beta_scaled_successor_prefix_from_pointwise x2
  31. 0031specialize beta_scaled_successor_prefix_from_pointwise x3
  32. 0032specialize beta_scaled_successor_prefix_from_pointwise h
  33. 0033apply beta_scaled_successor_prefix_from_pointwise
  34. 0034exact hhalf
  35. 0035exact hrepeat_exists_witness_witness
  36. 0036exact hpointwise_exists_witness_witness
  37. 0037have hp0 : ~(p = 0)
  38. 0038intro hpzero
  39. 0039specialize prime_nonzero p
  40. 0040apply prime_nonzero
  41. 0041exact hprime
  42. 0042exact hpzero
  43. 0043have hdivision_exists : exists qb qc rb rc. (forall fdp_index_eisenstein_division_exists. (exists gsp_lt_gap_eisenstein_division_exists_index_bound. gsp_lt_gap_eisenstein_division_exists_index_bound + S fdp_index_eisenstein_division_exists = h) -> exists fdp_value_eisenstein_division_exists fdp_quotient_eisenstein_division_exists fdp_remainder_eisenstein_division_exists. (((exists ff_h_fdp_eisenstein_division_exists_source. ff_h_fdp_eisenstein_division_exists_source + S (fdp_value_eisenstein_division_exists) = S ((S (fdp_index_eisenstein_division_exists)) * x3)) /\ exists ff_q_fdp_eisenstein_division_exists_source. x2 = ff_q_fdp_eisenstein_division_exists_source * S ((S (fdp_index_eisenstein_division_exists)) * x3) + (fdp_value_eisenstein_division_exists))) /\ ((((exists ff_h_fdp_eisenstein_division_exists_quotient_entry. ff_h_fdp_eisenstein_division_exists_quotient_entry + S (fdp_quotient_eisenstein_division_exists) = S ((S (fdp_index_eisenstein_division_exists)) * qc)) /\ exists ff_q_fdp_eisenstein_division_exists_quotient_entry. qb = ff_q_fdp_eisenstein_division_exists_quotient_entry * S ((S (fdp_index_eisenstein_division_exists)) * qc) + (fdp_quotient_eisenstein_division_exists))) /\ ((((exists ff_h_fdp_eisenstein_division_exists_remainder_entry. ff_h_fdp_eisenstein_division_exists_remainder_entry + S (fdp_remainder_eisenstein_division_exists) = S ((S (fdp_index_eisenstein_division_exists)) * rc)) /\ exists ff_q_fdp_eisenstein_division_exists_remainder_entry. rb = ff_q_fdp_eisenstein_division_exists_remainder_entry * S ((S (fdp_index_eisenstein_division_exists)) * rc) + (fdp_remainder_eisenstein_division_exists))) /\ (fdp_value_eisenstein_division_exists = p * fdp_quotient_eisenstein_division_exists + fdp_remainder_eisenstein_division_exists /\ (exists gsp_lt_gap_eisenstein_division_exists_remainder_bound. gsp_lt_gap_eisenstein_division_exists_remainder_bound + S fdp_remainder_eisenstein_division_exists = p)))))
  44. 0044specialize beta_division_prefix_exists p
  45. 0045specialize beta_division_prefix_exists x2
  46. 0046specialize beta_division_prefix_exists x3
  47. 0047specialize beta_division_prefix_exists h
  48. 0048apply beta_division_prefix_exists
  49. 0049exact hp0
  50. 0050cases hdivision_exists
  51. 0051cases hdivision_exists_witness
  52. 0052cases hdivision_exists_witness_witness
  53. 0053cases hdivision_exists_witness_witness_witness
  54. 0054exists x2
  55. 0055exists x3
  56. 0056exists x4
  57. 0057exists x5
  58. 0058exists x6
  59. 0059exists x7
  60. 0060split
  61. 0061exact hscaled
  62. 0062exact hdivision_exists_witness_witness_witness_witness