PA008I

prime_mul_residue_reindex_exists

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

A nonzero multiplier modulo a prime induces a beta-coded residue reindexing.

Exact expanded PA statement

forall p n a b c. p = S n -> ((~(p = 1) /\ forall frm_prime_left_package_prime frm_prime_right_package_prime. p = frm_prime_left_package_prime * frm_prime_right_package_prime -> frm_prime_left_package_prime = 1 \/ frm_prime_right_package_prime = 1)) -> (~(exists frm_factor_package_multiplier. a = p * frm_factor_package_multiplier)) -> (forall ff_i_frp_range_package_range. (exists ff_lt_frp_range_package_range_bound. ff_lt_frp_range_package_range_bound + S ff_i_frp_range_package_range = n) -> (((exists ff_h_frp_range_package_range_decoded. ff_h_frp_range_package_range_decoded + S (1 + ff_i_frp_range_package_range) = S ((S (ff_i_frp_range_package_range)) * c)) /\ exists ff_q_frp_range_package_range_decoded. b = ff_q_frp_range_package_range_decoded * S ((S (ff_i_frp_range_package_range)) * c) + (1 + ff_i_frp_range_package_range)))) -> exists r s z d. (forall fp_i_package_result_bounded. (exists fp_gap_package_result_bounded_index. fp_gap_package_result_bounded_index + S fp_i_package_result_bounded = n) -> exists fp_value_package_result_bounded. ((((exists ff_h_package_result_bounded_entry. ff_h_package_result_bounded_entry + S (fp_value_package_result_bounded) = S ((S (fp_i_package_result_bounded)) * s)) /\ exists ff_q_package_result_bounded_entry. r = ff_q_package_result_bounded_entry * S ((S (fp_i_package_result_bounded)) * s) + (fp_value_package_result_bounded))) /\ (exists fp_gap_package_result_bounded_value. fp_gap_package_result_bounded_value + S fp_value_package_result_bounded = n))) /\ ((forall fp_i_package_result_injective fp_j_package_result_injective fp_value_package_result_injective. (exists fp_gap_package_result_injective_i. fp_gap_package_result_injective_i + S fp_i_package_result_injective = n) -> (exists fp_gap_package_result_injective_j. fp_gap_package_result_injective_j + S fp_j_package_result_injective = n) -> (((exists ff_h_package_result_injective_left. ff_h_package_result_injective_left + S (fp_value_package_result_injective) = S ((S (fp_i_package_result_injective)) * s)) /\ exists ff_q_package_result_injective_left. r = ff_q_package_result_injective_left * S ((S (fp_i_package_result_injective)) * s) + (fp_value_package_result_injective))) -> (((exists ff_h_package_result_injective_right. ff_h_package_result_injective_right + S (fp_value_package_result_injective) = S ((S (fp_j_package_result_injective)) * s)) /\ exists ff_q_package_result_injective_right. r = ff_q_package_result_injective_right * S ((S (fp_j_package_result_injective)) * s) + (fp_value_package_result_injective))) -> fp_i_package_result_injective = fp_j_package_result_injective) /\ ((forall fpr_i_package_result_aligned fpr_j_package_result_aligned fpr_x_package_result_aligned. (exists fpr_h_package_result_aligned. fpr_h_package_result_aligned + S fpr_i_package_result_aligned = n) -> (((exists ff_h_package_result_aligned_map. ff_h_package_result_aligned_map + S (fpr_j_package_result_aligned) = S ((S (fpr_i_package_result_aligned)) * s)) /\ exists ff_q_package_result_aligned_map. r = ff_q_package_result_aligned_map * S ((S (fpr_i_package_result_aligned)) * s) + (fpr_j_package_result_aligned))) -> (((exists ff_h_package_result_aligned_source. ff_h_package_result_aligned_source + S (fpr_x_package_result_aligned) = S ((S (fpr_j_package_result_aligned)) * c)) /\ exists ff_q_package_result_aligned_source. b = ff_q_package_result_aligned_source * S ((S (fpr_j_package_result_aligned)) * c) + (fpr_x_package_result_aligned))) -> (((exists ff_h_package_result_aligned_target. ff_h_package_result_aligned_target + S (fpr_x_package_result_aligned) = S ((S (fpr_i_package_result_aligned)) * d)) /\ exists ff_q_package_result_aligned_target. z = ff_q_package_result_aligned_target * S ((S (fpr_i_package_result_aligned)) * d) + (fpr_x_package_result_aligned)))) /\ (forall fsp_index_package_result_scale fsp_source_package_result_scale fsp_target_package_result_scale. (exists fsp_gap_package_result_scale. fsp_gap_package_result_scale + S fsp_index_package_result_scale = n) -> (((exists fsp_source_height_package_result_scale. fsp_source_height_package_result_scale + S (fsp_source_package_result_scale) = S ((S (fsp_index_package_result_scale)) * c)) /\ exists fsp_source_quotient_package_result_scale. b = fsp_source_quotient_package_result_scale * S ((S (fsp_index_package_result_scale)) * c) + (fsp_source_package_result_scale))) -> (((exists fsp_target_height_package_result_scale. fsp_target_height_package_result_scale + S (fsp_target_package_result_scale) = S ((S (fsp_index_package_result_scale)) * d)) /\ exists fsp_target_quotient_package_result_scale. z = fsp_target_quotient_package_result_scale * S ((S (fsp_index_package_result_scale)) * d) + (fsp_target_package_result_scale))) -> (exists fsp_mod_left_package_result_scale fsp_mod_right_package_result_scale. a * fsp_source_package_result_scale + p * fsp_mod_left_package_result_scale = fsp_target_package_result_scale + p * fsp_mod_right_package_result_scale))))

