PA007T

beta_magnitude_predecessor_recode_reflect

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

Unique target decoding reflects every predecessor-code entry back to its source successor magnitude.

Exact expanded PA statement

forall mb mc rb rc H l i r. (forall gmp_index_predecessor_transport_range. (exists gsp_lt_gap_predecessor_transport_range_index_bound. gsp_lt_gap_predecessor_transport_range_index_bound + S gmp_index_predecessor_transport_range = l) -> exists gmp_magnitude_predecessor_transport_range. ((((exists ff_h_gmp_predecessor_transport_range_decoded. ff_h_gmp_predecessor_transport_range_decoded + S (gmp_magnitude_predecessor_transport_range) = S ((S (gmp_index_predecessor_transport_range)) * mc)) /\ exists ff_q_gmp_predecessor_transport_range_decoded. mb = ff_q_gmp_predecessor_transport_range_decoded * S ((S (gmp_index_predecessor_transport_range)) * mc) + (gmp_magnitude_predecessor_transport_range))) /\ ((exists gsp_lt_gap_predecessor_transport_range_positive. gsp_lt_gap_predecessor_transport_range_positive + S 0 = gmp_magnitude_predecessor_transport_range) /\ (exists gsp_le_gap_predecessor_transport_range_bounded. gsp_le_gap_predecessor_transport_range_bounded + gmp_magnitude_predecessor_transport_range = H)))) -> (forall gmp_index_predecessor_transport_recode gmp_predecessor_predecessor_transport_recode. (exists gsp_lt_gap_predecessor_transport_recode_index_bound. gsp_lt_gap_predecessor_transport_recode_index_bound + S gmp_index_predecessor_transport_recode = l) -> (((exists gsp_beta_height_gmp_predecessor_transport_recode_source. gsp_beta_height_gmp_predecessor_transport_recode_source + S (S gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_transport_recode_source. mb = gsp_beta_quotient_gmp_predecessor_transport_recode_source * S ((S (gmp_index_predecessor_transport_recode)) * mc) + (S gmp_predecessor_predecessor_transport_recode))) -> (((exists ff_h_gmp_predecessor_transport_recode_target. ff_h_gmp_predecessor_transport_recode_target + S (gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * rc)) /\ exists ff_q_gmp_predecessor_transport_recode_target. rb = ff_q_gmp_predecessor_transport_recode_target * S ((S (gmp_index_predecessor_transport_recode)) * rc) + (gmp_predecessor_predecessor_transport_recode)))) -> (exists gsp_lt_gap_predecessor_transport_index_bound. gsp_lt_gap_predecessor_transport_index_bound + S i = l) -> (((exists ff_h_gmp_predecessor_transport_target_entry. ff_h_gmp_predecessor_transport_target_entry + S (r) = S ((S (i)) * rc)) /\ exists ff_q_gmp_predecessor_transport_target_entry. rb = ff_q_gmp_predecessor_transport_target_entry * S ((S (i)) * rc) + (r))) -> (((exists gsp_beta_height_predecessor_transport_source_entry. gsp_beta_height_predecessor_transport_source_entry + S (S r) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_predecessor_transport_source_entry. mb = gsp_beta_quotient_predecessor_transport_source_entry * S ((S (i)) * mc) + (S r)))

Structural proof guide

Generated structural guide

Unique target decoding reflects every predecessor-code entry back to its source successor magnitude.

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

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

Referenced ingredients

PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA002F beta_at_unique

Direct dependents

PA007U beta_magnitude_predecessor_recode_injective PA007V gauss_predecessor_half_range_aligned PA00B4 finite_bounded_nonendpoint_injective_coverage PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00CS beta_magnitude_predecessor_recode_aligned_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 H
  6. 0006intro l
  7. 0007intro i
  8. 0008intro r
  9. 0009intro hrange
  10. 0010intro hrecode
  11. 0011intro hi
  12. 0012intro htarget
  13. 0013have hentry : exists m. (((exists ff_h_gmp_predecessor_transport_range_entry. ff_h_gmp_predecessor_transport_range_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_gmp_predecessor_transport_range_entry. mb = ff_q_gmp_predecessor_transport_range_entry * S ((S (i)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_transport_positive. gsp_lt_gap_predecessor_transport_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_transport_bounded. gsp_le_gap_predecessor_transport_bounded + m = H))
  14. 0014specialize hrange i
  15. 0015apply hrange
  16. 0016exact hi
  17. 0017cases hentry
  18. 0018cases hentry_witness
  19. 0019cases hentry_witness_right
  20. 0020have hx0 : ~(x = 0)
  21. 0021intro hxzero
  22. 0022specialize ne_zero_of_one_le x
  23. 0023apply ne_zero_of_one_le
  24. 0024exact hentry_witness_right_left
  25. 0025exact hxzero
  26. 0026have hxpredecessor : exists q. x = S q
  27. 0027specialize nonzero_is_succ x
  28. 0028apply nonzero_is_succ
  29. 0029exact hx0
  30. 0030cases hxpredecessor
  31. 0031have hsource_predecessor : ((exists gsp_beta_height_predecessor_transport_source_predecessor. gsp_beta_height_predecessor_transport_source_predecessor + S (S x1) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_predecessor_transport_source_predecessor. mb = gsp_beta_quotient_predecessor_transport_source_predecessor * S ((S (i)) * mc) + (S x1))
  32. 0032rewrite <- hxpredecessor_witness
  33. 0033rewrite <- hxpredecessor_witness
  34. 0034exact hentry_witness_left
  35. 0035have htarget_predecessor : ((exists ff_h_gmp_predecessor_transport_target_predecessor. ff_h_gmp_predecessor_transport_target_predecessor + S (x1) = S ((S (i)) * rc)) /\ exists ff_q_gmp_predecessor_transport_target_predecessor. rb = ff_q_gmp_predecessor_transport_target_predecessor * S ((S (i)) * rc) + (x1))
  36. 0036specialize hrecode i
  37. 0037specialize hrecode x1
  38. 0038apply hrecode
  39. 0039exact hi
  40. 0040exact hsource_predecessor
  41. 0041have hrx : r = x1
  42. 0042specialize beta_at_unique rb
  43. 0043specialize beta_at_unique rc
  44. 0044specialize beta_at_unique i
  45. 0045specialize beta_at_unique r
  46. 0046specialize beta_at_unique x1
  47. 0047apply beta_at_unique
  48. 0048exact htarget
  49. 0049exact htarget_predecessor
  50. 0050have hxsr : x = S r
  51. 0051trans S x1
  52. 0052exact hxpredecessor_witness
  53. 0053congr
  54. 0054symm
  55. 0055exact hrx
  56. 0056rewrite hxsr at hentry_witness_left
  57. 0057rewrite hxsr at hentry_witness_left
  58. 0058exact hentry_witness_left