PA008G

beta_successor_range_reindex_aligned

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

A bounded residue map aligns the range 1,...,n with its successor lift.

Exact expanded PA statement

forall r s b c z d n. (forall fp_i_aligned_bounded. (exists fp_gap_aligned_bounded_index. fp_gap_aligned_bounded_index + S fp_i_aligned_bounded = n) -> exists fp_value_aligned_bounded. ((((exists ff_h_aligned_bounded_entry. ff_h_aligned_bounded_entry + S (fp_value_aligned_bounded) = S ((S (fp_i_aligned_bounded)) * s)) /\ exists ff_q_aligned_bounded_entry. r = ff_q_aligned_bounded_entry * S ((S (fp_i_aligned_bounded)) * s) + (fp_value_aligned_bounded))) /\ (exists fp_gap_aligned_bounded_value. fp_gap_aligned_bounded_value + S fp_value_aligned_bounded = n))) -> (forall ff_i_frp_range_aligned_range. (exists ff_lt_frp_range_aligned_range_bound. ff_lt_frp_range_aligned_range_bound + S ff_i_frp_range_aligned_range = n) -> (((exists ff_h_frp_range_aligned_range_decoded. ff_h_frp_range_aligned_range_decoded + S (1 + ff_i_frp_range_aligned_range) = S ((S (ff_i_frp_range_aligned_range)) * c)) /\ exists ff_q_frp_range_aligned_range_decoded. b = ff_q_frp_range_aligned_range_decoded * S ((S (ff_i_frp_range_aligned_range)) * c) + (1 + ff_i_frp_range_aligned_range)))) -> (forall frr_index_aligned_lift frr_value_aligned_lift. (exists frr_gap_aligned_lift. frr_gap_aligned_lift + S frr_index_aligned_lift = n) -> (((exists ff_h_frr_aligned_lift_source. ff_h_frr_aligned_lift_source + S (frr_value_aligned_lift) = S ((S (frr_index_aligned_lift)) * s)) /\ exists ff_q_frr_aligned_lift_source. r = ff_q_frr_aligned_lift_source * S ((S (frr_index_aligned_lift)) * s) + (frr_value_aligned_lift))) -> (((exists frm_height_frr_aligned_lift_target. frm_height_frr_aligned_lift_target + S (S frr_value_aligned_lift) = S ((S (frr_index_aligned_lift)) * d)) /\ exists frm_quotient_frr_aligned_lift_target. z = frm_quotient_frr_aligned_lift_target * S ((S (frr_index_aligned_lift)) * d) + (S frr_value_aligned_lift)))) -> (forall fpr_i_aligned_result fpr_j_aligned_result fpr_x_aligned_result. (exists fpr_h_aligned_result. fpr_h_aligned_result + S fpr_i_aligned_result = n) -> (((exists ff_h_aligned_result_map. ff_h_aligned_result_map + S (fpr_j_aligned_result) = S ((S (fpr_i_aligned_result)) * s)) /\ exists ff_q_aligned_result_map. r = ff_q_aligned_result_map * S ((S (fpr_i_aligned_result)) * s) + (fpr_j_aligned_result))) -> (((exists ff_h_aligned_result_source. ff_h_aligned_result_source + S (fpr_x_aligned_result) = S ((S (fpr_j_aligned_result)) * c)) /\ exists ff_q_aligned_result_source. b = ff_q_aligned_result_source * S ((S (fpr_j_aligned_result)) * c) + (fpr_x_aligned_result))) -> (((exists ff_h_aligned_result_target. ff_h_aligned_result_target + S (fpr_x_aligned_result) = S ((S (fpr_i_aligned_result)) * d)) /\ exists ff_q_aligned_result_target. z = ff_q_aligned_result_target * S ((S (fpr_i_aligned_result)) * d) + (fpr_x_aligned_result))))

Structural proof guide

Generated structural guide

A bounded residue map aligns the range 1,...,n with its successor lift.

Use the direct prerequisites beta_at_unique, beta_range_one_entry_eq_succ as previously established PA formulas.

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

Referenced ingredients

PA002F beta_at_unique PA008F beta_range_one_entry_eq_succ

Proof neighborhood

Direct dependencies

PA002F beta_at_unique PA008F beta_range_one_entry_eq_succ

Direct dependents

PA008I prime_mul_residue_reindex_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 r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro n
  8. 0008intro hbounded
  9. 0009intro hrange
  10. 0010intro hlift
  11. 0011intro i
  12. 0012intro j
  13. 0013intro value
  14. 0014intro hi
  15. 0015intro hmap
  16. 0016intro hsource
  17. 0017have hbounded_i : exists frr_value_aligned_entry. (((exists ff_h_frr_aligned_entry_entry. ff_h_frr_aligned_entry_entry + S (frr_value_aligned_entry) = S ((S (i)) * s)) /\ exists ff_q_frr_aligned_entry_entry. r = ff_q_frr_aligned_entry_entry * S ((S (i)) * s) + (frr_value_aligned_entry))) /\ (exists frr_gap_aligned_entry. frr_gap_aligned_entry + S frr_value_aligned_entry = n)
  18. 0018specialize hbounded i
  19. 0019apply hbounded
  20. 0020exact hi
  21. 0021cases hbounded_i
  22. 0022cases hbounded_i_witness
  23. 0023have hjx : j = x
  24. 0024specialize beta_at_unique r
  25. 0025specialize beta_at_unique s
  26. 0026specialize beta_at_unique i
  27. 0027specialize beta_at_unique j
  28. 0028specialize beta_at_unique x
  29. 0029apply beta_at_unique
  30. 0030exact hmap
  31. 0031exact hbounded_i_witness_left
  32. 0032have hjbound : exists frr_gap_aligned_j_bound. frr_gap_aligned_j_bound + S j = n
  33. 0033rewrite hjx
  34. 0034exact hbounded_i_witness_right
  35. 0035have hvalue : value = S j
  36. 0036specialize beta_range_one_entry_eq_succ b
  37. 0037specialize beta_range_one_entry_eq_succ c
  38. 0038specialize beta_range_one_entry_eq_succ n
  39. 0039specialize beta_range_one_entry_eq_succ j
  40. 0040specialize beta_range_one_entry_eq_succ value
  41. 0041apply beta_range_one_entry_eq_succ
  42. 0042exact hrange
  43. 0043exact hjbound
  44. 0044exact hsource
  45. 0045have htarget_succ : ((exists frm_height_aligned_target. frm_height_aligned_target + S (S j) = S ((S (i)) * d)) /\ exists frm_quotient_aligned_target. z = frm_quotient_aligned_target * S ((S (i)) * d) + (S j))
  46. 0046specialize hlift i
  47. 0047specialize hlift j
  48. 0048apply hlift
  49. 0049exact hi
  50. 0050exact hmap
  51. 0051rewrite hvalue
  52. 0052rewrite hvalue
  53. 0053exact htarget_succ