PA00D0

gauss_signed_half_magnitude_sum_equals_half_sum

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

Gauss signed-half data makes the magnitude Sum equal the canonical half Sum.

Exact expanded PA statement

forall p h a b c mb mc sb sc X M. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_ges_prime gsp_prime_right_ges_prime. p = gsp_prime_left_ges_prime * gsp_prime_right_ges_prime -> gsp_prime_left_ges_prime = 1 \/ gsp_prime_right_ges_prime = 1)) -> (~(exists gsp_divisor_factor_ges_nondivisor. a = p * gsp_divisor_factor_ges_nondivisor)) -> (forall gsp_range_index_ges_half. (exists gsp_lt_gap_ges_half_range_bound. gsp_lt_gap_ges_half_range_bound + S gsp_range_index_ges_half = h) -> (((exists gsp_beta_height_ges_half_range_entry. gsp_beta_height_ges_half_range_entry + S (1 + gsp_range_index_ges_half) = S ((S (gsp_range_index_ges_half)) * c)) /\ exists gsp_beta_quotient_ges_half_range_entry. b = gsp_beta_quotient_ges_half_range_entry * S ((S (gsp_range_index_ges_half)) * c) + (1 + gsp_range_index_ges_half)))) -> (forall gsp_index_ges_signed. (exists gsp_lt_gap_ges_signed_index_bound. gsp_lt_gap_ges_signed_index_bound + S gsp_index_ges_signed = h) -> (exists gsp_value_ges_signed_entry gsp_magnitude_ges_signed_entry gsp_sign_ges_signed_entry. (((exists ff_h_gsp_ges_signed_entry_source. ff_h_gsp_ges_signed_entry_source + S (gsp_value_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * c)) /\ exists ff_q_gsp_ges_signed_entry_source. b = ff_q_gsp_ges_signed_entry_source * S ((S (gsp_index_ges_signed)) * c) + (gsp_value_ges_signed_entry))) /\ ((((exists ff_h_gsp_ges_signed_entry_magnitude. ff_h_gsp_ges_signed_entry_magnitude + S (gsp_magnitude_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * mc)) /\ exists ff_q_gsp_ges_signed_entry_magnitude. mb = ff_q_gsp_ges_signed_entry_magnitude * S ((S (gsp_index_ges_signed)) * mc) + (gsp_magnitude_ges_signed_entry))) /\ ((((exists ff_h_gsp_ges_signed_entry_sign. ff_h_gsp_ges_signed_entry_sign + S (gsp_sign_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * sc)) /\ exists ff_q_gsp_ges_signed_entry_sign. sb = ff_q_gsp_ges_signed_entry_sign * S ((S (gsp_index_ges_signed)) * sc) + (gsp_sign_ges_signed_entry))) /\ ((exists gsp_lt_gap_ges_signed_entry_positive. gsp_lt_gap_ges_signed_entry_positive + S 0 = gsp_magnitude_ges_signed_entry) /\ ((exists gsp_le_gap_ges_signed_entry_bounded. gsp_le_gap_ges_signed_entry_bounded + gsp_magnitude_ges_signed_entry = h) /\ ((gsp_sign_ges_signed_entry = 0 \/ gsp_sign_ges_signed_entry = 1) /\ (((gsp_sign_ges_signed_entry = 0 /\ (exists gsp_mod_left_ges_signed_entry_lower gsp_mod_right_ges_signed_entry_lower. (a * gsp_value_ges_signed_entry) + p * gsp_mod_left_ges_signed_entry_lower = (gsp_magnitude_ges_signed_entry) + p * gsp_mod_right_ges_signed_entry_lower)) \/ (gsp_sign_ges_signed_entry = 1 /\ (exists gsp_mod_left_ges_signed_entry_reflected gsp_mod_right_ges_signed_entry_reflected. (a * gsp_value_ges_signed_entry) + p * gsp_mod_left_ges_signed_entry_reflected = ((2 * h) * gsp_magnitude_ges_signed_entry) + p * gsp_mod_right_ges_signed_entry_reflected))))))))))) -> (exists ff_u_ges_half_sum ff_v_ges_half_sum. ((((exists ff_h_ges_half_sum_start. ff_h_ges_half_sum_start + S (0) = S ((S (0)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_start. ff_u_ges_half_sum = ff_q_ges_half_sum_start * S ((S (0)) * ff_v_ges_half_sum) + (0))) /\ ((((exists ff_h_ges_half_sum_terminal. ff_h_ges_half_sum_terminal + S (X) = S ((S (h)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_terminal. ff_u_ges_half_sum = ff_q_ges_half_sum_terminal * S ((S (h)) * ff_v_ges_half_sum) + (X))) /\ forall ff_i_ges_half_sum. (exists ff_lt_ges_half_sum_bound. ff_lt_ges_half_sum_bound + S ff_i_ges_half_sum = h) -> exists ff_a_ges_half_sum ff_r_ges_half_sum ff_s_ges_half_sum. ((((exists ff_h_ges_half_sum_summand. ff_h_ges_half_sum_summand + S (ff_a_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * c)) /\ exists ff_q_ges_half_sum_summand. b = ff_q_ges_half_sum_summand * S ((S (ff_i_ges_half_sum)) * c) + (ff_a_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_partial. ff_h_ges_half_sum_partial + S (ff_r_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_partial. ff_u_ges_half_sum = ff_q_ges_half_sum_partial * S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_r_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_successor. ff_h_ges_half_sum_successor + S (ff_s_ges_half_sum) = S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_successor. ff_u_ges_half_sum = ff_q_ges_half_sum_successor * S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_s_ges_half_sum))) /\ ff_s_ges_half_sum = ff_r_ges_half_sum + ff_a_ges_half_sum)))))) -> (exists ff_u_ges_magnitude_sum ff_v_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_start. ff_h_ges_magnitude_sum_start + S (0) = S ((S (0)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_start. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_start * S ((S (0)) * ff_v_ges_magnitude_sum) + (0))) /\ ((((exists ff_h_ges_magnitude_sum_terminal. ff_h_ges_magnitude_sum_terminal + S (M) = S ((S (h)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_terminal. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_terminal * S ((S (h)) * ff_v_ges_magnitude_sum) + (M))) /\ forall ff_i_ges_magnitude_sum. (exists ff_lt_ges_magnitude_sum_bound. ff_lt_ges_magnitude_sum_bound + S ff_i_ges_magnitude_sum = h) -> exists ff_a_ges_magnitude_sum ff_r_ges_magnitude_sum ff_s_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_summand. ff_h_ges_magnitude_sum_summand + S (ff_a_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * mc)) /\ exists ff_q_ges_magnitude_sum_summand. mb = ff_q_ges_magnitude_sum_summand * S ((S (ff_i_ges_magnitude_sum)) * mc) + (ff_a_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_partial. ff_h_ges_magnitude_sum_partial + S (ff_r_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_partial. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_partial * S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_r_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_successor. ff_h_ges_magnitude_sum_successor + S (ff_s_ges_magnitude_sum) = S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_successor. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_successor * S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_s_ges_magnitude_sum))) /\ ff_s_ges_magnitude_sum = ff_r_ges_magnitude_sum + ff_a_ges_magnitude_sum)))))) -> X = M

Structural proof guide

Generated structural guide

Gauss signed-half data makes the magnitude Sum equal the canonical half Sum.

Use the direct prerequisites gauss_signed_half_magnitude_range, gauss_signed_half_magnitude_injective, gauss_signed_half_predecessor_recode_exists, beta_magnitude_sum_permutation_exact as previously established PA formulas.

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

Referenced ingredients

PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA00CY beta_magnitude_sum_permutation_exact

Proof neighborhood

Direct dependencies

PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA00CY beta_magnitude_sum_permutation_exact

Direct dependents

PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two

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 mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro X
  11. 0011intro M
  12. 0012intro hp
  13. 0013intro hprime
  14. 0014intro hnondiv
  15. 0015intro hhalf
  16. 0016intro hsigned
  17. 0017intro hhalf_sum
  18. 0018intro hmagnitude_sum
  19. 0019have hrange : forall gmp_index_ges_magnitude_range. (exists gsp_lt_gap_ges_magnitude_range_index_bound. gsp_lt_gap_ges_magnitude_range_index_bound + S gmp_index_ges_magnitude_range = h) -> exists gmp_magnitude_ges_magnitude_range. ((((exists ff_h_gmp_ges_magnitude_range_decoded. ff_h_gmp_ges_magnitude_range_decoded + S (gmp_magnitude_ges_magnitude_range) = S ((S (gmp_index_ges_magnitude_range)) * mc)) /\ exists ff_q_gmp_ges_magnitude_range_decoded. mb = ff_q_gmp_ges_magnitude_range_decoded * S ((S (gmp_index_ges_magnitude_range)) * mc) + (gmp_magnitude_ges_magnitude_range))) /\ ((exists gsp_lt_gap_ges_magnitude_range_positive. gsp_lt_gap_ges_magnitude_range_positive + S 0 = gmp_magnitude_ges_magnitude_range) /\ (exists gsp_le_gap_ges_magnitude_range_bounded. gsp_le_gap_ges_magnitude_range_bounded + gmp_magnitude_ges_magnitude_range = h)))
  20. 0020specialize gauss_signed_half_magnitude_range p
  21. 0021specialize gauss_signed_half_magnitude_range h
  22. 0022specialize gauss_signed_half_magnitude_range a
  23. 0023specialize gauss_signed_half_magnitude_range b
  24. 0024specialize gauss_signed_half_magnitude_range c
  25. 0025specialize gauss_signed_half_magnitude_range mb
  26. 0026specialize gauss_signed_half_magnitude_range mc
  27. 0027specialize gauss_signed_half_magnitude_range sb
  28. 0028specialize gauss_signed_half_magnitude_range sc
  29. 0029specialize gauss_signed_half_magnitude_range h
  30. 0030apply gauss_signed_half_magnitude_range
  31. 0031exact hsigned
  32. 0032have hinjective : forall fp_i_ges_magnitude_injective fp_j_ges_magnitude_injective fp_value_ges_magnitude_injective. (exists fp_gap_ges_magnitude_injective_i. fp_gap_ges_magnitude_injective_i + S fp_i_ges_magnitude_injective = h) -> (exists fp_gap_ges_magnitude_injective_j. fp_gap_ges_magnitude_injective_j + S fp_j_ges_magnitude_injective = h) -> (((exists ff_h_ges_magnitude_injective_left. ff_h_ges_magnitude_injective_left + S (fp_value_ges_magnitude_injective) = S ((S (fp_i_ges_magnitude_injective)) * mc)) /\ exists ff_q_ges_magnitude_injective_left. mb = ff_q_ges_magnitude_injective_left * S ((S (fp_i_ges_magnitude_injective)) * mc) + (fp_value_ges_magnitude_injective))) -> (((exists ff_h_ges_magnitude_injective_right. ff_h_ges_magnitude_injective_right + S (fp_value_ges_magnitude_injective) = S ((S (fp_j_ges_magnitude_injective)) * mc)) /\ exists ff_q_ges_magnitude_injective_right. mb = ff_q_ges_magnitude_injective_right * S ((S (fp_j_ges_magnitude_injective)) * mc) + (fp_value_ges_magnitude_injective))) -> fp_i_ges_magnitude_injective = fp_j_ges_magnitude_injective
  33. 0033specialize gauss_signed_half_magnitude_injective p
  34. 0034specialize gauss_signed_half_magnitude_injective h
  35. 0035specialize gauss_signed_half_magnitude_injective a
  36. 0036specialize gauss_signed_half_magnitude_injective b
  37. 0037specialize gauss_signed_half_magnitude_injective c
  38. 0038specialize gauss_signed_half_magnitude_injective mb
  39. 0039specialize gauss_signed_half_magnitude_injective mc
  40. 0040specialize gauss_signed_half_magnitude_injective sb
  41. 0041specialize gauss_signed_half_magnitude_injective sc
  42. 0042apply gauss_signed_half_magnitude_injective
  43. 0043exact hp
  44. 0044exact hprime
  45. 0045exact hnondiv
  46. 0046exact hhalf
  47. 0047exact hsigned
  48. 0048have hrecode_exists : exists rb rc. (forall gmp_index_ges_recode_exists gmp_predecessor_ges_recode_exists. (exists gsp_lt_gap_ges_recode_exists_index_bound. gsp_lt_gap_ges_recode_exists_index_bound + S gmp_index_ges_recode_exists = h) -> (((exists gsp_beta_height_gmp_ges_recode_exists_source. gsp_beta_height_gmp_ges_recode_exists_source + S (S gmp_predecessor_ges_recode_exists) = S ((S (gmp_index_ges_recode_exists)) * mc)) /\ exists gsp_beta_quotient_gmp_ges_recode_exists_source. mb = gsp_beta_quotient_gmp_ges_recode_exists_source * S ((S (gmp_index_ges_recode_exists)) * mc) + (S gmp_predecessor_ges_recode_exists))) -> (((exists ff_h_gmp_ges_recode_exists_target. ff_h_gmp_ges_recode_exists_target + S (gmp_predecessor_ges_recode_exists) = S ((S (gmp_index_ges_recode_exists)) * rc)) /\ exists ff_q_gmp_ges_recode_exists_target. rb = ff_q_gmp_ges_recode_exists_target * S ((S (gmp_index_ges_recode_exists)) * rc) + (gmp_predecessor_ges_recode_exists))))
  49. 0049specialize gauss_signed_half_predecessor_recode_exists p
  50. 0050specialize gauss_signed_half_predecessor_recode_exists h
  51. 0051specialize gauss_signed_half_predecessor_recode_exists a
  52. 0052specialize gauss_signed_half_predecessor_recode_exists b
  53. 0053specialize gauss_signed_half_predecessor_recode_exists c
  54. 0054specialize gauss_signed_half_predecessor_recode_exists mb
  55. 0055specialize gauss_signed_half_predecessor_recode_exists mc
  56. 0056specialize gauss_signed_half_predecessor_recode_exists sb
  57. 0057specialize gauss_signed_half_predecessor_recode_exists sc
  58. 0058apply gauss_signed_half_predecessor_recode_exists
  59. 0059exact hsigned
  60. 0060cases hrecode_exists
  61. 0061cases hrecode_exists_witness
  62. 0062specialize beta_magnitude_sum_permutation_exact b
  63. 0063specialize beta_magnitude_sum_permutation_exact c
  64. 0064specialize beta_magnitude_sum_permutation_exact mb
  65. 0065specialize beta_magnitude_sum_permutation_exact mc
  66. 0066specialize beta_magnitude_sum_permutation_exact x
  67. 0067specialize beta_magnitude_sum_permutation_exact x1
  68. 0068specialize beta_magnitude_sum_permutation_exact h
  69. 0069specialize beta_magnitude_sum_permutation_exact X
  70. 0070specialize beta_magnitude_sum_permutation_exact M
  71. 0071apply beta_magnitude_sum_permutation_exact
  72. 0072exact hhalf
  73. 0073exact hrange
  74. 0074exact hinjective
  75. 0075exact hrecode_exists_witness_witness
  76. 0076exact hhalf_sum
  77. 0077exact hmagnitude_sum