PA009Q · theorem

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.

Statement with defined notation

∀ t. ∀ m. Lt(t,m) → Lt(t + t,m + m)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt

2 occurrences

In local proof propositions

PD0001 Le

3 occurrences

Exact expanded native-PA statement
forall t m. (exists h. h + S t = m) -> exists h. h + S (t + t) = m + m

Proof neighborhood

Direct theorem prerequisites

PA000X lt_to_le PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000E add_succ_left

Direct theorem 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

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
  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 : Le(S t + t,m + t)Definitions: Le(S t + t,m + t)Original native command in the exact edition
  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 : Le(m + t,m + m)Definitions: Le(m + t,m + m)Original native command in the exact edition
  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 defined command ledger · 31 lines
  1. 0001intro t
  2. 0002intro m
  3. 0003intro htm
  4. 0004have htle : Le(t,m)
    Exact native replay linehave 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 : Le(S t + t,m + t)
    Exact native replay linehave 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 : Le(m + t,m + m)
    Exact native replay linehave 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