PA008H

beta_successor_range_scale_mod

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

The range and its successor-lifted residue map are pointwise congruent after scaling.

Exact expanded PA statement

forall p n a r s b c z d. (forall frm_index_scale_map. (exists frm_gap_scale_map_index_bound. frm_gap_scale_map_index_bound + S frm_index_scale_map = n) -> (exists frm_residue_scale_map_result. (exists frm_gap_scale_map_result_residue_bound. frm_gap_scale_map_result_residue_bound + S frm_residue_scale_map_result = n) /\ ((((exists ff_h_frm_scale_map_result_decoded. ff_h_frm_scale_map_result_decoded + S (frm_residue_scale_map_result) = S ((S (frm_index_scale_map)) * s)) /\ exists ff_q_frm_scale_map_result_decoded. r = ff_q_frm_scale_map_result_decoded * S ((S (frm_index_scale_map)) * s) + (frm_residue_scale_map_result))) /\ (exists frm_mod_left_scale_map_result_congruence frm_mod_right_scale_map_result_congruence. a * S frm_index_scale_map + p * frm_mod_left_scale_map_result_congruence = S frm_residue_scale_map_result + p * frm_mod_right_scale_map_result_congruence)))) -> (forall ff_i_frp_range_scale_range. (exists ff_lt_frp_range_scale_range_bound. ff_lt_frp_range_scale_range_bound + S ff_i_frp_range_scale_range = n) -> (((exists ff_h_frp_range_scale_range_decoded. ff_h_frp_range_scale_range_decoded + S (1 + ff_i_frp_range_scale_range) = S ((S (ff_i_frp_range_scale_range)) * c)) /\ exists ff_q_frp_range_scale_range_decoded. b = ff_q_frp_range_scale_range_decoded * S ((S (ff_i_frp_range_scale_range)) * c) + (1 + ff_i_frp_range_scale_range)))) -> (forall frr_index_scale_lift frr_value_scale_lift. (exists frr_gap_scale_lift. frr_gap_scale_lift + S frr_index_scale_lift = n) -> (((exists ff_h_frr_scale_lift_source. ff_h_frr_scale_lift_source + S (frr_value_scale_lift) = S ((S (frr_index_scale_lift)) * s)) /\ exists ff_q_frr_scale_lift_source. r = ff_q_frr_scale_lift_source * S ((S (frr_index_scale_lift)) * s) + (frr_value_scale_lift))) -> (((exists frm_height_frr_scale_lift_target. frm_height_frr_scale_lift_target + S (S frr_value_scale_lift) = S ((S (frr_index_scale_lift)) * d)) /\ exists frm_quotient_frr_scale_lift_target. z = frm_quotient_frr_scale_lift_target * S ((S (frr_index_scale_lift)) * d) + (S frr_value_scale_lift)))) -> (forall fsp_index_scale_result fsp_source_scale_result fsp_target_scale_result. (exists fsp_gap_scale_result. fsp_gap_scale_result + S fsp_index_scale_result = n) -> (((exists fsp_source_height_scale_result. fsp_source_height_scale_result + S (fsp_source_scale_result) = S ((S (fsp_index_scale_result)) * c)) /\ exists fsp_source_quotient_scale_result. b = fsp_source_quotient_scale_result * S ((S (fsp_index_scale_result)) * c) + (fsp_source_scale_result))) -> (((exists fsp_target_height_scale_result. fsp_target_height_scale_result + S (fsp_target_scale_result) = S ((S (fsp_index_scale_result)) * d)) /\ exists fsp_target_quotient_scale_result. z = fsp_target_quotient_scale_result * S ((S (fsp_index_scale_result)) * d) + (fsp_target_scale_result))) -> (exists fsp_mod_left_scale_result fsp_mod_right_scale_result. a * fsp_source_scale_result + p * fsp_mod_left_scale_result = fsp_target_scale_result + p * fsp_mod_right_scale_result))

Structural proof guide

Generated structural guide

The range and its successor-lifted residue map are pointwise congruent after scaling.

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

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

Referenced ingredients

PA008F beta_range_one_entry_eq_succ PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA008F beta_range_one_entry_eq_succ PA002F beta_at_unique

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 p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro r
  5. 0005intro s
  6. 0006intro b
  7. 0007intro c
  8. 0008intro z
  9. 0009intro d
  10. 0010intro hmap
  11. 0011intro hrange
  12. 0012intro hlift
  13. 0013intro i
  14. 0014intro source
  15. 0015intro target
  16. 0016intro hi
  17. 0017intro hsource
  18. 0018intro htarget
  19. 0019have hmi : exists frm_residue_scale_at_i. (exists frm_gap_scale_at_i_residue_bound. frm_gap_scale_at_i_residue_bound + S frm_residue_scale_at_i = n) /\ ((((exists ff_h_frm_scale_at_i_decoded. ff_h_frm_scale_at_i_decoded + S (frm_residue_scale_at_i) = S ((S (i)) * s)) /\ exists ff_q_frm_scale_at_i_decoded. r = ff_q_frm_scale_at_i_decoded * S ((S (i)) * s) + (frm_residue_scale_at_i))) /\ (exists frm_mod_left_scale_at_i_congruence frm_mod_right_scale_at_i_congruence. a * S i + p * frm_mod_left_scale_at_i_congruence = S frm_residue_scale_at_i + p * frm_mod_right_scale_at_i_congruence))
  20. 0020specialize hmap i
  21. 0021apply hmap
  22. 0022exact hi
  23. 0023cases hmi
  24. 0024cases hmi_witness
  25. 0025cases hmi_witness_right
  26. 0026have hsource_value : source = S i
  27. 0027specialize beta_range_one_entry_eq_succ b
  28. 0028specialize beta_range_one_entry_eq_succ c
  29. 0029specialize beta_range_one_entry_eq_succ n
  30. 0030specialize beta_range_one_entry_eq_succ i
  31. 0031specialize beta_range_one_entry_eq_succ source
  32. 0032apply beta_range_one_entry_eq_succ
  33. 0033exact hrange
  34. 0034exact hi
  35. 0035exact hsource
  36. 0036have htarget_succ : ((exists frm_height_scale_target. frm_height_scale_target + S (S x) = S ((S (i)) * d)) /\ exists frm_quotient_scale_target. z = frm_quotient_scale_target * S ((S (i)) * d) + (S x))
  37. 0037specialize hlift i
  38. 0038specialize hlift x
  39. 0039apply hlift
  40. 0040exact hi
  41. 0041exact hmi_witness_right_left
  42. 0042have htarget_value : target = S x
  43. 0043specialize beta_at_unique z
  44. 0044specialize beta_at_unique d
  45. 0045specialize beta_at_unique i
  46. 0046specialize beta_at_unique target
  47. 0047specialize beta_at_unique (S x)
  48. 0048apply beta_at_unique
  49. 0049exact htarget
  50. 0050exact htarget_succ
  51. 0051rewrite hsource_value
  52. 0052rewrite htarget_value
  53. 0053exact hmi_witness_right_right