PA008J

prime_mul_residue_product_balance

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

Scaling the nonzero residues modulo a prime preserves their exact product modulo p.

Exact expanded PA statement

forall p n a b c F A. p = S n -> ((~(p = 1) /\ forall frm_prime_left_balance_prime frm_prime_right_balance_prime. p = frm_prime_left_balance_prime * frm_prime_right_balance_prime -> frm_prime_left_balance_prime = 1 \/ frm_prime_right_balance_prime = 1)) -> (~(exists frm_factor_balance_multiplier. a = p * frm_factor_balance_multiplier)) -> (forall ff_i_frp_range_balance_range. (exists ff_lt_frp_range_balance_range_bound. ff_lt_frp_range_balance_range_bound + S ff_i_frp_range_balance_range = n) -> (((exists ff_h_frp_range_balance_range_decoded. ff_h_frp_range_balance_range_decoded + S (1 + ff_i_frp_range_balance_range) = S ((S (ff_i_frp_range_balance_range)) * c)) /\ exists ff_q_frp_range_balance_range_decoded. b = ff_q_frp_range_balance_range_decoded * S ((S (ff_i_frp_range_balance_range)) * c) + (1 + ff_i_frp_range_balance_range)))) -> (exists ff_u_balance_source ff_v_balance_source. ((((exists ff_h_balance_source_start. ff_h_balance_source_start + S (1) = S ((S (0)) * ff_v_balance_source)) /\ exists ff_q_balance_source_start. ff_u_balance_source = ff_q_balance_source_start * S ((S (0)) * ff_v_balance_source) + (1))) /\ ((((exists ff_h_balance_source_terminal. ff_h_balance_source_terminal + S (F) = S ((S (n)) * ff_v_balance_source)) /\ exists ff_q_balance_source_terminal. ff_u_balance_source = ff_q_balance_source_terminal * S ((S (n)) * ff_v_balance_source) + (F))) /\ forall ff_i_balance_source. (exists ff_lt_balance_source_bound. ff_lt_balance_source_bound + S ff_i_balance_source = n) -> exists ff_p_balance_source ff_r_balance_source ff_s_balance_source. ((((exists ff_h_balance_source_factor. ff_h_balance_source_factor + S (ff_p_balance_source) = S ((S (ff_i_balance_source)) * c)) /\ exists ff_q_balance_source_factor. b = ff_q_balance_source_factor * S ((S (ff_i_balance_source)) * c) + (ff_p_balance_source))) /\ ((((exists ff_h_balance_source_partial. ff_h_balance_source_partial + S (ff_r_balance_source) = S ((S (ff_i_balance_source)) * ff_v_balance_source)) /\ exists ff_q_balance_source_partial. ff_u_balance_source = ff_q_balance_source_partial * S ((S (ff_i_balance_source)) * ff_v_balance_source) + (ff_r_balance_source))) /\ ((((exists ff_h_balance_source_successor. ff_h_balance_source_successor + S (ff_s_balance_source) = S ((S (S ff_i_balance_source)) * ff_v_balance_source)) /\ exists ff_q_balance_source_successor. ff_u_balance_source = ff_q_balance_source_successor * S ((S (S ff_i_balance_source)) * ff_v_balance_source) + (ff_s_balance_source))) /\ ff_s_balance_source = ff_r_balance_source * ff_p_balance_source)))))) -> (exists ff_b_balance_power ff_c_balance_power. ((forall ff_i_balance_power_repeat. (exists ff_lt_balance_power_repeat_bound. ff_lt_balance_power_repeat_bound + S ff_i_balance_power_repeat = n) -> (((exists ff_h_balance_power_repeat_decoded. ff_h_balance_power_repeat_decoded + S (a) = S ((S (ff_i_balance_power_repeat)) * ff_c_balance_power)) /\ exists ff_q_balance_power_repeat_decoded. ff_b_balance_power = ff_q_balance_power_repeat_decoded * S ((S (ff_i_balance_power_repeat)) * ff_c_balance_power) + (a)))) /\ (exists ff_u_balance_power_product ff_v_balance_power_product. ((((exists ff_h_balance_power_product_start. ff_h_balance_power_product_start + S (1) = S ((S (0)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_start. ff_u_balance_power_product = ff_q_balance_power_product_start * S ((S (0)) * ff_v_balance_power_product) + (1))) /\ ((((exists ff_h_balance_power_product_terminal. ff_h_balance_power_product_terminal + S (A) = S ((S (n)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_terminal. ff_u_balance_power_product = ff_q_balance_power_product_terminal * S ((S (n)) * ff_v_balance_power_product) + (A))) /\ forall ff_i_balance_power_product. (exists ff_lt_balance_power_product_bound. ff_lt_balance_power_product_bound + S ff_i_balance_power_product = n) -> exists ff_p_balance_power_product ff_r_balance_power_product ff_s_balance_power_product. ((((exists ff_h_balance_power_product_factor. ff_h_balance_power_product_factor + S (ff_p_balance_power_product) = S ((S (ff_i_balance_power_product)) * ff_c_balance_power)) /\ exists ff_q_balance_power_product_factor. ff_b_balance_power = ff_q_balance_power_product_factor * S ((S (ff_i_balance_power_product)) * ff_c_balance_power) + (ff_p_balance_power_product))) /\ ((((exists ff_h_balance_power_product_partial. ff_h_balance_power_product_partial + S (ff_r_balance_power_product) = S ((S (ff_i_balance_power_product)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_partial. ff_u_balance_power_product = ff_q_balance_power_product_partial * S ((S (ff_i_balance_power_product)) * ff_v_balance_power_product) + (ff_r_balance_power_product))) /\ ((((exists ff_h_balance_power_product_successor. ff_h_balance_power_product_successor + S (ff_s_balance_power_product) = S ((S (S ff_i_balance_power_product)) * ff_v_balance_power_product)) /\ exists ff_q_balance_power_product_successor. ff_u_balance_power_product = ff_q_balance_power_product_successor * S ((S (S ff_i_balance_power_product)) * ff_v_balance_power_product) + (ff_s_balance_power_product))) /\ ff_s_balance_power_product = ff_r_balance_power_product * ff_p_balance_power_product)))))))) -> (exists fsp_product_mod_left_balance_result fsp_product_mod_right_balance_result. (A * F) + p * fsp_product_mod_left_balance_result = F + p * fsp_product_mod_right_balance_result)

Structural proof guide

Generated structural guide

Scaling the nonzero residues modulo a prime preserves their exact product modulo p.

Use the direct prerequisites prime_mul_residue_reindex_exists, beta_product_pointwise_scale_mod, beta_product_exists, beta_product_permutation_invariant as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (4), equality transport (1).

Referenced ingredients

PA008I prime_mul_residue_reindex_exists PA007Q beta_product_pointwise_scale_mod PA003X beta_product_exists PA007X beta_product_permutation_invariant

Proof neighborhood

Direct dependencies

PA008I prime_mul_residue_reindex_exists PA007Q beta_product_pointwise_scale_mod PA003X beta_product_exists PA007X beta_product_permutation_invariant

Direct dependents

PA008L fermat_predecessor_exponent_mod_one

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 F
  7. 0007intro A
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro hnotdiv
  11. 0011intro hrange
  12. 0012intro hF
  13. 0013intro hA
  14. 0014have hreindex : exists fpb_map_code_balance_reindex fpb_map_scale_balance_reindex fpb_target_code_balance_reindex fpb_target_scale_balance_reindex. ((forall fp_i_fpb_balance_reindex_data_bounded. (exists fp_gap_fpb_balance_reindex_data_bounded_index. fp_gap_fpb_balance_reindex_data_bounded_index + S fp_i_fpb_balance_reindex_data_bounded = n) -> exists fp_value_fpb_balance_reindex_data_bounded. ((((exists ff_h_fpb_balance_reindex_data_bounded_entry. ff_h_fpb_balance_reindex_data_bounded_entry + S (fp_value_fpb_balance_reindex_data_bounded) = S ((S (fp_i_fpb_balance_reindex_data_bounded)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_bounded_entry. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_bounded_entry * S ((S (fp_i_fpb_balance_reindex_data_bounded)) * fpb_map_scale_balance_reindex) + (fp_value_fpb_balance_reindex_data_bounded))) /\ (exists fp_gap_fpb_balance_reindex_data_bounded_value. fp_gap_fpb_balance_reindex_data_bounded_value + S fp_value_fpb_balance_reindex_data_bounded = n))) /\ ((forall fp_i_fpb_balance_reindex_data_injective fp_j_fpb_balance_reindex_data_injective fp_value_fpb_balance_reindex_data_injective. (exists fp_gap_fpb_balance_reindex_data_injective_i. fp_gap_fpb_balance_reindex_data_injective_i + S fp_i_fpb_balance_reindex_data_injective = n) -> (exists fp_gap_fpb_balance_reindex_data_injective_j. fp_gap_fpb_balance_reindex_data_injective_j + S fp_j_fpb_balance_reindex_data_injective = n) -> (((exists ff_h_fpb_balance_reindex_data_injective_left. ff_h_fpb_balance_reindex_data_injective_left + S (fp_value_fpb_balance_reindex_data_injective) = S ((S (fp_i_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_injective_left. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_injective_left * S ((S (fp_i_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex) + (fp_value_fpb_balance_reindex_data_injective))) -> (((exists ff_h_fpb_balance_reindex_data_injective_right. ff_h_fpb_balance_reindex_data_injective_right + S (fp_value_fpb_balance_reindex_data_injective) = S ((S (fp_j_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_injective_right. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_injective_right * S ((S (fp_j_fpb_balance_reindex_data_injective)) * fpb_map_scale_balance_reindex) + (fp_value_fpb_balance_reindex_data_injective))) -> fp_i_fpb_balance_reindex_data_injective = fp_j_fpb_balance_reindex_data_injective) /\ ((forall fpr_i_fpb_balance_reindex_data_aligned fpr_j_fpb_balance_reindex_data_aligned fpr_x_fpb_balance_reindex_data_aligned. (exists fpr_h_fpb_balance_reindex_data_aligned. fpr_h_fpb_balance_reindex_data_aligned + S fpr_i_fpb_balance_reindex_data_aligned = n) -> (((exists ff_h_fpb_balance_reindex_data_aligned_map. ff_h_fpb_balance_reindex_data_aligned_map + S (fpr_j_fpb_balance_reindex_data_aligned) = S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_map_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_aligned_map. fpb_map_code_balance_reindex = ff_q_fpb_balance_reindex_data_aligned_map * S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_map_scale_balance_reindex) + (fpr_j_fpb_balance_reindex_data_aligned))) -> (((exists ff_h_fpb_balance_reindex_data_aligned_source. ff_h_fpb_balance_reindex_data_aligned_source + S (fpr_x_fpb_balance_reindex_data_aligned) = S ((S (fpr_j_fpb_balance_reindex_data_aligned)) * c)) /\ exists ff_q_fpb_balance_reindex_data_aligned_source. b = ff_q_fpb_balance_reindex_data_aligned_source * S ((S (fpr_j_fpb_balance_reindex_data_aligned)) * c) + (fpr_x_fpb_balance_reindex_data_aligned))) -> (((exists ff_h_fpb_balance_reindex_data_aligned_target. ff_h_fpb_balance_reindex_data_aligned_target + S (fpr_x_fpb_balance_reindex_data_aligned) = S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_target_scale_balance_reindex)) /\ exists ff_q_fpb_balance_reindex_data_aligned_target. fpb_target_code_balance_reindex = ff_q_fpb_balance_reindex_data_aligned_target * S ((S (fpr_i_fpb_balance_reindex_data_aligned)) * fpb_target_scale_balance_reindex) + (fpr_x_fpb_balance_reindex_data_aligned)))) /\ (forall fsp_index_fpb_balance_reindex_data_scaled fsp_source_fpb_balance_reindex_data_scaled fsp_target_fpb_balance_reindex_data_scaled. (exists fsp_gap_fpb_balance_reindex_data_scaled. fsp_gap_fpb_balance_reindex_data_scaled + S fsp_index_fpb_balance_reindex_data_scaled = n) -> (((exists fsp_source_height_fpb_balance_reindex_data_scaled. fsp_source_height_fpb_balance_reindex_data_scaled + S (fsp_source_fpb_balance_reindex_data_scaled) = S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * c)) /\ exists fsp_source_quotient_fpb_balance_reindex_data_scaled. b = fsp_source_quotient_fpb_balance_reindex_data_scaled * S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * c) + (fsp_source_fpb_balance_reindex_data_scaled))) -> (((exists fsp_target_height_fpb_balance_reindex_data_scaled. fsp_target_height_fpb_balance_reindex_data_scaled + S (fsp_target_fpb_balance_reindex_data_scaled) = S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * fpb_target_scale_balance_reindex)) /\ exists fsp_target_quotient_fpb_balance_reindex_data_scaled. fpb_target_code_balance_reindex = fsp_target_quotient_fpb_balance_reindex_data_scaled * S ((S (fsp_index_fpb_balance_reindex_data_scaled)) * fpb_target_scale_balance_reindex) + (fsp_target_fpb_balance_reindex_data_scaled))) -> (exists fsp_mod_left_fpb_balance_reindex_data_scaled fsp_mod_right_fpb_balance_reindex_data_scaled. a * fsp_source_fpb_balance_reindex_data_scaled + p * fsp_mod_left_fpb_balance_reindex_data_scaled = fsp_target_fpb_balance_reindex_data_scaled + p * fsp_mod_right_fpb_balance_reindex_data_scaled)))))
  15. 0015specialize prime_mul_residue_reindex_exists p
  16. 0016specialize prime_mul_residue_reindex_exists n
  17. 0017specialize prime_mul_residue_reindex_exists a
  18. 0018specialize prime_mul_residue_reindex_exists b
  19. 0019specialize prime_mul_residue_reindex_exists c
  20. 0020apply prime_mul_residue_reindex_exists
  21. 0021exact hpn
  22. 0022exact hp
  23. 0023exact hnotdiv
  24. 0024exact hrange
  25. 0025cases hreindex
  26. 0026cases hreindex_witness
  27. 0027cases hreindex_witness_witness
  28. 0028cases hreindex_witness_witness_witness
  29. 0029cases hreindex_witness_witness_witness_witness
  30. 0030cases hreindex_witness_witness_witness_witness_right
  31. 0031cases hreindex_witness_witness_witness_witness_right_right
  32. 0032have htarget_product_exists : exists Q. (exists ff_u_balance_target_exists ff_v_balance_target_exists. ((((exists ff_h_balance_target_exists_start. ff_h_balance_target_exists_start + S (1) = S ((S (0)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_start. ff_u_balance_target_exists = ff_q_balance_target_exists_start * S ((S (0)) * ff_v_balance_target_exists) + (1))) /\ ((((exists ff_h_balance_target_exists_terminal. ff_h_balance_target_exists_terminal + S (Q) = S ((S (n)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_terminal. ff_u_balance_target_exists = ff_q_balance_target_exists_terminal * S ((S (n)) * ff_v_balance_target_exists) + (Q))) /\ forall ff_i_balance_target_exists. (exists ff_lt_balance_target_exists_bound. ff_lt_balance_target_exists_bound + S ff_i_balance_target_exists = n) -> exists ff_p_balance_target_exists ff_r_balance_target_exists ff_s_balance_target_exists. ((((exists ff_h_balance_target_exists_factor. ff_h_balance_target_exists_factor + S (ff_p_balance_target_exists) = S ((S (ff_i_balance_target_exists)) * x3)) /\ exists ff_q_balance_target_exists_factor. x2 = ff_q_balance_target_exists_factor * S ((S (ff_i_balance_target_exists)) * x3) + (ff_p_balance_target_exists))) /\ ((((exists ff_h_balance_target_exists_partial. ff_h_balance_target_exists_partial + S (ff_r_balance_target_exists) = S ((S (ff_i_balance_target_exists)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_partial. ff_u_balance_target_exists = ff_q_balance_target_exists_partial * S ((S (ff_i_balance_target_exists)) * ff_v_balance_target_exists) + (ff_r_balance_target_exists))) /\ ((((exists ff_h_balance_target_exists_successor. ff_h_balance_target_exists_successor + S (ff_s_balance_target_exists) = S ((S (S ff_i_balance_target_exists)) * ff_v_balance_target_exists)) /\ exists ff_q_balance_target_exists_successor. ff_u_balance_target_exists = ff_q_balance_target_exists_successor * S ((S (S ff_i_balance_target_exists)) * ff_v_balance_target_exists) + (ff_s_balance_target_exists))) /\ ff_s_balance_target_exists = ff_r_balance_target_exists * ff_p_balance_target_exists))))))
  33. 0033specialize beta_product_exists x2
  34. 0034specialize beta_product_exists x3
  35. 0035specialize beta_product_exists n
  36. 0036exact beta_product_exists
  37. 0037cases htarget_product_exists
  38. 0038have hFQ : F = x4
  39. 0039specialize beta_product_permutation_invariant n
  40. 0040specialize beta_product_permutation_invariant x
  41. 0041specialize beta_product_permutation_invariant x1
  42. 0042specialize beta_product_permutation_invariant b
  43. 0043specialize beta_product_permutation_invariant c
  44. 0044specialize beta_product_permutation_invariant x2
  45. 0045specialize beta_product_permutation_invariant x3
  46. 0046specialize beta_product_permutation_invariant F
  47. 0047specialize beta_product_permutation_invariant x4
  48. 0048apply beta_product_permutation_invariant
  49. 0049exact hreindex_witness_witness_witness_witness_left
  50. 0050exact hreindex_witness_witness_witness_witness_right_left
  51. 0051exact hreindex_witness_witness_witness_witness_right_right_left
  52. 0052exact hF
  53. 0053exact htarget_product_exists_witness
  54. 0054have hscale : exists fsp_product_mod_left_balance_scaled_product fsp_product_mod_right_balance_scaled_product. (A * F) + p * fsp_product_mod_left_balance_scaled_product = x4 + p * fsp_product_mod_right_balance_scaled_product
  55. 0055specialize beta_product_pointwise_scale_mod p
  56. 0056specialize beta_product_pointwise_scale_mod a
  57. 0057specialize beta_product_pointwise_scale_mod b
  58. 0058specialize beta_product_pointwise_scale_mod c
  59. 0059specialize beta_product_pointwise_scale_mod x2
  60. 0060specialize beta_product_pointwise_scale_mod x3
  61. 0061specialize beta_product_pointwise_scale_mod n
  62. 0062specialize beta_product_pointwise_scale_mod F
  63. 0063specialize beta_product_pointwise_scale_mod x4
  64. 0064specialize beta_product_pointwise_scale_mod A
  65. 0065apply beta_product_pointwise_scale_mod
  66. 0066exact hreindex_witness_witness_witness_witness_right_right_right
  67. 0067exact hF
  68. 0068exact htarget_product_exists_witness
  69. 0069exact hA
  70. 0070rewrite <- hFQ at hscale
  71. 0071exact hscale