PA0071

gauss_pointwise_signed_half_choice

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

A canonical nonzero remainder yields one explicit zero/one signed-half choice at its decoded source index.

Exact expanded PA statement

forall p h a b c i x q r. p = 2 * h + 1 -> (((exists ff_h_gsp_point_source. ff_h_gsp_point_source + S (x) = S ((S (i)) * c)) /\ exists ff_q_gsp_point_source. b = ff_q_gsp_point_source * S ((S (i)) * c) + (x))) -> a * x = q * p + r -> (exists gsp_lt_gap_point_remainder_bound. gsp_lt_gap_point_remainder_bound + S r = p) -> ~(r = 0) -> (exists gsp_value_point_result gsp_magnitude_point_result gsp_sign_point_result. (((exists ff_h_gsp_point_result_source. ff_h_gsp_point_result_source + S (gsp_value_point_result) = S ((S (i)) * c)) /\ exists ff_q_gsp_point_result_source. b = ff_q_gsp_point_result_source * S ((S (i)) * c) + (gsp_value_point_result))) /\ ((exists gsp_lt_gap_point_result_positive. gsp_lt_gap_point_result_positive + S 0 = gsp_magnitude_point_result) /\ ((exists gsp_le_gap_point_result_bounded. gsp_le_gap_point_result_bounded + gsp_magnitude_point_result = h) /\ ((gsp_sign_point_result = 0 \/ gsp_sign_point_result = 1) /\ (((gsp_sign_point_result = 0 /\ (exists gsp_mod_left_point_result_lower gsp_mod_right_point_result_lower. (a * gsp_value_point_result) + p * gsp_mod_left_point_result_lower = (gsp_magnitude_point_result) + p * gsp_mod_right_point_result_lower)) \/ (gsp_sign_point_result = 1 /\ (exists gsp_mod_left_point_result_reflected gsp_mod_right_point_result_reflected. (a * gsp_value_point_result) + p * gsp_mod_left_point_result_reflected = ((2 * h) * gsp_magnitude_point_result) + p * gsp_mod_right_point_result_reflected))))))))

Structural proof guide

Generated structural guide

A canonical nonzero remainder yields one explicit zero/one signed-half choice at its decoded source index.

Use the direct prerequisites gauss_pointwise_signed_half_representative as previously established PA formulas.

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

Referenced ingredients

PA0070 gauss_pointwise_signed_half_representative

Proof neighborhood

Direct dependencies

PA0070 gauss_pointwise_signed_half_representative

Direct dependents

PA0072 gauss_half_range_signed_choices

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 i
  7. 0007intro x
  8. 0008intro q
  9. 0009intro r
  10. 0010intro hp
  11. 0011intro hsource
  12. 0012intro hdecomp
  13. 0013intro hrp
  14. 0014intro hr0
  15. 0015have hrepresentative : exists m. (exists gsp_lt_gap_point_result_positive. gsp_lt_gap_point_result_positive + S 0 = m) /\ ((exists gsp_le_gap_point_result_bounded. gsp_le_gap_point_result_bounded + m = h) /\ ((exists gsp_mod_left_point_result_lower gsp_mod_right_point_result_lower. (a * x) + p * gsp_mod_left_point_result_lower = (m) + p * gsp_mod_right_point_result_lower) \/ (exists gsp_mod_left_point_result_reflected gsp_mod_right_point_result_reflected. (a * x) + p * gsp_mod_left_point_result_reflected = ((2 * h) * m) + p * gsp_mod_right_point_result_reflected)))
  16. 0016specialize gauss_pointwise_signed_half_representative p
  17. 0017specialize gauss_pointwise_signed_half_representative h
  18. 0018specialize gauss_pointwise_signed_half_representative a
  19. 0019specialize gauss_pointwise_signed_half_representative x
  20. 0020specialize gauss_pointwise_signed_half_representative q
  21. 0021specialize gauss_pointwise_signed_half_representative r
  22. 0022apply gauss_pointwise_signed_half_representative
  23. 0023exact hp
  24. 0024exact hdecomp
  25. 0025exact hrp
  26. 0026exact hr0
  27. 0027cases hrepresentative
  28. 0028cases hrepresentative_witness
  29. 0029cases hrepresentative_witness_right
  30. 0030cases hrepresentative_witness_right_right
  31. 0031exists x
  32. 0032exists x1
  33. 0033exists 0
  34. 0034split
  35. 0035exact hsource
  36. 0036split
  37. 0037exact hrepresentative_witness_left
  38. 0038split
  39. 0039exact hrepresentative_witness_right_left
  40. 0040split
  41. 0041left
  42. 0042refl
  43. 0043left
  44. 0044split
  45. 0045refl
  46. 0046exact hrepresentative_witness_right_right_left
  47. 0047exists x
  48. 0048exists x1
  49. 0049exists 1
  50. 0050split
  51. 0051exact hsource
  52. 0052split
  53. 0053exact hrepresentative_witness_left
  54. 0054split
  55. 0055exact hrepresentative_witness_right_left
  56. 0056split
  57. 0057right
  58. 0058refl
  59. 0059right
  60. 0060split
  61. 0061refl
  62. 0062exact hrepresentative_witness_right_right_right