PA007V

gauss_predecessor_half_range_aligned

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

The predecessor map aligns canonical factor 1+j with magnitude S j at every position.

Exact expanded PA statement

forall mb mc rb rc b c h. (forall gmp_index_product_magnitude_range. (exists gsp_lt_gap_product_magnitude_range_index_bound. gsp_lt_gap_product_magnitude_range_index_bound + S gmp_index_product_magnitude_range = h) -> exists gmp_magnitude_product_magnitude_range. ((((exists ff_h_gmp_product_magnitude_range_decoded. ff_h_gmp_product_magnitude_range_decoded + S (gmp_magnitude_product_magnitude_range) = S ((S (gmp_index_product_magnitude_range)) * mc)) /\ exists ff_q_gmp_product_magnitude_range_decoded. mb = ff_q_gmp_product_magnitude_range_decoded * S ((S (gmp_index_product_magnitude_range)) * mc) + (gmp_magnitude_product_magnitude_range))) /\ ((exists gsp_lt_gap_product_magnitude_range_positive. gsp_lt_gap_product_magnitude_range_positive + S 0 = gmp_magnitude_product_magnitude_range) /\ (exists gsp_le_gap_product_magnitude_range_bounded. gsp_le_gap_product_magnitude_range_bounded + gmp_magnitude_product_magnitude_range = h)))) -> (forall gmp_index_product_predecessor_recode gmp_predecessor_product_predecessor_recode. (exists gsp_lt_gap_product_predecessor_recode_index_bound. gsp_lt_gap_product_predecessor_recode_index_bound + S gmp_index_product_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_product_predecessor_recode_source. gsp_beta_height_gmp_product_predecessor_recode_source + S (S gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_product_predecessor_recode_source. mb = gsp_beta_quotient_gmp_product_predecessor_recode_source * S ((S (gmp_index_product_predecessor_recode)) * mc) + (S gmp_predecessor_product_predecessor_recode))) -> (((exists ff_h_gmp_product_predecessor_recode_target. ff_h_gmp_product_predecessor_recode_target + S (gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * rc)) /\ exists ff_q_gmp_product_predecessor_recode_target. rb = ff_q_gmp_product_predecessor_recode_target * S ((S (gmp_index_product_predecessor_recode)) * rc) + (gmp_predecessor_product_predecessor_recode)))) -> (forall gsp_range_index_product_canonical_half_range. (exists gsp_lt_gap_product_canonical_half_range_range_bound. gsp_lt_gap_product_canonical_half_range_range_bound + S gsp_range_index_product_canonical_half_range = h) -> (((exists gsp_beta_height_product_canonical_half_range_range_entry. gsp_beta_height_product_canonical_half_range_range_entry + S (1 + gsp_range_index_product_canonical_half_range) = S ((S (gsp_range_index_product_canonical_half_range)) * c)) /\ exists gsp_beta_quotient_product_canonical_half_range_range_entry. b = gsp_beta_quotient_product_canonical_half_range_range_entry * S ((S (gsp_range_index_product_canonical_half_range)) * c) + (1 + gsp_range_index_product_canonical_half_range)))) -> (forall fpr_i_product_alignment fpr_j_product_alignment fpr_x_product_alignment. (exists fpr_h_product_alignment. fpr_h_product_alignment + S fpr_i_product_alignment = h) -> (((exists ff_h_product_alignment_map. ff_h_product_alignment_map + S (fpr_j_product_alignment) = S ((S (fpr_i_product_alignment)) * rc)) /\ exists ff_q_product_alignment_map. rb = ff_q_product_alignment_map * S ((S (fpr_i_product_alignment)) * rc) + (fpr_j_product_alignment))) -> (((exists ff_h_product_alignment_source. ff_h_product_alignment_source + S (fpr_x_product_alignment) = S ((S (fpr_j_product_alignment)) * c)) /\ exists ff_q_product_alignment_source. b = ff_q_product_alignment_source * S ((S (fpr_j_product_alignment)) * c) + (fpr_x_product_alignment))) -> (((exists ff_h_product_alignment_target. ff_h_product_alignment_target + S (fpr_x_product_alignment) = S ((S (fpr_i_product_alignment)) * mc)) /\ exists ff_q_product_alignment_target. mb = ff_q_product_alignment_target * S ((S (fpr_i_product_alignment)) * mc) + (fpr_x_product_alignment))))

Structural proof guide

Generated structural guide

The predecessor map aligns canonical factor 1+j with magnitude S j at every position.

Use the direct prerequisites beta_magnitude_predecessor_recode_bounded, beta_magnitude_predecessor_recode_reflect, beta_at_unique, beta_range_entry_eq, add_succ_left, zero_add as previously established PA formulas.

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

Referenced ingredients

PA007S beta_magnitude_predecessor_recode_bounded PA007T beta_magnitude_predecessor_recode_reflect PA002F beta_at_unique PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add

Proof neighborhood

Direct dependencies

PA007S beta_magnitude_predecessor_recode_bounded PA007T beta_magnitude_predecessor_recode_reflect PA002F beta_at_unique PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add

Direct dependents

