PA0074

gauss_signed_half_prefix_exists

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

Every bounded family of pointwise signed choices admits aligned beta-coded magnitude and sign prefixes.

Exact expanded PA statement

forall p h a b c l. (forall gsp_choice_index_exists_all. (exists gsp_lt_gap_exists_all_choice_bound. gsp_lt_gap_exists_all_choice_bound + S gsp_choice_index_exists_all = l) -> (exists gsp_value_exists_all_choice gsp_magnitude_exists_all_choice gsp_sign_exists_all_choice. (((exists ff_h_gsp_exists_all_choice_source. ff_h_gsp_exists_all_choice_source + S (gsp_value_exists_all_choice) = S ((S (gsp_choice_index_exists_all)) * c)) /\ exists ff_q_gsp_exists_all_choice_source. b = ff_q_gsp_exists_all_choice_source * S ((S (gsp_choice_index_exists_all)) * c) + (gsp_value_exists_all_choice))) /\ ((exists gsp_lt_gap_exists_all_choice_positive. gsp_lt_gap_exists_all_choice_positive + S 0 = gsp_magnitude_exists_all_choice) /\ ((exists gsp_le_gap_exists_all_choice_bounded. gsp_le_gap_exists_all_choice_bounded + gsp_magnitude_exists_all_choice = h) /\ ((gsp_sign_exists_all_choice = 0 \/ gsp_sign_exists_all_choice = 1) /\ (((gsp_sign_exists_all_choice = 0 /\ (exists gsp_mod_left_exists_all_choice_lower gsp_mod_right_exists_all_choice_lower. (a * gsp_value_exists_all_choice) + p * gsp_mod_left_exists_all_choice_lower = (gsp_magnitude_exists_all_choice) + p * gsp_mod_right_exists_all_choice_lower)) \/ (gsp_sign_exists_all_choice = 1 /\ (exists gsp_mod_left_exists_all_choice_reflected gsp_mod_right_exists_all_choice_reflected. (a * gsp_value_exists_all_choice) + p * gsp_mod_left_exists_all_choice_reflected = ((2 * h) * gsp_magnitude_exists_all_choice) + p * gsp_mod_right_exists_all_choice_reflected))))))))) -> (exists mb mc sb sc. (forall gsp_index_exists_result. (exists gsp_lt_gap_exists_result_index_bound. gsp_lt_gap_exists_result_index_bound + S gsp_index_exists_result = l) -> (exists gsp_value_exists_result_entry gsp_magnitude_exists_result_entry gsp_sign_exists_result_entry. (((exists ff_h_gsp_exists_result_entry_source. ff_h_gsp_exists_result_entry_source + S (gsp_value_exists_result_entry) = S ((S (gsp_index_exists_result)) * c)) /\ exists ff_q_gsp_exists_result_entry_source. b = ff_q_gsp_exists_result_entry_source * S ((S (gsp_index_exists_result)) * c) + (gsp_value_exists_result_entry))) /\ ((((exists ff_h_gsp_exists_result_entry_magnitude. ff_h_gsp_exists_result_entry_magnitude + S (gsp_magnitude_exists_result_entry) = S ((S (gsp_index_exists_result)) * mc)) /\ exists ff_q_gsp_exists_result_entry_magnitude. mb = ff_q_gsp_exists_result_entry_magnitude * S ((S (gsp_index_exists_result)) * mc) + (gsp_magnitude_exists_result_entry))) /\ ((((exists ff_h_gsp_exists_result_entry_sign. ff_h_gsp_exists_result_entry_sign + S (gsp_sign_exists_result_entry) = S ((S (gsp_index_exists_result)) * sc)) /\ exists ff_q_gsp_exists_result_entry_sign. sb = ff_q_gsp_exists_result_entry_sign * S ((S (gsp_index_exists_result)) * sc) + (gsp_sign_exists_result_entry))) /\ ((exists gsp_lt_gap_exists_result_entry_positive. gsp_lt_gap_exists_result_entry_positive + S 0 = gsp_magnitude_exists_result_entry) /\ ((exists gsp_le_gap_exists_result_entry_bounded. gsp_le_gap_exists_result_entry_bounded + gsp_magnitude_exists_result_entry = h) /\ ((gsp_sign_exists_result_entry = 0 \/ gsp_sign_exists_result_entry = 1) /\ (((gsp_sign_exists_result_entry = 0 /\ (exists gsp_mod_left_exists_result_entry_lower gsp_mod_right_exists_result_entry_lower. (a * gsp_value_exists_result_entry) + p * gsp_mod_left_exists_result_entry_lower = (gsp_magnitude_exists_result_entry) + p * gsp_mod_right_exists_result_entry_lower)) \/ (gsp_sign_exists_result_entry = 1 /\ (exists gsp_mod_left_exists_result_entry_reflected gsp_mod_right_exists_result_entry_reflected. (a * gsp_value_exists_result_entry) + p * gsp_mod_left_exists_result_entry_reflected = ((2 * h) * gsp_magnitude_exists_result_entry) + p * gsp_mod_right_exists_result_entry_reflected))))))))))))

