PA009Q

pair_index_left_below_double

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

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

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 t m. (exists h. h + S t = m) -> exists h. h + S (t + t) = m + m

Structural proof guide

Generated structural guide

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

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

The proof proceeds by intermediate claims (4), equality transport (1).

Referenced ingredients

PA000X lt_to_le PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA000X lt_to_le 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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

31 script commands · 6 reading checkpoints · 4 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 (5)
lt to leadd le add rightadd le add leftle transadd succ left
01Fix variables and assumptionsL1–3

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

  1. L1
    intro t
  2. L2
    intro m
  3. L3
    intro htm
02Establish htleL4–8

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

  1. L4
    have htle : exists h. h + t = m
  2. L5
    specialize lt_to_le t
  3. L6
    specialize lt_to_le m
  4. L7
    apply lt_to_le
  5. L8
    exact htm
03Establish hfirstL9–14

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

  1. L9
    have hfirst : exists h. h + (S t + t) = m + t
  2. L10
    specialize add_le_add_right (S t)
  3. L11
    specialize add_le_add_right m
  4. L12
    specialize add_le_add_right t
  5. L13
    apply add_le_add_right
  6. L14
    exact htm
04Establish hsingleL15–19

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

  1. L15
    have hsingle : S t + t = S (t + t)
  2. L16
    specialize add_succ_left t
  3. L17
    specialize add_succ_left t
  4. L18
    exact add_succ_left
  5. L19
    rewrite hsingle at hfirst
05Establish hsecondL20–29

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

  1. L20
    have hsecond : exists h. h + (m + t) = m + m
  2. L21
    specialize add_le_add_left t
  3. L22
    specialize add_le_add_left m
  4. L23
    specialize add_le_add_left m
  5. L24
    apply add_le_add_left
  6. L25
    exact htle
  7. L26
    specialize le_trans (S (t + t))
  8. L27
    specialize le_trans (m + t)
  9. L28
    specialize le_trans (m + m)
  10. L29
    apply le_trans
06Use earlier factsL30–31

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

  1. L30
    exact hfirst
  2. L31
    exact hsecond

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro t
  2. 0002intro m
  3. 0003intro htm
  4. 0004have htle : exists h. h + t = m
  5. 0005specialize lt_to_le t
  6. 0006specialize lt_to_le m
  7. 0007apply lt_to_le
  8. 0008exact htm
  9. 0009have hfirst : exists h. h + (S t + t) = m + t
  10. 0010specialize add_le_add_right (S t)
  11. 0011specialize add_le_add_right m
  12. 0012specialize add_le_add_right t
  13. 0013apply add_le_add_right
  14. 0014exact htm
  15. 0015have hsingle : S t + t = S (t + t)
  16. 0016specialize add_succ_left t
  17. 0017specialize add_succ_left t
  18. 0018exact add_succ_left
  19. 0019rewrite hsingle at hfirst
  20. 0020have hsecond : exists h. h + (m + t) = m + m
  21. 0021specialize add_le_add_left t
  22. 0022specialize add_le_add_left m
  23. 0023specialize add_le_add_left m
  24. 0024apply add_le_add_left
  25. 0025exact htle
  26. 0026specialize le_trans (S (t + t))
  27. 0027specialize le_trans (m + t)
  28. 0028specialize le_trans (m + m)
  29. 0029apply le_trans
  30. 0030exact hfirst
  31. 0031exact hsecond