PA000K

bounded_common_multiple_exists

Stable checked-use theorem · independently closed

Every finite initial interval has a nonzero common-multiple surrogate.

Exact expanded PA statement

forall B. exists c. (~(c = 0) /\ forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k)

Structural proof guide

Generated structural guide

Every finite initial interval has a nonzero common-multiple surrogate.

Use the direct prerequisites bounded_common_multiple_step, succ_ne_zero, add_eq_zero_left as previously established PA formulas.

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

Referenced ingredients

PA000I bounded_common_multiple_step PA0005 succ_ne_zero PA000J add_eq_zero_left

Proof neighborhood

Direct dependencies

PA000I bounded_common_multiple_step PA0005 succ_ne_zero PA000J add_eq_zero_left

Direct dependents

PA002X beta_prefix_extend

Formal native tactic body

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

  1. 0001intro B
  2. 0002induction B
  3. 0003exists 1
  4. 0004split
  5. 0005specialize succ_ne_zero 0
  6. 0006exact succ_ne_zero
  7. 0007intro t
  8. 0008intro ht
  9. 0009cases ht
  10. 0010exfalso
  11. 0011have hz : S t + x = 0
  12. 0012rewrite PA4 at ht_witness
  13. 0013apply PA2
  14. 0014exact ht_witness
  15. 0015have hst0 : S t = 0
  16. 0016specialize add_eq_zero_left (S t)
  17. 0017specialize add_eq_zero_left x
  18. 0018apply add_eq_zero_left
  19. 0019exact hz
  20. 0020specialize succ_ne_zero t
  21. 0021apply succ_ne_zero
  22. 0022exact hst0
  23. 0023cases IH
  24. 0024cases IH_witness
  25. 0025specialize bounded_common_multiple_step B
  26. 0026specialize bounded_common_multiple_step x
  27. 0027apply bounded_common_multiple_step
  28. 0028exact IH_witness_left
  29. 0029exact IH_witness_right