Structural proof guide

Generated structural guide

Every bounded family of pointwise signed choices admits aligned beta-coded magnitude and sign prefixes.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, le_succ, le_refl, gauss_signed_half_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (5), intermediate claims (5).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0073 gauss_signed_half_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0073 gauss_signed_half_prefix_extend

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. 0006induction l
  7. 0007intro hchoices
  8. 0008exists 0
  9. 0009exists 0
  10. 0010exists 0
  11. 0011exists 0
  12. 0012intro i
  13. 0013intro hi
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have hsi : S i = 0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right (S i)
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact hsi
  24. 0024intro hchoices
  25. 0025have hprevious_choices : forall gsp_choice_index_exists_previous. (exists gsp_lt_gap_exists_previous_choice_bound. gsp_lt_gap_exists_previous_choice_bound + S gsp_choice_index_exists_previous = l) -> (exists gsp_value_exists_previous_choice gsp_magnitude_exists_previous_choice gsp_sign_exists_previous_choice. (((exists ff_h_gsp_exists_previous_choice_source. ff_h_gsp_exists_previous_choice_source + S (gsp_value_exists_previous_choice) = S ((S (gsp_choice_index_exists_previous)) * c)) /\ exists ff_q_gsp_exists_previous_choice_source. b = ff_q_gsp_exists_previous_choice_source * S ((S (gsp_choice_index_exists_previous)) * c) + (gsp_value_exists_previous_choice))) /\ ((exists gsp_lt_gap_exists_previous_choice_positive. gsp_lt_gap_exists_previous_choice_positive + S 0 = gsp_magnitude_exists_previous_choice) /\ ((exists gsp_le_gap_exists_previous_choice_bounded. gsp_le_gap_exists_previous_choice_bounded + gsp_magnitude_exists_previous_choice = h) /\ ((gsp_sign_exists_previous_choice = 0 \/ gsp_sign_exists_previous_choice = 1) /\ (((gsp_sign_exists_previous_choice = 0 /\ (exists gsp_mod_left_exists_previous_choice_lower gsp_mod_right_exists_previous_choice_lower. (a * gsp_value_exists_previous_choice) + p * gsp_mod_left_exists_previous_choice_lower = (gsp_magnitude_exists_previous_choice) + p * gsp_mod_right_exists_previous_choice_lower)) \/ (gsp_sign_exists_previous_choice = 1 /\ (exists gsp_mod_left_exists_previous_choice_reflected gsp_mod_right_exists_previous_choice_reflected. (a * gsp_value_exists_previous_choice) + p * gsp_mod_left_exists_previous_choice_reflected = ((2 * h) * gsp_magnitude_exists_previous_choice) + p * gsp_mod_right_exists_previous_choice_reflected))))))))
  26. 0026intro i
  27. 0027intro hi
  28. 0028specialize hchoices i
  29. 0029apply hchoices
  30. 0030specialize le_succ (S i)
  31. 0031specialize le_succ l
  32. 0032apply le_succ
  33. 0033exact hi
  34. 0034have hprevious : exists mb mc sb sc. (forall gsp_index_exists_previous_result. (exists gsp_lt_gap_exists_previous_result_index_bound. gsp_lt_gap_exists_previous_result_index_bound + S gsp_index_exists_previous_result = l) -> (exists gsp_value_exists_previous_result_entry gsp_magnitude_exists_previous_result_entry gsp_sign_exists_previous_result_entry. (((exists ff_h_gsp_exists_previous_result_entry_source. ff_h_gsp_exists_previous_result_entry_source + S (gsp_value_exists_previous_result_entry) = S ((S (gsp_index_exists_previous_result)) * c)) /\ exists ff_q_gsp_exists_previous_result_entry_source. b = ff_q_gsp_exists_previous_result_entry_source * S ((S (gsp_index_exists_previous_result)) * c) + (gsp_value_exists_previous_result_entry))) /\ ((((exists ff_h_gsp_exists_previous_result_entry_magnitude. ff_h_gsp_exists_previous_result_entry_magnitude + S (gsp_magnitude_exists_previous_result_entry) = S ((S (gsp_index_exists_previous_result)) * mc)) /\ exists ff_q_gsp_exists_previous_result_entry_magnitude. mb = ff_q_gsp_exists_previous_result_entry_magnitude * S ((S (gsp_index_exists_previous_result)) * mc) + (gsp_magnitude_exists_previous_result_entry))) /\ ((((exists ff_h_gsp_exists_previous_result_entry_sign. ff_h_gsp_exists_previous_result_entry_sign + S (gsp_sign_exists_previous_result_entry) = S ((S (gsp_index_exists_previous_result)) * sc)) /\ exists ff_q_gsp_exists_previous_result_entry_sign. sb = ff_q_gsp_exists_previous_result_entry_sign * S ((S (gsp_index_exists_previous_result)) * sc) + (gsp_sign_exists_previous_result_entry))) /\ ((exists gsp_lt_gap_exists_previous_result_entry_positive. gsp_lt_gap_exists_previous_result_entry_positive + S 0 = gsp_magnitude_exists_previous_result_entry) /\ ((exists gsp_le_gap_exists_previous_result_entry_bounded. gsp_le_gap_exists_previous_result_entry_bounded + gsp_magnitude_exists_previous_result_entry = h) /\ ((gsp_sign_exists_previous_result_entry = 0 \/ gsp_sign_exists_previous_result_entry = 1) /\ (((gsp_sign_exists_previous_result_entry = 0 /\ (exists gsp_mod_left_exists_previous_result_entry_lower gsp_mod_right_exists_previous_result_entry_lower. (a * gsp_value_exists_previous_result_entry) + p * gsp_mod_left_exists_previous_result_entry_lower = (gsp_magnitude_exists_previous_result_entry) + p * gsp_mod_right_exists_previous_result_entry_lower)) \/ (gsp_sign_exists_previous_result_entry = 1 /\ (exists gsp_mod_left_exists_previous_result_entry_reflected gsp_mod_right_exists_previous_result_entry_reflected. (a * gsp_value_exists_previous_result_entry) + p * gsp_mod_left_exists_previous_result_entry_reflected = ((2 * h) * gsp_magnitude_exists_previous_result_entry) + p * gsp_mod_right_exists_previous_result_entry_reflected)))))))))))
  35. 0035apply IH
  36. 0036exact hprevious_choices
  37. 0037cases hprevious
  38. 0038cases hprevious_witness
  39. 0039cases hprevious_witness_witness
  40. 0040cases hprevious_witness_witness_witness
  41. 0041have hlast : exists gsp_value_exists_last_choice gsp_magnitude_exists_last_choice gsp_sign_exists_last_choice. (((exists ff_h_gsp_exists_last_choice_source. ff_h_gsp_exists_last_choice_source + S (gsp_value_exists_last_choice) = S ((S (l)) * c)) /\ exists ff_q_gsp_exists_last_choice_source. b = ff_q_gsp_exists_last_choice_source * S ((S (l)) * c) + (gsp_value_exists_last_choice))) /\ ((exists gsp_lt_gap_exists_last_choice_positive. gsp_lt_gap_exists_last_choice_positive + S 0 = gsp_magnitude_exists_last_choice) /\ ((exists gsp_le_gap_exists_last_choice_bounded. gsp_le_gap_exists_last_choice_bounded + gsp_magnitude_exists_last_choice = h) /\ ((gsp_sign_exists_last_choice = 0 \/ gsp_sign_exists_last_choice = 1) /\ (((gsp_sign_exists_last_choice = 0 /\ (exists gsp_mod_left_exists_last_choice_lower gsp_mod_right_exists_last_choice_lower. (a * gsp_value_exists_last_choice) + p * gsp_mod_left_exists_last_choice_lower = (gsp_magnitude_exists_last_choice) + p * gsp_mod_right_exists_last_choice_lower)) \/ (gsp_sign_exists_last_choice = 1 /\ (exists gsp_mod_left_exists_last_choice_reflected gsp_mod_right_exists_last_choice_reflected. (a * gsp_value_exists_last_choice) + p * gsp_mod_left_exists_last_choice_reflected = ((2 * h) * gsp_magnitude_exists_last_choice) + p * gsp_mod_right_exists_last_choice_reflected)))))))
  42. 0042specialize hchoices l
  43. 0043apply hchoices
  44. 0044specialize le_refl (S l)
  45. 0045exact le_refl
  46. 0046have hnext : exists mb mc sb sc. (forall gsp_index_exists_next_result. (exists gsp_lt_gap_exists_next_result_index_bound. gsp_lt_gap_exists_next_result_index_bound + S gsp_index_exists_next_result = S l) -> (exists gsp_value_exists_next_result_entry gsp_magnitude_exists_next_result_entry gsp_sign_exists_next_result_entry. (((exists ff_h_gsp_exists_next_result_entry_source. ff_h_gsp_exists_next_result_entry_source + S (gsp_value_exists_next_result_entry) = S ((S (gsp_index_exists_next_result)) * c)) /\ exists ff_q_gsp_exists_next_result_entry_source. b = ff_q_gsp_exists_next_result_entry_source * S ((S (gsp_index_exists_next_result)) * c) + (gsp_value_exists_next_result_entry))) /\ ((((exists ff_h_gsp_exists_next_result_entry_magnitude. ff_h_gsp_exists_next_result_entry_magnitude + S (gsp_magnitude_exists_next_result_entry) = S ((S (gsp_index_exists_next_result)) * mc)) /\ exists ff_q_gsp_exists_next_result_entry_magnitude. mb = ff_q_gsp_exists_next_result_entry_magnitude * S ((S (gsp_index_exists_next_result)) * mc) + (gsp_magnitude_exists_next_result_entry))) /\ ((((exists ff_h_gsp_exists_next_result_entry_sign. ff_h_gsp_exists_next_result_entry_sign + S (gsp_sign_exists_next_result_entry) = S ((S (gsp_index_exists_next_result)) * sc)) /\ exists ff_q_gsp_exists_next_result_entry_sign. sb = ff_q_gsp_exists_next_result_entry_sign * S ((S (gsp_index_exists_next_result)) * sc) + (gsp_sign_exists_next_result_entry))) /\ ((exists gsp_lt_gap_exists_next_result_entry_positive. gsp_lt_gap_exists_next_result_entry_positive + S 0 = gsp_magnitude_exists_next_result_entry) /\ ((exists gsp_le_gap_exists_next_result_entry_bounded. gsp_le_gap_exists_next_result_entry_bounded + gsp_magnitude_exists_next_result_entry = h) /\ ((gsp_sign_exists_next_result_entry = 0 \/ gsp_sign_exists_next_result_entry = 1) /\ (((gsp_sign_exists_next_result_entry = 0 /\ (exists gsp_mod_left_exists_next_result_entry_lower gsp_mod_right_exists_next_result_entry_lower. (a * gsp_value_exists_next_result_entry) + p * gsp_mod_left_exists_next_result_entry_lower = (gsp_magnitude_exists_next_result_entry) + p * gsp_mod_right_exists_next_result_entry_lower)) \/ (gsp_sign_exists_next_result_entry = 1 /\ (exists gsp_mod_left_exists_next_result_entry_reflected gsp_mod_right_exists_next_result_entry_reflected. (a * gsp_value_exists_next_result_entry) + p * gsp_mod_left_exists_next_result_entry_reflected = ((2 * h) * gsp_magnitude_exists_next_result_entry) + p * gsp_mod_right_exists_next_result_entry_reflected)))))))))))
  47. 0047specialize gauss_signed_half_prefix_extend p
  48. 0048specialize gauss_signed_half_prefix_extend h
  49. 0049specialize gauss_signed_half_prefix_extend a
  50. 0050specialize gauss_signed_half_prefix_extend b
  51. 0051specialize gauss_signed_half_prefix_extend c
  52. 0052specialize gauss_signed_half_prefix_extend x
  53. 0053specialize gauss_signed_half_prefix_extend x1
  54. 0054specialize gauss_signed_half_prefix_extend x2
  55. 0055specialize gauss_signed_half_prefix_extend x3
  56. 0056specialize gauss_signed_half_prefix_extend l
  57. 0057apply gauss_signed_half_prefix_extend
  58. 0058exact hprevious_witness_witness_witness_witness
  59. 0059exact hlast
  60. 0060exact hnext