PA0073

gauss_signed_half_prefix_extend

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

Append one pointwise signed choice simultaneously to the magnitude and zero/one sign beta prefixes.

Exact expanded PA statement

forall p h a b c mb mc sb sc l. (forall gsp_index_extend_before. (exists gsp_lt_gap_extend_before_index_bound. gsp_lt_gap_extend_before_index_bound + S gsp_index_extend_before = l) -> (exists gsp_value_extend_before_entry gsp_magnitude_extend_before_entry gsp_sign_extend_before_entry. (((exists ff_h_gsp_extend_before_entry_source. ff_h_gsp_extend_before_entry_source + S (gsp_value_extend_before_entry) = S ((S (gsp_index_extend_before)) * c)) /\ exists ff_q_gsp_extend_before_entry_source. b = ff_q_gsp_extend_before_entry_source * S ((S (gsp_index_extend_before)) * c) + (gsp_value_extend_before_entry))) /\ ((((exists ff_h_gsp_extend_before_entry_magnitude. ff_h_gsp_extend_before_entry_magnitude + S (gsp_magnitude_extend_before_entry) = S ((S (gsp_index_extend_before)) * mc)) /\ exists ff_q_gsp_extend_before_entry_magnitude. mb = ff_q_gsp_extend_before_entry_magnitude * S ((S (gsp_index_extend_before)) * mc) + (gsp_magnitude_extend_before_entry))) /\ ((((exists ff_h_gsp_extend_before_entry_sign. ff_h_gsp_extend_before_entry_sign + S (gsp_sign_extend_before_entry) = S ((S (gsp_index_extend_before)) * sc)) /\ exists ff_q_gsp_extend_before_entry_sign. sb = ff_q_gsp_extend_before_entry_sign * S ((S (gsp_index_extend_before)) * sc) + (gsp_sign_extend_before_entry))) /\ ((exists gsp_lt_gap_extend_before_entry_positive. gsp_lt_gap_extend_before_entry_positive + S 0 = gsp_magnitude_extend_before_entry) /\ ((exists gsp_le_gap_extend_before_entry_bounded. gsp_le_gap_extend_before_entry_bounded + gsp_magnitude_extend_before_entry = h) /\ ((gsp_sign_extend_before_entry = 0 \/ gsp_sign_extend_before_entry = 1) /\ (((gsp_sign_extend_before_entry = 0 /\ (exists gsp_mod_left_extend_before_entry_lower gsp_mod_right_extend_before_entry_lower. (a * gsp_value_extend_before_entry) + p * gsp_mod_left_extend_before_entry_lower = (gsp_magnitude_extend_before_entry) + p * gsp_mod_right_extend_before_entry_lower)) \/ (gsp_sign_extend_before_entry = 1 /\ (exists gsp_mod_left_extend_before_entry_reflected gsp_mod_right_extend_before_entry_reflected. (a * gsp_value_extend_before_entry) + p * gsp_mod_left_extend_before_entry_reflected = ((2 * h) * gsp_magnitude_extend_before_entry) + p * gsp_mod_right_extend_before_entry_reflected))))))))))) -> (exists gsp_value_extend_choice gsp_magnitude_extend_choice gsp_sign_extend_choice. (((exists ff_h_gsp_extend_choice_source. ff_h_gsp_extend_choice_source + S (gsp_value_extend_choice) = S ((S (l)) * c)) /\ exists ff_q_gsp_extend_choice_source. b = ff_q_gsp_extend_choice_source * S ((S (l)) * c) + (gsp_value_extend_choice))) /\ ((exists gsp_lt_gap_extend_choice_positive. gsp_lt_gap_extend_choice_positive + S 0 = gsp_magnitude_extend_choice) /\ ((exists gsp_le_gap_extend_choice_bounded. gsp_le_gap_extend_choice_bounded + gsp_magnitude_extend_choice = h) /\ ((gsp_sign_extend_choice = 0 \/ gsp_sign_extend_choice = 1) /\ (((gsp_sign_extend_choice = 0 /\ (exists gsp_mod_left_extend_choice_lower gsp_mod_right_extend_choice_lower. (a * gsp_value_extend_choice) + p * gsp_mod_left_extend_choice_lower = (gsp_magnitude_extend_choice) + p * gsp_mod_right_extend_choice_lower)) \/ (gsp_sign_extend_choice = 1 /\ (exists gsp_mod_left_extend_choice_reflected gsp_mod_right_extend_choice_reflected. (a * gsp_value_extend_choice) + p * gsp_mod_left_extend_choice_reflected = ((2 * h) * gsp_magnitude_extend_choice) + p * gsp_mod_right_extend_choice_reflected)))))))) -> exists z d u v. (forall gsp_index_extend_after. (exists gsp_lt_gap_extend_after_index_bound. gsp_lt_gap_extend_after_index_bound + S gsp_index_extend_after = S l) -> (exists gsp_value_extend_after_entry gsp_magnitude_extend_after_entry gsp_sign_extend_after_entry. (((exists ff_h_gsp_extend_after_entry_source. ff_h_gsp_extend_after_entry_source + S (gsp_value_extend_after_entry) = S ((S (gsp_index_extend_after)) * c)) /\ exists ff_q_gsp_extend_after_entry_source. b = ff_q_gsp_extend_after_entry_source * S ((S (gsp_index_extend_after)) * c) + (gsp_value_extend_after_entry))) /\ ((((exists ff_h_gsp_extend_after_entry_magnitude. ff_h_gsp_extend_after_entry_magnitude + S (gsp_magnitude_extend_after_entry) = S ((S (gsp_index_extend_after)) * d)) /\ exists ff_q_gsp_extend_after_entry_magnitude. z = ff_q_gsp_extend_after_entry_magnitude * S ((S (gsp_index_extend_after)) * d) + (gsp_magnitude_extend_after_entry))) /\ ((((exists ff_h_gsp_extend_after_entry_sign. ff_h_gsp_extend_after_entry_sign + S (gsp_sign_extend_after_entry) = S ((S (gsp_index_extend_after)) * v)) /\ exists ff_q_gsp_extend_after_entry_sign. u = ff_q_gsp_extend_after_entry_sign * S ((S (gsp_index_extend_after)) * v) + (gsp_sign_extend_after_entry))) /\ ((exists gsp_lt_gap_extend_after_entry_positive. gsp_lt_gap_extend_after_entry_positive + S 0 = gsp_magnitude_extend_after_entry) /\ ((exists gsp_le_gap_extend_after_entry_bounded. gsp_le_gap_extend_after_entry_bounded + gsp_magnitude_extend_after_entry = h) /\ ((gsp_sign_extend_after_entry = 0 \/ gsp_sign_extend_after_entry = 1) /\ (((gsp_sign_extend_after_entry = 0 /\ (exists gsp_mod_left_extend_after_entry_lower gsp_mod_right_extend_after_entry_lower. (a * gsp_value_extend_after_entry) + p * gsp_mod_left_extend_after_entry_lower = (gsp_magnitude_extend_after_entry) + p * gsp_mod_right_extend_after_entry_lower)) \/ (gsp_sign_extend_after_entry = 1 /\ (exists gsp_mod_left_extend_after_entry_reflected gsp_mod_right_extend_after_entry_reflected. (a * gsp_value_extend_after_entry) + p * gsp_mod_left_extend_after_entry_reflected = ((2 * h) * gsp_magnitude_extend_after_entry) + p * gsp_mod_right_extend_after_entry_reflected)))))))))))

