PA00BC

pair_order_predecessor_range_two_successor_lift_aligned

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

The predecessor map aligns canonical residues 2+j with successor-lifted PairOrder entries.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall b c r s z d f g l. (forall gmp_index_wtp_alignment_range. (exists gsp_lt_gap_wtp_alignment_range_index_bound. gsp_lt_gap_wtp_alignment_range_index_bound + S gmp_index_wtp_alignment_range = l) -> exists gmp_magnitude_wtp_alignment_range. ((((exists ff_h_gmp_wtp_alignment_range_decoded. ff_h_gmp_wtp_alignment_range_decoded + S (gmp_magnitude_wtp_alignment_range) = S ((S (gmp_index_wtp_alignment_range)) * c)) /\ exists ff_q_gmp_wtp_alignment_range_decoded. b = ff_q_gmp_wtp_alignment_range_decoded * S ((S (gmp_index_wtp_alignment_range)) * c) + (gmp_magnitude_wtp_alignment_range))) /\ ((exists gsp_lt_gap_wtp_alignment_range_positive. gsp_lt_gap_wtp_alignment_range_positive + S 0 = gmp_magnitude_wtp_alignment_range) /\ (exists gsp_le_gap_wtp_alignment_range_bounded. gsp_le_gap_wtp_alignment_range_bounded + gmp_magnitude_wtp_alignment_range = l)))) -> (forall gmp_index_wtp_alignment_recode gmp_predecessor_wtp_alignment_recode. (exists gsp_lt_gap_wtp_alignment_recode_index_bound. gsp_lt_gap_wtp_alignment_recode_index_bound + S gmp_index_wtp_alignment_recode = l) -> (((exists gsp_beta_height_gmp_wtp_alignment_recode_source. gsp_beta_height_gmp_wtp_alignment_recode_source + S (S gmp_predecessor_wtp_alignment_recode) = S ((S (gmp_index_wtp_alignment_recode)) * c)) /\ exists gsp_beta_quotient_gmp_wtp_alignment_recode_source. b = gsp_beta_quotient_gmp_wtp_alignment_recode_source * S ((S (gmp_index_wtp_alignment_recode)) * c) + (S gmp_predecessor_wtp_alignment_recode))) -> (((exists ff_h_gmp_wtp_alignment_recode_target. ff_h_gmp_wtp_alignment_recode_target + S (gmp_predecessor_wtp_alignment_recode) = S ((S (gmp_index_wtp_alignment_recode)) * s)) /\ exists ff_q_gmp_wtp_alignment_recode_target. r = ff_q_gmp_wtp_alignment_recode_target * S ((S (gmp_index_wtp_alignment_recode)) * s) + (gmp_predecessor_wtp_alignment_recode)))) -> (forall wsl_index_wtp_alignment_lift wsl_value_wtp_alignment_lift. (exists wpo_gap_wtp_alignment_lift_bound. wpo_gap_wtp_alignment_lift_bound + S (wsl_index_wtp_alignment_lift) = l) -> (((exists wpo_beta_height_wtp_alignment_lift_source. wpo_beta_height_wtp_alignment_lift_source + S (wsl_value_wtp_alignment_lift) = S ((S (wsl_index_wtp_alignment_lift)) * c)) /\ exists wpo_beta_quotient_wtp_alignment_lift_source. b = wpo_beta_quotient_wtp_alignment_lift_source * S ((S (wsl_index_wtp_alignment_lift)) * c) + (wsl_value_wtp_alignment_lift))) -> (((exists wpo_beta_height_wtp_alignment_lift_target. wpo_beta_height_wtp_alignment_lift_target + S (S wsl_value_wtp_alignment_lift) = S ((S (wsl_index_wtp_alignment_lift)) * g)) /\ exists wpo_beta_quotient_wtp_alignment_lift_target. f = wpo_beta_quotient_wtp_alignment_lift_target * S ((S (wsl_index_wtp_alignment_lift)) * g) + (S wsl_value_wtp_alignment_lift)))) -> (forall wtp_range_index_wtp_alignment_range_two. (exists wtp_range_gap_wtp_alignment_range_two. wtp_range_gap_wtp_alignment_range_two + S wtp_range_index_wtp_alignment_range_two = l) -> (((exists ff_h_wtp_alignment_range_two_decoded. ff_h_wtp_alignment_range_two_decoded + S (2 + wtp_range_index_wtp_alignment_range_two) = S ((S (wtp_range_index_wtp_alignment_range_two)) * d)) /\ exists ff_q_wtp_alignment_range_two_decoded. z = ff_q_wtp_alignment_range_two_decoded * S ((S (wtp_range_index_wtp_alignment_range_two)) * d) + (2 + wtp_range_index_wtp_alignment_range_two)))) -> (forall fpr_i_wtp_alignment fpr_j_wtp_alignment fpr_x_wtp_alignment. (exists fpr_h_wtp_alignment. fpr_h_wtp_alignment + S fpr_i_wtp_alignment = l) -> (((exists ff_h_wtp_alignment_map. ff_h_wtp_alignment_map + S (fpr_j_wtp_alignment) = S ((S (fpr_i_wtp_alignment)) * s)) /\ exists ff_q_wtp_alignment_map. r = ff_q_wtp_alignment_map * S ((S (fpr_i_wtp_alignment)) * s) + (fpr_j_wtp_alignment))) -> (((exists ff_h_wtp_alignment_source. ff_h_wtp_alignment_source + S (fpr_x_wtp_alignment) = S ((S (fpr_j_wtp_alignment)) * d)) /\ exists ff_q_wtp_alignment_source. z = ff_q_wtp_alignment_source * S ((S (fpr_j_wtp_alignment)) * d) + (fpr_x_wtp_alignment))) -> (((exists ff_h_wtp_alignment_target. ff_h_wtp_alignment_target + S (fpr_x_wtp_alignment) = S ((S (fpr_i_wtp_alignment)) * g)) /\ exists ff_q_wtp_alignment_target. f = ff_q_wtp_alignment_target * S ((S (fpr_i_wtp_alignment)) * g) + (fpr_x_wtp_alignment))))

