PA009R

pair_index_right_below_double

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

The right position of an earlier pair lies below the doubled prefix.

Exact expanded PA statement

forall t m. (exists h. h + S t = m) -> exists h. h + S (S (t + t)) = m + m

Structural proof guide

Generated structural guide

The right position of an earlier pair lies below the doubled prefix.

Use the direct prerequisites add_le_add_right, add_le_add_left, le_trans, add_succ_left as previously established PA formulas.

The proof proceeds by intermediate claims (3), equality transport (1), certified simplification (1).

Referenced ingredients

PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000E add_succ_left

Direct dependents

PA009S adjacent_scaled_orbit_history_append PA009X scaled_pair_order_successor_lift_adjacent_targets PA00AY paired_inverse_witness_append PA00B7 paired_successor_lift_adjacent_units

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 t
  2. 0002intro m
  3. 0003intro htm
  4. 0004have hfirst : exists h. h + (S t + S t) = m + S t
  5. 0005specialize add_le_add_right (S t)
  6. 0006specialize add_le_add_right m
  7. 0007specialize add_le_add_right (S t)
  8. 0008apply add_le_add_right
  9. 0009exact htm
  10. 0010have hdouble : S (S (t + t)) = S t + S t
  11. 0011simp [add_succ_left]
  12. 0012rewrite <- hdouble at hfirst
  13. 0013have hsecond : exists h. h + (m + S t) = m + m
  14. 0014specialize add_le_add_left (S t)
  15. 0015specialize add_le_add_left m
  16. 0016specialize add_le_add_left m
  17. 0017apply add_le_add_left
  18. 0018exact htm
  19. 0019specialize le_trans (S (S (t + t)))
  20. 0020specialize le_trans (m + S t)
  21. 0021specialize le_trans (m + m)
  22. 0022apply le_trans
  23. 0023exact hfirst
  24. 0024exact hsecond