Structural proof guide

Generated structural guide

Append one pointwise signed choice simultaneously to the magnitude and zero/one sign beta prefixes.

Use the direct prerequisites beta_prefix_extend, finite_lt_succ_eq_or_lt as previously established PA formulas.

The proof proceeds by case analysis (23), intermediate claims (4), equality transport (6).

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA0074 gauss_signed_half_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 mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro l
  11. 0011intro hprefix
  12. 0012intro hchoice
  13. 0013cases hchoice
  14. 0014cases hchoice_witness
  15. 0015cases hchoice_witness_witness
  16. 0016cases hchoice_witness_witness_witness
  17. 0017cases hchoice_witness_witness_witness_right
  18. 0018cases hchoice_witness_witness_witness_right_right
  19. 0019cases hchoice_witness_witness_witness_right_right_right
  20. 0020have hmag_extend : exists gsp_new_code_magnitude_extension gsp_new_scale_magnitude_extension. (((exists ff_h_gsp_magnitude_extension_new_last. ff_h_gsp_magnitude_extension_new_last + S (x1) = S ((S (l)) * gsp_new_scale_magnitude_extension)) /\ exists ff_q_gsp_magnitude_extension_new_last. gsp_new_code_magnitude_extension = ff_q_gsp_magnitude_extension_new_last * S ((S (l)) * gsp_new_scale_magnitude_extension) + (x1))) /\ forall gsp_old_index_magnitude_extension gsp_old_value_magnitude_extension. (exists gsp_lt_gap_magnitude_extension_old_bound. gsp_lt_gap_magnitude_extension_old_bound + S gsp_old_index_magnitude_extension = l) -> (((exists ff_h_gsp_magnitude_extension_old_entry. ff_h_gsp_magnitude_extension_old_entry + S (gsp_old_value_magnitude_extension) = S ((S (gsp_old_index_magnitude_extension)) * mc)) /\ exists ff_q_gsp_magnitude_extension_old_entry. mb = ff_q_gsp_magnitude_extension_old_entry * S ((S (gsp_old_index_magnitude_extension)) * mc) + (gsp_old_value_magnitude_extension))) -> (((exists ff_h_gsp_magnitude_extension_new_entry. ff_h_gsp_magnitude_extension_new_entry + S (gsp_old_value_magnitude_extension) = S ((S (gsp_old_index_magnitude_extension)) * gsp_new_scale_magnitude_extension)) /\ exists ff_q_gsp_magnitude_extension_new_entry. gsp_new_code_magnitude_extension = ff_q_gsp_magnitude_extension_new_entry * S ((S (gsp_old_index_magnitude_extension)) * gsp_new_scale_magnitude_extension) + (gsp_old_value_magnitude_extension)))
  21. 0021specialize beta_prefix_extend l
  22. 0022specialize beta_prefix_extend mb
  23. 0023specialize beta_prefix_extend mc
  24. 0024specialize beta_prefix_extend x1
  25. 0025exact beta_prefix_extend
  26. 0026cases hmag_extend
  27. 0027cases hmag_extend_witness
  28. 0028cases hmag_extend_witness_witness
  29. 0029have hsign_extend : exists gsp_new_code_sign_extension gsp_new_scale_sign_extension. (((exists ff_h_gsp_sign_extension_new_last. ff_h_gsp_sign_extension_new_last + S (x2) = S ((S (l)) * gsp_new_scale_sign_extension)) /\ exists ff_q_gsp_sign_extension_new_last. gsp_new_code_sign_extension = ff_q_gsp_sign_extension_new_last * S ((S (l)) * gsp_new_scale_sign_extension) + (x2))) /\ forall gsp_old_index_sign_extension gsp_old_value_sign_extension. (exists gsp_lt_gap_sign_extension_old_bound. gsp_lt_gap_sign_extension_old_bound + S gsp_old_index_sign_extension = l) -> (((exists ff_h_gsp_sign_extension_old_entry. ff_h_gsp_sign_extension_old_entry + S (gsp_old_value_sign_extension) = S ((S (gsp_old_index_sign_extension)) * sc)) /\ exists ff_q_gsp_sign_extension_old_entry. sb = ff_q_gsp_sign_extension_old_entry * S ((S (gsp_old_index_sign_extension)) * sc) + (gsp_old_value_sign_extension))) -> (((exists ff_h_gsp_sign_extension_new_entry. ff_h_gsp_sign_extension_new_entry + S (gsp_old_value_sign_extension) = S ((S (gsp_old_index_sign_extension)) * gsp_new_scale_sign_extension)) /\ exists ff_q_gsp_sign_extension_new_entry. gsp_new_code_sign_extension = ff_q_gsp_sign_extension_new_entry * S ((S (gsp_old_index_sign_extension)) * gsp_new_scale_sign_extension) + (gsp_old_value_sign_extension)))
  30. 0030specialize beta_prefix_extend l
  31. 0031specialize beta_prefix_extend sb
  32. 0032specialize beta_prefix_extend sc
  33. 0033specialize beta_prefix_extend x2
  34. 0034exact beta_prefix_extend
  35. 0035cases hsign_extend
  36. 0036cases hsign_extend_witness
  37. 0037cases hsign_extend_witness_witness
  38. 0038exists x3
  39. 0039exists x4
  40. 0040exists x5
  41. 0041exists x6
  42. 0042intro i
  43. 0043intro hi
  44. 0044have hsplit : i = l \/ exists gap. gap + S i = l
  45. 0045specialize finite_lt_succ_eq_or_lt l
  46. 0046specialize finite_lt_succ_eq_or_lt i
  47. 0047apply finite_lt_succ_eq_or_lt
  48. 0048exact hi
  49. 0049cases hsplit
  50. 0050exists x
  51. 0051exists x1
  52. 0052exists x2
  53. 0053split
  54. 0054rewrite hsplit_left
  55. 0055rewrite hsplit_left
  56. 0056exact hchoice_witness_witness_witness_left
  57. 0057split
  58. 0058rewrite hsplit_left
  59. 0059rewrite hsplit_left
  60. 0060exact hmag_extend_witness_witness_left
  61. 0061split
  62. 0062rewrite hsplit_left
  63. 0063rewrite hsplit_left
  64. 0064exact hsign_extend_witness_witness_left
  65. 0065split
  66. 0066exact hchoice_witness_witness_witness_right_left
  67. 0067split
  68. 0068exact hchoice_witness_witness_witness_right_right_left
  69. 0069split
  70. 0070exact hchoice_witness_witness_witness_right_right_right_left
  71. 0071exact hchoice_witness_witness_witness_right_right_right_right
  72. 0072have hold : exists gsp_value_extend_previous_entry gsp_magnitude_extend_previous_entry gsp_sign_extend_previous_entry. (((exists ff_h_gsp_extend_previous_entry_source. ff_h_gsp_extend_previous_entry_source + S (gsp_value_extend_previous_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_extend_previous_entry_source. b = ff_q_gsp_extend_previous_entry_source * S ((S (i)) * c) + (gsp_value_extend_previous_entry))) /\ ((((exists ff_h_gsp_extend_previous_entry_magnitude. ff_h_gsp_extend_previous_entry_magnitude + S (gsp_magnitude_extend_previous_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_extend_previous_entry_magnitude. mb = ff_q_gsp_extend_previous_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_extend_previous_entry))) /\ ((((exists ff_h_gsp_extend_previous_entry_sign. ff_h_gsp_extend_previous_entry_sign + S (gsp_sign_extend_previous_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_extend_previous_entry_sign. sb = ff_q_gsp_extend_previous_entry_sign * S ((S (i)) * sc) + (gsp_sign_extend_previous_entry))) /\ ((exists gsp_lt_gap_extend_previous_entry_positive. gsp_lt_gap_extend_previous_entry_positive + S 0 = gsp_magnitude_extend_previous_entry) /\ ((exists gsp_le_gap_extend_previous_entry_bounded. gsp_le_gap_extend_previous_entry_bounded + gsp_magnitude_extend_previous_entry = h) /\ ((gsp_sign_extend_previous_entry = 0 \/ gsp_sign_extend_previous_entry = 1) /\ (((gsp_sign_extend_previous_entry = 0 /\ (exists gsp_mod_left_extend_previous_entry_lower gsp_mod_right_extend_previous_entry_lower. (a * gsp_value_extend_previous_entry) + p * gsp_mod_left_extend_previous_entry_lower = (gsp_magnitude_extend_previous_entry) + p * gsp_mod_right_extend_previous_entry_lower)) \/ (gsp_sign_extend_previous_entry = 1 /\ (exists gsp_mod_left_extend_previous_entry_reflected gsp_mod_right_extend_previous_entry_reflected. (a * gsp_value_extend_previous_entry) + p * gsp_mod_left_extend_previous_entry_reflected = ((2 * h) * gsp_magnitude_extend_previous_entry) + p * gsp_mod_right_extend_previous_entry_reflected)))))))))
  73. 0073specialize hprefix i
  74. 0074apply hprefix
  75. 0075exact hsplit_right
  76. 0076cases hold
  77. 0077cases hold_witness
  78. 0078cases hold_witness_witness
  79. 0079cases hold_witness_witness_witness
  80. 0080cases hold_witness_witness_witness_right
  81. 0081cases hold_witness_witness_witness_right_right
  82. 0082cases hold_witness_witness_witness_right_right_right
  83. 0083cases hold_witness_witness_witness_right_right_right_right
  84. 0084cases hold_witness_witness_witness_right_right_right_right_right
  85. 0085exists x7
  86. 0086exists x8
  87. 0087exists x9
  88. 0088split
  89. 0089exact hold_witness_witness_witness_left
  90. 0090split
  91. 0091specialize hmag_extend_witness_witness_right i
  92. 0092specialize hmag_extend_witness_witness_right x8
  93. 0093apply hmag_extend_witness_witness_right
  94. 0094exact hsplit_right
  95. 0095exact hold_witness_witness_witness_right_left
  96. 0096split
  97. 0097specialize hsign_extend_witness_witness_right i
  98. 0098specialize hsign_extend_witness_witness_right x9
  99. 0099apply hsign_extend_witness_witness_right
  100. 0100exact hsplit_right
  101. 0101exact hold_witness_witness_witness_right_right_left
  102. 0102split
  103. 0103exact hold_witness_witness_witness_right_right_right_left
  104. 0104split
  105. 0105exact hold_witness_witness_witness_right_right_right_right_left
  106. 0106split
  107. 0107exact hold_witness_witness_witness_right_right_right_right_right_left
  108. 0108exact hold_witness_witness_witness_right_right_right_right_right_right