Structural proof guide

Generated structural guide

A nonzero multiplier modulo a prime induces a beta-coded residue reindexing.

Use the direct prerequisites le_refl, prime_mul_index_map_exists_up_to, beta_successor_lift_exists, fermat_index_map_bounded, prime_mul_index_map_injective, beta_successor_range_reindex_aligned, beta_successor_range_scale_mod as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (6).

Referenced ingredients

PA001A le_refl PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008D fermat_index_map_bounded PA008E prime_mul_index_map_injective PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod

Proof neighborhood

Direct dependencies

PA001A le_refl PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008D fermat_index_map_bounded PA008E prime_mul_index_map_injective PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod

Direct dependents

PA008J prime_mul_residue_product_balance

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 n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotdiv
  9. 0009intro hrange
  10. 0010have hmaps : exists r s. (forall frm_index_package_map. (exists frm_gap_package_map_index_bound. frm_gap_package_map_index_bound + S frm_index_package_map = n) -> (exists frm_residue_package_map_result. (exists frm_gap_package_map_result_residue_bound. frm_gap_package_map_result_residue_bound + S frm_residue_package_map_result = n) /\ ((((exists ff_h_frm_package_map_result_decoded. ff_h_frm_package_map_result_decoded + S (frm_residue_package_map_result) = S ((S (frm_index_package_map)) * s)) /\ exists ff_q_frm_package_map_result_decoded. r = ff_q_frm_package_map_result_decoded * S ((S (frm_index_package_map)) * s) + (frm_residue_package_map_result))) /\ (exists frm_mod_left_package_map_result_congruence frm_mod_right_package_map_result_congruence. a * S frm_index_package_map + p * frm_mod_left_package_map_result_congruence = S frm_residue_package_map_result + p * frm_mod_right_package_map_result_congruence))))
  11. 0011specialize prime_mul_index_map_exists_up_to n
  12. 0012specialize prime_mul_index_map_exists_up_to n
  13. 0013specialize prime_mul_index_map_exists_up_to p
  14. 0014specialize prime_mul_index_map_exists_up_to a
  15. 0015apply prime_mul_index_map_exists_up_to
  16. 0016specialize le_refl n
  17. 0017exact le_refl
  18. 0018exact hpn
  19. 0019exact hp
  20. 0020exact hnotdiv
  21. 0021cases hmaps
  22. 0022cases hmaps_witness
  23. 0023have hlifts : exists z d. (forall frr_index_package_lift frr_value_package_lift. (exists frr_gap_package_lift. frr_gap_package_lift + S frr_index_package_lift = n) -> (((exists ff_h_frr_package_lift_source. ff_h_frr_package_lift_source + S (frr_value_package_lift) = S ((S (frr_index_package_lift)) * x1)) /\ exists ff_q_frr_package_lift_source. x = ff_q_frr_package_lift_source * S ((S (frr_index_package_lift)) * x1) + (frr_value_package_lift))) -> (((exists frm_height_frr_package_lift_target. frm_height_frr_package_lift_target + S (S frr_value_package_lift) = S ((S (frr_index_package_lift)) * d)) /\ exists frm_quotient_frr_package_lift_target. z = frm_quotient_frr_package_lift_target * S ((S (frr_index_package_lift)) * d) + (S frr_value_package_lift))))
  24. 0024specialize beta_successor_lift_exists x
  25. 0025specialize beta_successor_lift_exists x1
  26. 0026specialize beta_successor_lift_exists n
  27. 0027exact beta_successor_lift_exists
  28. 0028cases hlifts
  29. 0029cases hlifts_witness
  30. 0030have hbounded : forall fp_i_package_bounded. (exists fp_gap_package_bounded_index. fp_gap_package_bounded_index + S fp_i_package_bounded = n) -> exists fp_value_package_bounded. ((((exists ff_h_package_bounded_entry. ff_h_package_bounded_entry + S (fp_value_package_bounded) = S ((S (fp_i_package_bounded)) * x1)) /\ exists ff_q_package_bounded_entry. x = ff_q_package_bounded_entry * S ((S (fp_i_package_bounded)) * x1) + (fp_value_package_bounded))) /\ (exists fp_gap_package_bounded_value. fp_gap_package_bounded_value + S fp_value_package_bounded = n))
  31. 0031specialize fermat_index_map_bounded x
  32. 0032specialize fermat_index_map_bounded x1
  33. 0033specialize fermat_index_map_bounded n
  34. 0034specialize fermat_index_map_bounded p
  35. 0035specialize fermat_index_map_bounded a
  36. 0036apply fermat_index_map_bounded
  37. 0037exact hmaps_witness_witness
  38. 0038have hinjective : forall fp_i_package_injective fp_j_package_injective fp_value_package_injective. (exists fp_gap_package_injective_i. fp_gap_package_injective_i + S fp_i_package_injective = n) -> (exists fp_gap_package_injective_j. fp_gap_package_injective_j + S fp_j_package_injective = n) -> (((exists ff_h_package_injective_left. ff_h_package_injective_left + S (fp_value_package_injective) = S ((S (fp_i_package_injective)) * x1)) /\ exists ff_q_package_injective_left. x = ff_q_package_injective_left * S ((S (fp_i_package_injective)) * x1) + (fp_value_package_injective))) -> (((exists ff_h_package_injective_right. ff_h_package_injective_right + S (fp_value_package_injective) = S ((S (fp_j_package_injective)) * x1)) /\ exists ff_q_package_injective_right. x = ff_q_package_injective_right * S ((S (fp_j_package_injective)) * x1) + (fp_value_package_injective))) -> fp_i_package_injective = fp_j_package_injective
  39. 0039specialize prime_mul_index_map_injective p
  40. 0040specialize prime_mul_index_map_injective n
  41. 0041specialize prime_mul_index_map_injective a
  42. 0042specialize prime_mul_index_map_injective x
  43. 0043specialize prime_mul_index_map_injective x1
  44. 0044apply prime_mul_index_map_injective
  45. 0045exact hpn
  46. 0046exact hp
  47. 0047exact hnotdiv
  48. 0048exact hmaps_witness_witness
  49. 0049have haligned : forall fpr_i_package_aligned fpr_j_package_aligned fpr_x_package_aligned. (exists fpr_h_package_aligned. fpr_h_package_aligned + S fpr_i_package_aligned = n) -> (((exists ff_h_package_aligned_map. ff_h_package_aligned_map + S (fpr_j_package_aligned) = S ((S (fpr_i_package_aligned)) * x1)) /\ exists ff_q_package_aligned_map. x = ff_q_package_aligned_map * S ((S (fpr_i_package_aligned)) * x1) + (fpr_j_package_aligned))) -> (((exists ff_h_package_aligned_source. ff_h_package_aligned_source + S (fpr_x_package_aligned) = S ((S (fpr_j_package_aligned)) * c)) /\ exists ff_q_package_aligned_source. b = ff_q_package_aligned_source * S ((S (fpr_j_package_aligned)) * c) + (fpr_x_package_aligned))) -> (((exists ff_h_package_aligned_target. ff_h_package_aligned_target + S (fpr_x_package_aligned) = S ((S (fpr_i_package_aligned)) * x3)) /\ exists ff_q_package_aligned_target. x2 = ff_q_package_aligned_target * S ((S (fpr_i_package_aligned)) * x3) + (fpr_x_package_aligned)))
  50. 0050specialize beta_successor_range_reindex_aligned x
  51. 0051specialize beta_successor_range_reindex_aligned x1
  52. 0052specialize beta_successor_range_reindex_aligned b
  53. 0053specialize beta_successor_range_reindex_aligned c
  54. 0054specialize beta_successor_range_reindex_aligned x2
  55. 0055specialize beta_successor_range_reindex_aligned x3
  56. 0056specialize beta_successor_range_reindex_aligned n
  57. 0057apply beta_successor_range_reindex_aligned
  58. 0058exact hbounded
  59. 0059exact hrange
  60. 0060exact hlifts_witness_witness
  61. 0061have hscale : forall fsp_index_package_scale fsp_source_package_scale fsp_target_package_scale. (exists fsp_gap_package_scale. fsp_gap_package_scale + S fsp_index_package_scale = n) -> (((exists fsp_source_height_package_scale. fsp_source_height_package_scale + S (fsp_source_package_scale) = S ((S (fsp_index_package_scale)) * c)) /\ exists fsp_source_quotient_package_scale. b = fsp_source_quotient_package_scale * S ((S (fsp_index_package_scale)) * c) + (fsp_source_package_scale))) -> (((exists fsp_target_height_package_scale. fsp_target_height_package_scale + S (fsp_target_package_scale) = S ((S (fsp_index_package_scale)) * x3)) /\ exists fsp_target_quotient_package_scale. x2 = fsp_target_quotient_package_scale * S ((S (fsp_index_package_scale)) * x3) + (fsp_target_package_scale))) -> (exists fsp_mod_left_package_scale fsp_mod_right_package_scale. a * fsp_source_package_scale + p * fsp_mod_left_package_scale = fsp_target_package_scale + p * fsp_mod_right_package_scale)
  62. 0062specialize beta_successor_range_scale_mod p
  63. 0063specialize beta_successor_range_scale_mod n
  64. 0064specialize beta_successor_range_scale_mod a
  65. 0065specialize beta_successor_range_scale_mod x
  66. 0066specialize beta_successor_range_scale_mod x1
  67. 0067specialize beta_successor_range_scale_mod b
  68. 0068specialize beta_successor_range_scale_mod c
  69. 0069specialize beta_successor_range_scale_mod x2
  70. 0070specialize beta_successor_range_scale_mod x3
  71. 0071apply beta_successor_range_scale_mod
  72. 0072exact hmaps_witness_witness
  73. 0073exact hrange
  74. 0074exact hlifts_witness_witness
  75. 0075exists x
  76. 0076exists x1
  77. 0077exists x2
  78. 0078exists x3
  79. 0079split
  80. 0080exact hbounded
  81. 0081split
  82. 0082exact hinjective
  83. 0083split
  84. 0084exact haligned
  85. 0085exact hscale