PA007Y gauss_magnitude_product_eq_half_range

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 mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro b
  6. 0006intro c
  7. 0007intro h
  8. 0008intro hrange
  9. 0009intro hrecode
  10. 0010intro hhalf
  11. 0011have hbounded : forall fp_i_product_predecessor_bounded. (exists fp_gap_product_predecessor_bounded_index. fp_gap_product_predecessor_bounded_index + S fp_i_product_predecessor_bounded = h) -> exists fp_value_product_predecessor_bounded. ((((exists ff_h_product_predecessor_bounded_entry. ff_h_product_predecessor_bounded_entry + S (fp_value_product_predecessor_bounded) = S ((S (fp_i_product_predecessor_bounded)) * rc)) /\ exists ff_q_product_predecessor_bounded_entry. rb = ff_q_product_predecessor_bounded_entry * S ((S (fp_i_product_predecessor_bounded)) * rc) + (fp_value_product_predecessor_bounded))) /\ (exists fp_gap_product_predecessor_bounded_value. fp_gap_product_predecessor_bounded_value + S fp_value_product_predecessor_bounded = h))
  12. 0012specialize beta_magnitude_predecessor_recode_bounded mb
  13. 0013specialize beta_magnitude_predecessor_recode_bounded mc
  14. 0014specialize beta_magnitude_predecessor_recode_bounded rb
  15. 0015specialize beta_magnitude_predecessor_recode_bounded rc
  16. 0016specialize beta_magnitude_predecessor_recode_bounded h
  17. 0017apply beta_magnitude_predecessor_recode_bounded
  18. 0018exact hrange
  19. 0019exact hrecode
  20. 0020intro i
  21. 0021intro j
  22. 0022intro x
  23. 0023intro hi
  24. 0024intro hmap
  25. 0025intro hsource
  26. 0026have hjdata : exists y. ((((exists ff_h_product_alignment_bounded_entry. ff_h_product_alignment_bounded_entry + S (y) = S ((S (i)) * rc)) /\ exists ff_q_product_alignment_bounded_entry. rb = ff_q_product_alignment_bounded_entry * S ((S (i)) * rc) + (y))) /\ (exists gsp_lt_gap_product_alignment_bounded_value. gsp_lt_gap_product_alignment_bounded_value + S y = h))
  27. 0027specialize hbounded i
  28. 0028apply hbounded
  29. 0029exact hi
  30. 0030cases hjdata
  31. 0031cases hjdata_witness
  32. 0032have hjy : j = x1
  33. 0033specialize beta_at_unique rb
  34. 0034specialize beta_at_unique rc
  35. 0035specialize beta_at_unique i
  36. 0036specialize beta_at_unique j
  37. 0037specialize beta_at_unique x1
  38. 0038apply beta_at_unique
  39. 0039exact hmap
  40. 0040exact hjdata_witness_left
  41. 0041have hj : exists gsp_lt_gap_product_alignment_j_bound. gsp_lt_gap_product_alignment_j_bound + S j = h
  42. 0042rewrite hjy
  43. 0043exact hjdata_witness_right
  44. 0044have hmagnitude : ((exists gsp_beta_height_product_alignment_magnitude_successor. gsp_beta_height_product_alignment_magnitude_successor + S (S j) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_product_alignment_magnitude_successor. mb = gsp_beta_quotient_product_alignment_magnitude_successor * S ((S (i)) * mc) + (S j))
  45. 0045specialize beta_magnitude_predecessor_recode_reflect mb
  46. 0046specialize beta_magnitude_predecessor_recode_reflect mc
  47. 0047specialize beta_magnitude_predecessor_recode_reflect rb
  48. 0048specialize beta_magnitude_predecessor_recode_reflect rc
  49. 0049specialize beta_magnitude_predecessor_recode_reflect h
  50. 0050specialize beta_magnitude_predecessor_recode_reflect h
  51. 0051specialize beta_magnitude_predecessor_recode_reflect i
  52. 0052specialize beta_magnitude_predecessor_recode_reflect j
  53. 0053apply beta_magnitude_predecessor_recode_reflect
  54. 0054exact hrange
  55. 0055exact hrecode
  56. 0056exact hi
  57. 0057exact hmap
  58. 0058have hxraw : x = 1 + j
  59. 0059specialize beta_range_entry_eq b
  60. 0060specialize beta_range_entry_eq c
  61. 0061specialize beta_range_entry_eq 1
  62. 0062specialize beta_range_entry_eq h
  63. 0063specialize beta_range_entry_eq j
  64. 0064specialize beta_range_entry_eq x
  65. 0065apply beta_range_entry_eq
  66. 0066exact hhalf
  67. 0067exact hj
  68. 0068exact hsource
  69. 0069have hone : 1 + j = S j
  70. 0070trans S (0 + j)
  71. 0071specialize add_succ_left 0
  72. 0072specialize add_succ_left j
  73. 0073exact add_succ_left
  74. 0074congr
  75. 0075specialize zero_add j
  76. 0076exact zero_add
  77. 0077have hxsucc : x = S j
  78. 0078trans 1 + j
  79. 0079exact hxraw
  80. 0080exact hone
  81. 0081rewrite hxsucc
  82. 0082rewrite hxsucc
  83. 0083exact hmagnitude