Structural proof guide

Generated structural guide

The predecessor map aligns canonical residues 2+j with successor-lifted PairOrder entries.

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 (9), equality transport (3), certified simplification (1).

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

PA00BD pair_order_terminal_successor_product_eq_range_two

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

86 script commands · 15 reading checkpoints · 9 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
beta magnitude predecessor recode boundedbeta magnitude predecessor recode reflectbeta at uniquebeta range entry eq

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro z
  6. L6
    intro d
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro l
  10. L10
    intro hrange
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hrecode
  2. L12
    intro hlift
  3. L13
    intro hcanonical
03Establish hboundedL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode bounded.

  1. L14
    have hbounded : BoundedPrefix(r,s,l)Definitions: BoundedPrefix
  2. L15
    specialize beta_magnitude_predecessor_recode_bounded b
  3. L16
    specialize beta_magnitude_predecessor_recode_bounded c
  4. L17
    specialize beta_magnitude_predecessor_recode_bounded r
  5. L18
    specialize beta_magnitude_predecessor_recode_bounded s
  6. L19
    specialize beta_magnitude_predecessor_recode_bounded l
  7. L20
    apply beta_magnitude_predecessor_recode_bounded
  8. L21
    exact hrange
  9. L22
    exact hrecode
  10. L23
    intro i
04Fix variables and assumptionsL24–28

Work with arbitrary variables or the premises of the current implication.

  1. L24
    intro j
  2. L25
    intro x
  3. L26
    intro hi
  4. L27
    intro hmap
  5. L28
    intro hsource
05Establish hjdataL29–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbounded.

  1. L29
    have hjdata : exists y. ((((exists ff_h_wtp_alignment_bounded_entry. ff_h_wtp_alignment_bounded_entry + S (y) = S ((S (i)) * s)) /\ exists ff_q_wtp_alignment_bounded_entry. r = ff_q_wtp_alignment_bounded_entry * S ((S (i)) * s) + (y))) /\ (exists wpo_gap_wtp_alignment_bounded_value. wpo_gap_wtp_alignment_bounded_value + S (y) = l))
  2. L30
    specialize hbounded i
  3. L31
    apply hbounded
  4. L32
    exact hi
06Separate the logical casesL33–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L33
    cases hjdata
  2. L34
    cases hjdata_witness
07Establish hjyL35–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L35
    have hjy : j = x1
  2. L36
    specialize beta_at_unique r
  3. L37
    specialize beta_at_unique s
  4. L38
    specialize beta_at_unique i
  5. L39
    specialize beta_at_unique j
  6. L40
    specialize beta_at_unique x1
  7. L41
    apply beta_at_unique
  8. L42
    exact hmap
  9. L43
    exact hjdata_witness_left
08Establish hjL44–46

