PA00AL

bounded_inverse_index_unique

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

A bounded inverse index is unique.

Exact expanded PA statement

forall p n i j k. p = S n -> (((exists wip_strict_gap_index_unique_left_left_bound. wip_strict_gap_index_unique_left_left_bound + S i = n) /\ ((exists wip_strict_gap_index_unique_left_right_bound. wip_strict_gap_index_unique_left_right_bound + S j = n) /\ (exists wip_mod_left_index_unique_left_inverse wip_mod_right_index_unique_left_inverse. (S i) * S j + p * wip_mod_left_index_unique_left_inverse = 1 + p * wip_mod_right_index_unique_left_inverse)))) -> (((exists wip_strict_gap_index_unique_right_left_bound. wip_strict_gap_index_unique_right_left_bound + S i = n) /\ ((exists wip_strict_gap_index_unique_right_right_bound. wip_strict_gap_index_unique_right_right_bound + S k = n) /\ (exists wip_mod_left_index_unique_right_inverse wip_mod_right_index_unique_right_inverse. (S i) * S k + p * wip_mod_left_index_unique_right_inverse = 1 + p * wip_mod_right_index_unique_right_inverse)))) -> j = k

Structural proof guide

Generated structural guide

A bounded inverse index is unique.

Use the direct prerequisites succ_le_succ, bounded_mod_inverse_unique, succ_injective as previously established PA formulas.

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

Referenced ingredients

PA002K succ_le_succ PA00AK bounded_mod_inverse_unique PA003V succ_injective

Proof neighborhood

Direct dependencies

PA002K succ_le_succ PA00AK bounded_mod_inverse_unique PA003V succ_injective

Direct dependents

PA00AM inverse_prefix_extensional

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 p
  2. 0002intro n
  3. 0003intro i
  4. 0004intro j
  5. 0005intro k
  6. 0006intro hpn
  7. 0007intro hij
  8. 0008intro hik
  9. 0009cases hij
  10. 0010cases hij_right
  11. 0011cases hik
  12. 0012cases hik_right
  13. 0013have hjp : exists wip_successor_gap_index_unique_j_bound. wip_successor_gap_index_unique_j_bound + S (S j) = p
  14. 0014rewrite hpn
  15. 0015specialize succ_le_succ (S j)
  16. 0016specialize succ_le_succ n
  17. 0017apply succ_le_succ
  18. 0018exact hij_right_left
  19. 0019have hkp : exists wip_successor_gap_index_unique_k_bound. wip_successor_gap_index_unique_k_bound + S (S k) = p
  20. 0020rewrite hpn
  21. 0021specialize succ_le_succ (S k)
  22. 0022specialize succ_le_succ n
  23. 0023apply succ_le_succ
  24. 0024exact hik_right_left
  25. 0025have hsucc : S j = S k
  26. 0026specialize bounded_mod_inverse_unique p
  27. 0027specialize bounded_mod_inverse_unique (S i)
  28. 0028specialize bounded_mod_inverse_unique (S j)
  29. 0029specialize bounded_mod_inverse_unique (S k)
  30. 0030apply bounded_mod_inverse_unique
  31. 0031exact hjp
  32. 0032exact hkp
  33. 0033exact hij_right_right
  34. 0034exact hik_right_right
  35. 0035specialize succ_injective j
  36. 0036specialize succ_injective k
  37. 0037apply succ_injective
  38. 0038exact hsucc