PA00CS

beta_magnitude_predecessor_recode_aligned_half_range

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

The magnitude-predecessor code aligns positive magnitudes with the canonical half range.

Exact expanded PA statement

forall b c mb mc rb rc h. (forall gsp_range_index_ges_half. (exists gsp_lt_gap_ges_half_range_bound. gsp_lt_gap_ges_half_range_bound + S gsp_range_index_ges_half = h) -> (((exists gsp_beta_height_ges_half_range_entry. gsp_beta_height_ges_half_range_entry + S (1 + gsp_range_index_ges_half) = S ((S (gsp_range_index_ges_half)) * c)) /\ exists gsp_beta_quotient_ges_half_range_entry. b = gsp_beta_quotient_ges_half_range_entry * S ((S (gsp_range_index_ges_half)) * c) + (1 + gsp_range_index_ges_half)))) -> (forall gmp_index_ges_magnitude_range. (exists gsp_lt_gap_ges_magnitude_range_index_bound. gsp_lt_gap_ges_magnitude_range_index_bound + S gmp_index_ges_magnitude_range = h) -> exists gmp_magnitude_ges_magnitude_range. ((((exists ff_h_gmp_ges_magnitude_range_decoded. ff_h_gmp_ges_magnitude_range_decoded + S (gmp_magnitude_ges_magnitude_range) = S ((S (gmp_index_ges_magnitude_range)) * mc)) /\ exists ff_q_gmp_ges_magnitude_range_decoded. mb = ff_q_gmp_ges_magnitude_range_decoded * S ((S (gmp_index_ges_magnitude_range)) * mc) + (gmp_magnitude_ges_magnitude_range))) /\ ((exists gsp_lt_gap_ges_magnitude_range_positive. gsp_lt_gap_ges_magnitude_range_positive + S 0 = gmp_magnitude_ges_magnitude_range) /\ (exists gsp_le_gap_ges_magnitude_range_bounded. gsp_le_gap_ges_magnitude_range_bounded + gmp_magnitude_ges_magnitude_range = h)))) -> (forall gmp_index_ges_recode gmp_predecessor_ges_recode. (exists gsp_lt_gap_ges_recode_index_bound. gsp_lt_gap_ges_recode_index_bound + S gmp_index_ges_recode = h) -> (((exists gsp_beta_height_gmp_ges_recode_source. gsp_beta_height_gmp_ges_recode_source + S (S gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_ges_recode_source. mb = gsp_beta_quotient_gmp_ges_recode_source * S ((S (gmp_index_ges_recode)) * mc) + (S gmp_predecessor_ges_recode))) -> (((exists ff_h_gmp_ges_recode_target. ff_h_gmp_ges_recode_target + S (gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * rc)) /\ exists ff_q_gmp_ges_recode_target. rb = ff_q_gmp_ges_recode_target * S ((S (gmp_index_ges_recode)) * rc) + (gmp_predecessor_ges_recode)))) -> (forall fpr_i_ges_alignment fpr_j_ges_alignment fpr_x_ges_alignment. (exists fpr_h_ges_alignment. fpr_h_ges_alignment + S fpr_i_ges_alignment = h) -> (((exists ff_h_ges_alignment_map. ff_h_ges_alignment_map + S (fpr_j_ges_alignment) = S ((S (fpr_i_ges_alignment)) * rc)) /\ exists ff_q_ges_alignment_map. rb = ff_q_ges_alignment_map * S ((S (fpr_i_ges_alignment)) * rc) + (fpr_j_ges_alignment))) -> (((exists ff_h_ges_alignment_source. ff_h_ges_alignment_source + S (fpr_x_ges_alignment) = S ((S (fpr_j_ges_alignment)) * c)) /\ exists ff_q_ges_alignment_source. b = ff_q_ges_alignment_source * S ((S (fpr_j_ges_alignment)) * c) + (fpr_x_ges_alignment))) -> (((exists ff_h_ges_alignment_target. ff_h_ges_alignment_target + S (fpr_x_ges_alignment) = S ((S (fpr_i_ges_alignment)) * mc)) /\ exists ff_q_ges_alignment_target. mb = ff_q_ges_alignment_target * S ((S (fpr_i_ges_alignment)) * mc) + (fpr_x_ges_alignment))))

Structural proof guide

Generated structural guide

The magnitude-predecessor code aligns positive magnitudes with the canonical half range.

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

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

Referenced ingredients

PA007T beta_magnitude_predecessor_recode_reflect PA002F beta_at_unique PA000E add_succ_left PA0001 zero_add

Proof neighborhood

Direct dependencies

PA007T beta_magnitude_predecessor_recode_reflect PA002F beta_at_unique PA000E add_succ_left PA0001 zero_add

Direct dependents

PA00CY beta_magnitude_sum_permutation_exact

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 b
  2. 0002intro c
  3. 0003intro mb
  4. 0004intro mc
  5. 0005intro rb
  6. 0006intro rc
  7. 0007intro h
  8. 0008intro hhalf
  9. 0009intro hrange
  10. 0010intro hrecode
  11. 0011intro i
  12. 0012intro j
  13. 0013intro v
  14. 0014intro hi
  15. 0015intro hmap
  16. 0016intro hsource
  17. 0017have hmagnitude_succ : ((exists gsp_beta_height_ges_proof_magnitude_succ. gsp_beta_height_ges_proof_magnitude_succ + S (S j) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_ges_proof_magnitude_succ. mb = gsp_beta_quotient_ges_proof_magnitude_succ * S ((S (i)) * mc) + (S j))
  18. 0018specialize beta_magnitude_predecessor_recode_reflect mb
  19. 0019specialize beta_magnitude_predecessor_recode_reflect mc
  20. 0020specialize beta_magnitude_predecessor_recode_reflect rb
  21. 0021specialize beta_magnitude_predecessor_recode_reflect rc
  22. 0022specialize beta_magnitude_predecessor_recode_reflect h
  23. 0023specialize beta_magnitude_predecessor_recode_reflect h
  24. 0024specialize beta_magnitude_predecessor_recode_reflect i
  25. 0025specialize beta_magnitude_predecessor_recode_reflect j
  26. 0026apply beta_magnitude_predecessor_recode_reflect
  27. 0027exact hrange
  28. 0028exact hrecode
  29. 0029exact hi
  30. 0030exact hmap
  31. 0031have hrange_i : exists m. (((exists ff_h_ges_proof_range_entry. ff_h_ges_proof_range_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_ges_proof_range_entry. mb = ff_q_ges_proof_range_entry * S ((S (i)) * mc) + (m))) /\ ((exists g. g + S 0 = m) /\ exists g. g + m = h)
  32. 0032specialize hrange i
  33. 0033apply hrange
  34. 0034exact hi
  35. 0035cases hrange_i
  36. 0036cases hrange_i_witness
  37. 0037cases hrange_i_witness_right
  38. 0038have hmagnitude_eq : x = S j
  39. 0039specialize beta_at_unique mb
  40. 0040specialize beta_at_unique mc
  41. 0041specialize beta_at_unique i
  42. 0042specialize beta_at_unique x
  43. 0043specialize beta_at_unique (S j)
  44. 0044apply beta_at_unique
  45. 0045exact hrange_i_witness_left
  46. 0046exact hmagnitude_succ
  47. 0047have hj : exists g. g + S j = h
  48. 0048rewrite <- hmagnitude_eq
  49. 0049exact hrange_i_witness_right_right
  50. 0050have hcanonical : ((exists gsp_beta_height_ges_proof_canonical. gsp_beta_height_ges_proof_canonical + S (1 + j) = S ((S (j)) * c)) /\ exists gsp_beta_quotient_ges_proof_canonical. b = gsp_beta_quotient_ges_proof_canonical * S ((S (j)) * c) + (1 + j))
  51. 0051specialize hhalf j
  52. 0052apply hhalf
  53. 0053exact hj
  54. 0054have hv : v = 1 + j
  55. 0055specialize beta_at_unique b
  56. 0056specialize beta_at_unique c
  57. 0057specialize beta_at_unique j
  58. 0058specialize beta_at_unique v
  59. 0059specialize beta_at_unique (1 + j)
  60. 0060apply beta_at_unique
  61. 0061exact hsource
  62. 0062exact hcanonical
  63. 0063have hone : 1 + j = S j
  64. 0064specialize add_succ_left 0
  65. 0065specialize add_succ_left j
  66. 0066trans S (0 + j)
  67. 0067exact add_succ_left
  68. 0068congr
  69. 0069specialize zero_add j
  70. 0070exact zero_add
  71. 0071have hv_succ : v = S j
  72. 0072trans 1 + j
  73. 0073exact hv
  74. 0074exact hone
  75. 0075rewrite <- hv_succ at hmagnitude_succ
  76. 0076rewrite <- hv_succ at hmagnitude_succ
  77. 0077exact hmagnitude_succ