Establish this local claim before using it. It is not an additional assumption.

  1. L44
    have hj : exists h. h + S j = l
  2. L45
    rewrite hjy
  3. L46
    exact hjdata_witness_right
09Establish horderL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode reflect.

  1. L47
    have horder : ((exists wpo_beta_height_wtp_reflected_order_entry. wpo_beta_height_wtp_reflected_order_entry + S (S j) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_wtp_reflected_order_entry. b = wpo_beta_quotient_wtp_reflected_order_entry * S ((S (i)) * c) + (S j))
  2. L48
    specialize beta_magnitude_predecessor_recode_reflect b
  3. L49
    specialize beta_magnitude_predecessor_recode_reflect c
  4. L50
    specialize beta_magnitude_predecessor_recode_reflect r
  5. L51
    specialize beta_magnitude_predecessor_recode_reflect s
  6. L52
    specialize beta_magnitude_predecessor_recode_reflect l
  7. L53
    specialize beta_magnitude_predecessor_recode_reflect l
  8. L54
    specialize beta_magnitude_predecessor_recode_reflect i
  9. L55
    specialize beta_magnitude_predecessor_recode_reflect j
  10. L56
    apply beta_magnitude_predecessor_recode_reflect
10Use earlier factsL57–60

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L57
    exact hrange
  2. L58
    exact hrecode
  3. L59
    exact hi
  4. L60
    exact hmap
11Establish htargetL61–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hlift.

  1. L61
    have htarget : ((exists wpo_beta_height_wtp_lifted_target_entry. wpo_beta_height_wtp_lifted_target_entry + S (S (S j)) = S ((S (i)) * g)) /\ exists wpo_beta_quotient_wtp_lifted_target_entry. f = wpo_beta_quotient_wtp_lifted_target_entry * S ((S (i)) * g) + (S (S j)))
  2. L62
    specialize hlift i
  3. L63
    specialize hlift (S j)
  4. L64
    apply hlift
  5. L65
    exact hi
  6. L66
    exact horder
12Establish hxrawL67–76

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range entry eq.

  1. L67
    have hxraw : x = 2 + j
  2. L68
    specialize beta_range_entry_eq z
  3. L69
    specialize beta_range_entry_eq d
  4. L70
    specialize beta_range_entry_eq 2
  5. L71
    specialize beta_range_entry_eq l
  6. L72
    specialize beta_range_entry_eq j
  7. L73
    specialize beta_range_entry_eq x
  8. L74
    apply beta_range_entry_eq
  9. L75
    exact hcanonical
  10. L76
    exact hj
13Use earlier factsL77–77

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L77
    exact hsource
14Establish htwoL78–79

Establish this local claim before using it. It is not an additional assumption.

  1. L78
    have htwo : 2 + j = S (S j)
  2. L79
    simp [add_succ_left, zero_add]
15Establish hxsuccL80–86

Establish this local claim before using it. It is not an additional assumption.

  1. L80
    have hxsucc : x = S (S j)
  2. L81
    trans 2 + j
  3. L82
    exact hxraw
  4. L83
    exact htwo
  5. L84
    rewrite hxsucc
  6. L85
    rewrite hxsucc
  7. L86
    exact htarget

Library-wide reading audit

Original exact command ledger · 86 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro r
  4. 0004intro s
  5. 0005intro z
  6. 0006intro d
  7. 0007intro f
  8. 0008intro g
  9. 0009intro l
  10. 0010intro hrange
  11. 0011intro hrecode
  12. 0012intro hlift
  13. 0013intro hcanonical
  14. 0014have hbounded : forall fp_i_wtp_predecessor_bounded. (exists fp_gap_wtp_predecessor_bounded_index. fp_gap_wtp_predecessor_bounded_index + S fp_i_wtp_predecessor_bounded = l) -> exists fp_value_wtp_predecessor_bounded. ((((exists ff_h_wtp_predecessor_bounded_entry. ff_h_wtp_predecessor_bounded_entry + S (fp_value_wtp_predecessor_bounded) = S ((S (fp_i_wtp_predecessor_bounded)) * s)) /\ exists ff_q_wtp_predecessor_bounded_entry. r = ff_q_wtp_predecessor_bounded_entry * S ((S (fp_i_wtp_predecessor_bounded)) * s) + (fp_value_wtp_predecessor_bounded))) /\ (exists fp_gap_wtp_predecessor_bounded_value. fp_gap_wtp_predecessor_bounded_value + S fp_value_wtp_predecessor_bounded = l))
  15. 0015specialize beta_magnitude_predecessor_recode_bounded b
  16. 0016specialize beta_magnitude_predecessor_recode_bounded c
  17. 0017specialize beta_magnitude_predecessor_recode_bounded r
  18. 0018specialize beta_magnitude_predecessor_recode_bounded s
  19. 0019specialize beta_magnitude_predecessor_recode_bounded l
  20. 0020apply beta_magnitude_predecessor_recode_bounded
  21. 0021exact hrange
  22. 0022exact hrecode
  23. 0023intro i
  24. 0024intro j
  25. 0025intro x
  26. 0026intro hi
  27. 0027intro hmap
  28. 0028intro hsource
  29. 0029have hjdata : exists y. ((((exists ff_h_wtp_alignment_bounded_entry. ff_h_wtp_alignment_bounded_entry + S (y) = S ((S (i)) * s)) /\ exists ff_q_wtp_alignment_bounded_entry. r = ff_q_wtp_alignment_bounded_entry * S ((S (i)) * s) + (y))) /\ (exists wpo_gap_wtp_alignment_bounded_value. wpo_gap_wtp_alignment_bounded_value + S (y) = l))
  30. 0030specialize hbounded i
  31. 0031apply hbounded
  32. 0032exact hi
  33. 0033cases hjdata
  34. 0034cases hjdata_witness
  35. 0035have hjy : j = x1
  36. 0036specialize beta_at_unique r
  37. 0037specialize beta_at_unique s
  38. 0038specialize beta_at_unique i
  39. 0039specialize beta_at_unique j
  40. 0040specialize beta_at_unique x1
  41. 0041apply beta_at_unique
  42. 0042exact hmap
  43. 0043exact hjdata_witness_left
  44. 0044have hj : exists h. h + S j = l
  45. 0045rewrite hjy
  46. 0046exact hjdata_witness_right
  47. 0047have horder : ((exists wpo_beta_height_wtp_reflected_order_entry. wpo_beta_height_wtp_reflected_order_entry + S (S j) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_wtp_reflected_order_entry. b = wpo_beta_quotient_wtp_reflected_order_entry * S ((S (i)) * c) + (S j))
  48. 0048specialize beta_magnitude_predecessor_recode_reflect b
  49. 0049specialize beta_magnitude_predecessor_recode_reflect c
  50. 0050specialize beta_magnitude_predecessor_recode_reflect r
  51. 0051specialize beta_magnitude_predecessor_recode_reflect s
  52. 0052specialize beta_magnitude_predecessor_recode_reflect l
  53. 0053specialize beta_magnitude_predecessor_recode_reflect l
  54. 0054specialize beta_magnitude_predecessor_recode_reflect i
  55. 0055specialize beta_magnitude_predecessor_recode_reflect j
  56. 0056apply beta_magnitude_predecessor_recode_reflect
  57. 0057exact hrange
  58. 0058exact hrecode
  59. 0059exact hi
  60. 0060exact hmap
  61. 0061have htarget : ((exists wpo_beta_height_wtp_lifted_target_entry. wpo_beta_height_wtp_lifted_target_entry + S (S (S j)) = S ((S (i)) * g)) /\ exists wpo_beta_quotient_wtp_lifted_target_entry. f = wpo_beta_quotient_wtp_lifted_target_entry * S ((S (i)) * g) + (S (S j)))
  62. 0062specialize hlift i
  63. 0063specialize hlift (S j)
  64. 0064apply hlift
  65. 0065exact hi
  66. 0066exact horder
  67. 0067have hxraw : x = 2 + j
  68. 0068specialize beta_range_entry_eq z
  69. 0069specialize beta_range_entry_eq d
  70. 0070specialize beta_range_entry_eq 2
  71. 0071specialize beta_range_entry_eq l
  72. 0072specialize beta_range_entry_eq j
  73. 0073specialize beta_range_entry_eq x
  74. 0074apply beta_range_entry_eq
  75. 0075exact hcanonical
  76. 0076exact hj
  77. 0077exact hsource
  78. 0078have htwo : 2 + j = S (S j)
  79. 0079simp [add_succ_left, zero_add]
  80. 0080have hxsucc : x = S (S j)
  81. 0081trans 2 + j
  82. 0082exact hxraw
  83. 0083exact htwo
  84. 0084rewrite hxsucc
  85. 0085rewrite hxsucc
  86. 0086exact htarget