PA0035

gcd_exists_up_to

Stable checked-use theorem · independently closed

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

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 B b. (exists t. t + b = B) -> forall a. exists d. (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

Structural proof guide

Generated structural guide

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

Use the direct prerequisites multiple_refl, le_zero, le_eq_or_lt, le_of_succ_le_succ, division_remainder_exists, is_gcd_euclid_forward as previously established PA formulas.

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

Referenced ingredients

PA0019 multiple_refl PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA001D division_remainder_exists PA001H is_gcd_euclid_forward

Proof neighborhood

Direct dependencies

PA0019 multiple_refl PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA001D division_remainder_exists PA001H is_gcd_euclid_forward

Direct dependents

PA0036 gcd_exists_relational

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.

Read the argument

Proof checkpoints

74 script commands · 28 reading checkpoints · 9 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 (6)
multiple reflle zerole eq or ltle of succ le succdivision remainder existsis gcd euclid forward
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro b
  3. L4
    intro hb
  4. L5
    intro a
03Establish hb0L6–8

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

  1. L6
    have hb0 : b = 0
  2. L7
    apply le_zero
  3. L8
    exact hb
04Construct an explicit witnessL9–9

Supply the displayed value, then prove that it has the required property.

  1. L9
    exists a
05Separate the logical casesL10–11

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    split
  2. L11
    split
06Use earlier factsL12–13

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

  1. L12
    specialize multiple_refl a
  2. L13
    exact multiple_refl
07Construct an explicit witnessL14–14

Supply the displayed value, then prove that it has the required property.

  1. L14
    exists 0
08Calculate and transport equalitiesL15–15

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L15
    trans 0
09Use earlier factsL16–16

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

  1. L16
    exact hb0
10Calculate and transport equalitiesL17–17

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L17
    symm
11Use earlier factsL18–18

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

  1. L18
    apply PA5
12Fix variables and assumptionsL19–21

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

  1. L19
    intro c
  2. L20
    intro hca
  3. L21
    intro hcb
13Use earlier factsL22–22

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

  1. L22
    exact hca
14Fix variables and assumptionsL23–25

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

  1. L23
    intro b
  2. L24
    intro hb
  3. L25
    intro a
15Use earlier factsL26–27

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

  1. L26
    specialize le_eq_or_lt b
  2. L27
    specialize le_eq_or_lt (S B)
16Establish hsplitL28–30

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

  1. L28
    have hsplit : b = S B \/ exists k. k + S b = S B
  2. L29
    apply le_eq_or_lt
  3. L30
    exact hb
17Separate the logical casesL31–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    cases hsplit
18Establish hb0L32–38

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

  1. L32
    have hb0 : ~(b = 0)
  2. L33
    intro hzero
  3. L34
    apply PA1
  4. L35
    trans b
  5. L36
    symm
  6. L37
    exact hsplit_left
  7. L38
    exact hzero
19Establish hdivL39–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L39
    have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  2. L40
    apply division_remainder_exists
  3. L41
    exact hb0
20Separate the logical casesL42–44

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L42
    cases hdiv
  2. L43
    cases hdiv_witness
  3. L44
    cases hdiv_witness_witness
21Establish hrBL45–48

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

  1. L45
    have hrB : exists k. k + x1 = B
  2. L46
    apply le_of_succ_le_succ
  3. L47
    rewrite hsplit_left at hdiv_witness_witness_right
  4. L48
    exact hdiv_witness_witness_right
22Establish hsmallL49–50

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

  1. L49
    have hsmall : exists d. (((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  2. L50
    specialize IH x1
23Establish hallL51–55

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

  1. L51
    have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  2. L52
    apply IH
  3. L53
    exact hrB
  4. L54
    specialize hall b
  5. L55
    exact hall
24Separate the logical casesL56–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L56
    cases hsmall
25Construct an explicit witnessL57–57

Supply the displayed value, then prove that it has the required property.

  1. L57
    exists x2
26Use earlier factsL58–65

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

  1. L58
    specialize is_gcd_euclid_forward x2
  2. L59
    specialize is_gcd_euclid_forward a
  3. L60
    specialize is_gcd_euclid_forward b
  4. L61
    specialize is_gcd_euclid_forward x
  5. L62
    specialize is_gcd_euclid_forward x1
  6. L63
    apply is_gcd_euclid_forward
  7. L64
    exact hdiv_witness_witness_left
  8. L65
    exact hsmall_witness
27Establish hbBL66–69

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

  1. L66
    have hbB : exists k. k + b = B
  2. L67
    apply le_of_succ_le_succ
  3. L68
    exact hsplit_right
  4. L69
    specialize IH b
28Establish hallL70–74

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

  1. L70
    have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w)
  2. L71
    apply IH
  3. L72
    exact hbB
  4. L73
    specialize hall a
  5. L74
    exact hall

Library-wide reading audit

Original exact command ledger · 74 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro b
  4. 0004intro hb
  5. 0005intro a
  6. 0006have hb0 : b = 0
  7. 0007apply le_zero
  8. 0008exact hb
  9. 0009exists a
  10. 0010split
  11. 0011split
  12. 0012specialize multiple_refl a
  13. 0013exact multiple_refl
  14. 0014exists 0
  15. 0015trans 0
  16. 0016exact hb0
  17. 0017symm
  18. 0018apply PA5
  19. 0019intro c
  20. 0020intro hca
  21. 0021intro hcb
  22. 0022exact hca
  23. 0023intro b
  24. 0024intro hb
  25. 0025intro a
  26. 0026specialize le_eq_or_lt b
  27. 0027specialize le_eq_or_lt (S B)
  28. 0028have hsplit : b = S B \/ exists k. k + S b = S B
  29. 0029apply le_eq_or_lt
  30. 0030exact hb
  31. 0031cases hsplit
  32. 0032have hb0 : ~(b = 0)
  33. 0033intro hzero
  34. 0034apply PA1
  35. 0035trans b
  36. 0036symm
  37. 0037exact hsplit_left
  38. 0038exact hzero
  39. 0039have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  40. 0040apply division_remainder_exists
  41. 0041exact hb0
  42. 0042cases hdiv
  43. 0043cases hdiv_witness
  44. 0044cases hdiv_witness_witness
  45. 0045have hrB : exists k. k + x1 = B
  46. 0046apply le_of_succ_le_succ
  47. 0047rewrite hsplit_left at hdiv_witness_witness_right
  48. 0048exact hdiv_witness_witness_right
  49. 0049have hsmall : exists d. (((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  50. 0050specialize IH x1
  51. 0051have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  52. 0052apply IH
  53. 0053exact hrB
  54. 0054specialize hall b
  55. 0055exact hall
  56. 0056cases hsmall
  57. 0057exists x2
  58. 0058specialize is_gcd_euclid_forward x2
  59. 0059specialize is_gcd_euclid_forward a
  60. 0060specialize is_gcd_euclid_forward b
  61. 0061specialize is_gcd_euclid_forward x
  62. 0062specialize is_gcd_euclid_forward x1
  63. 0063apply is_gcd_euclid_forward
  64. 0064exact hdiv_witness_witness_left
  65. 0065exact hsmall_witness
  66. 0066have hbB : exists k. k + b = B
  67. 0067apply le_of_succ_le_succ
  68. 0068exact hsplit_right
  69. 0069specialize IH b
  70. 0070have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w)
  71. 0071apply IH
  72. 0072exact hbB
  73. 0073specialize hall a
  74. 0074exact hall