BT004N

bounded_common_multiple_exists

Stable · empty-context checked

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

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

Direct prerequisites: bounded_common_multiple_step, succ_ne_zero, add_eq_zero_left. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT004M bounded_common_multiple_step BT000C succ_ne_zero BT001X add_eq_zero_left

Direct dependents

BT005D beta_prefix_extend

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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