PA0072

gauss_half_range_signed_choices

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

A prime odd half-range and a nondivisible multiplier provide a signed choice at every decoded entry.

Exact expanded PA statement

forall p h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_half_range_prime gsp_prime_right_half_range_prime. p = gsp_prime_left_half_range_prime * gsp_prime_right_half_range_prime -> gsp_prime_left_half_range_prime = 1 \/ gsp_prime_right_half_range_prime = 1)) -> (~(exists gsp_divisor_factor_half_range_multiplier. a = p * gsp_divisor_factor_half_range_multiplier)) -> (forall gsp_range_index_half_range_source. (exists gsp_lt_gap_half_range_source_range_bound. gsp_lt_gap_half_range_source_range_bound + S gsp_range_index_half_range_source = h) -> (((exists gsp_beta_height_half_range_source_range_entry. gsp_beta_height_half_range_source_range_entry + S (1 + gsp_range_index_half_range_source) = S ((S (gsp_range_index_half_range_source)) * c)) /\ exists gsp_beta_quotient_half_range_source_range_entry. b = gsp_beta_quotient_half_range_source_range_entry * S ((S (gsp_range_index_half_range_source)) * c) + (1 + gsp_range_index_half_range_source)))) -> (forall gsp_choice_index_half_range_choices. (exists gsp_lt_gap_half_range_choices_choice_bound. gsp_lt_gap_half_range_choices_choice_bound + S gsp_choice_index_half_range_choices = h) -> (exists gsp_value_half_range_choices_choice gsp_magnitude_half_range_choices_choice gsp_sign_half_range_choices_choice. (((exists ff_h_gsp_half_range_choices_choice_source. ff_h_gsp_half_range_choices_choice_source + S (gsp_value_half_range_choices_choice) = S ((S (gsp_choice_index_half_range_choices)) * c)) /\ exists ff_q_gsp_half_range_choices_choice_source. b = ff_q_gsp_half_range_choices_choice_source * S ((S (gsp_choice_index_half_range_choices)) * c) + (gsp_value_half_range_choices_choice))) /\ ((exists gsp_lt_gap_half_range_choices_choice_positive. gsp_lt_gap_half_range_choices_choice_positive + S 0 = gsp_magnitude_half_range_choices_choice) /\ ((exists gsp_le_gap_half_range_choices_choice_bounded. gsp_le_gap_half_range_choices_choice_bounded + gsp_magnitude_half_range_choices_choice = h) /\ ((gsp_sign_half_range_choices_choice = 0 \/ gsp_sign_half_range_choices_choice = 1) /\ (((gsp_sign_half_range_choices_choice = 0 /\ (exists gsp_mod_left_half_range_choices_choice_lower gsp_mod_right_half_range_choices_choice_lower. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_lower = (gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_lower)) \/ (gsp_sign_half_range_choices_choice = 1 /\ (exists gsp_mod_left_half_range_choices_choice_reflected gsp_mod_right_half_range_choices_choice_reflected. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_reflected = ((2 * h) * gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_reflected)))))))))

Structural proof guide

Generated structural guide

A prime odd half-range and a nondivisible multiplier provide a signed choice at every decoded entry.

Use the direct prerequisites prime_nonzero, division_remainder_exists, beta_half_range_entry_bounds, euclid_prime_dvd_product, divisor_le_nonzero, lt_not_le, mul_comm, gauss_pointwise_signed_half_choice as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (9), equality transport (1).

Referenced ingredients

PA0031 prime_nonzero PA001D division_remainder_exists PA0034 beta_half_range_entry_bounds PA0038 euclid_prime_dvd_product PA0039 divisor_le_nonzero PA003A lt_not_le PA000H mul_comm PA0071 gauss_pointwise_signed_half_choice

Proof neighborhood

Direct dependencies

PA0031 prime_nonzero PA001D division_remainder_exists PA0034 beta_half_range_entry_bounds PA0038 euclid_prime_dvd_product PA0039 divisor_le_nonzero PA003A lt_not_le PA000H mul_comm PA0071 gauss_pointwise_signed_half_choice

Direct dependents

PA0075 gauss_half_range_signed_prefix_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 hp
  7. 0007intro hprime
  8. 0008intro hnotdiv
  9. 0009intro hrange
  10. 0010intro i
  11. 0011intro hi
  12. 0012have hsource : ((exists gsp_beta_height_half_range_source_entry_i. gsp_beta_height_half_range_source_entry_i + S (1 + i) = S ((S (i)) * c)) /\ exists gsp_beta_quotient_half_range_source_entry_i. b = gsp_beta_quotient_half_range_source_entry_i * S ((S (i)) * c) + (1 + i))
  13. 0013specialize hrange i
  14. 0014apply hrange
  15. 0015exact hi
  16. 0016have hbounds : (~(1 + i = 0) /\ (exists gsp_half_value_bound_gap. gsp_half_value_bound_gap + S (1 + i) = p))
  17. 0017specialize beta_half_range_entry_bounds p
  18. 0018specialize beta_half_range_entry_bounds h
  19. 0019specialize beta_half_range_entry_bounds b
  20. 0020specialize beta_half_range_entry_bounds c
  21. 0021specialize beta_half_range_entry_bounds i
  22. 0022specialize beta_half_range_entry_bounds (1 + i)
  23. 0023apply beta_half_range_entry_bounds
  24. 0024exact hp
  25. 0025exact hrange
  26. 0026exact hi
  27. 0027exact hsource
  28. 0028cases hbounds
  29. 0029have hp0 : ~(p = 0)
  30. 0030intro hpzero
  31. 0031specialize prime_nonzero p
  32. 0032apply prime_nonzero
  33. 0033exact hprime
  34. 0034exact hpzero
  35. 0035have hdiv : exists q r. a * (1 + i) = p * q + r /\ (exists gsp_half_value_bound_gap. gsp_half_value_bound_gap + S (r) = p)
  36. 0036specialize division_remainder_exists p
  37. 0037specialize division_remainder_exists (a * (1 + i))
  38. 0038apply division_remainder_exists
  39. 0039exact hp0
  40. 0040cases hdiv
  41. 0041cases hdiv_witness
  42. 0042cases hdiv_witness_witness
  43. 0043have hrem0 : ~(x1 = 0)
  44. 0044intro hremzero
  45. 0045have hmultiple : exists k. a * (1 + i) = p * k
  46. 0046exists x
  47. 0047trans p * x + x1
  48. 0048exact hdiv_witness_witness_left
  49. 0049rewrite hremzero
  50. 0050apply PA3
  51. 0051have hfactor : (exists u. a = p * u) \/ exists v. 1 + i = p * v
  52. 0052specialize euclid_prime_dvd_product p
  53. 0053specialize euclid_prime_dvd_product a
  54. 0054specialize euclid_prime_dvd_product (1 + i)
  55. 0055apply euclid_prime_dvd_product
  56. 0056exact hprime
  57. 0057exact hmultiple
  58. 0058cases hfactor
  59. 0059apply hnotdiv
  60. 0060exact hfactor_left
  61. 0061have hple : exists k. k + p = 1 + i
  62. 0062specialize divisor_le_nonzero p
  63. 0063specialize divisor_le_nonzero (1 + i)
  64. 0064apply divisor_le_nonzero
  65. 0065exact hbounds_left
  66. 0066exact hfactor_right
  67. 0067specialize lt_not_le (1 + i)
  68. 0068specialize lt_not_le p
  69. 0069apply lt_not_le
  70. 0070exact hbounds_right
  71. 0071exact hple
  72. 0072have hdecomp : a * (1 + i) = x * p + x1
  73. 0073trans p * x + x1
  74. 0074exact hdiv_witness_witness_left
  75. 0075congr
  76. 0076apply mul_comm
  77. 0077refl
  78. 0078specialize gauss_pointwise_signed_half_choice p
  79. 0079specialize gauss_pointwise_signed_half_choice h
  80. 0080specialize gauss_pointwise_signed_half_choice a
  81. 0081specialize gauss_pointwise_signed_half_choice b
  82. 0082specialize gauss_pointwise_signed_half_choice c
  83. 0083specialize gauss_pointwise_signed_half_choice i
  84. 0084specialize gauss_pointwise_signed_half_choice (1 + i)
  85. 0085specialize gauss_pointwise_signed_half_choice x
  86. 0086specialize gauss_pointwise_signed_half_choice x1
  87. 0087apply gauss_pointwise_signed_half_choice
  88. 0088exact hp
  89. 0089exact hsource
  90. 0090exact hdecomp
  91. 0091exact hdiv_witness_witness_right
  92. 0092exact hrem0