PA001K

gcd_balanced_bezout_exists_up_to

Stable checked-use theorem · independently closed

Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.

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) /\ exists xp yp xn yn. a * xp + b * yp = d + (a * xn + b * yn))

Structural proof guide

Generated structural guide

Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.

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

The proof proceeds by structural induction (1), case analysis (10), intermediate claims (9), equality transport (4), certified simplification (1).

Referenced ingredients

PA0001 zero_add PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA001D division_remainder_exists PA001F is_gcd_zero_right PA001H is_gcd_euclid_forward PA001J balanced_bezout_euclid_step

Proof neighborhood

Direct dependencies

PA0001 zero_add PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA001D division_remainder_exists PA001F is_gcd_zero_right PA001H is_gcd_euclid_forward PA001J balanced_bezout_euclid_step

Direct dependents

PA001L gcd_balanced_bezout_exists

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

80 script commands · 27 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 (7)
le zerole eq or ltle of succ le succdivision remainder existsis gcd zero rightis gcd euclid forwardbalanced bezout euclid step
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–10

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

  1. L10
    split
06Calculate and transport equalitiesL11–12

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

  1. L11
    rewrite hb0
  2. L12
    rewrite hb0
07Use earlier factsL13–14

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

  1. L13
    specialize is_gcd_zero_right a
  2. L14
    exact is_gcd_zero_right
08Construct an explicit witnessL15–18

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

  1. L15
    exists 1
  2. L16
    exists 0
  3. L17
    exists 0
  4. L18
    exists 0
09Calculate and transport equalitiesL19–20

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

  1. L19
    rewrite hb0
  2. L20
    simp [zero_add]
10Fix variables and assumptionsL21–23

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

  1. L21
    intro b
  2. L22
    intro hb
  3. L23
    intro a
11Use earlier factsL24–25

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

  1. L24
    specialize le_eq_or_lt b
  2. L25
    specialize le_eq_or_lt (S B)
12Establish hsplitL26–28

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

  1. L26
    have hsplit : b = S B \/ exists k. k + S b = S B
  2. L27
    apply le_eq_or_lt
  3. L28
    exact hb
13Separate the logical casesL29–29

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

  1. L29
    cases hsplit
14Establish hb0L30–36

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

  1. L30
    have hb0 : ~(b = 0)
  2. L31
    intro hzero
  3. L32
    apply PA1
  4. L33
    trans b
  5. L34
    symm
  6. L35
    exact hsplit_left
  7. L36
    exact hzero
15Establish hdivL37–39

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

  1. L37
    have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  2. L38
    apply division_remainder_exists
  3. L39
    exact hb0
16Separate the logical casesL40–42

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

  1. L40
    cases hdiv
  2. L41
    cases hdiv_witness
  3. L42
    cases hdiv_witness_witness
17Establish hrBL43–46

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

  1. L43
    have hrB : exists k. k + x1 = B
  2. L44
    apply le_of_succ_le_succ
  3. L45
    rewrite hsplit_left at hdiv_witness_witness_right
  4. L46
    exact hdiv_witness_witness_right
18Establish hsmallL47–48

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

  1. L47
    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) /\ exists xp yp xn yn. b * xp + x1 * yp = d + (b * xn + x1 * yn))
  2. L48
    specialize IH x1
19Establish hallL49–53

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

  1. L49
    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) /\ exists xp yp xn yn. z * xp + x1 * yp = d + (z * xn + x1 * yn))
  2. L50
    apply IH
  3. L51
    exact hrB
  4. L52
    specialize hall b
  5. L53
    exact hall
20Separate the logical casesL54–59

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

  1. L54
    cases hsmall
  2. L55
    cases hsmall_witness
  3. L56
    cases hsmall_witness_right
  4. L57
    cases hsmall_witness_right_witness
  5. L58
    cases hsmall_witness_right_witness_witness
  6. L59
    cases hsmall_witness_right_witness_witness_witness
21Construct an explicit witnessL60–60

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

  1. L60
    exists x2
22Separate the logical casesL61–61

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

  1. L61
    split
23Use earlier factsL62–64

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

  1. L62
    apply is_gcd_euclid_forward
  2. L63
    exact hdiv_witness_witness_left
  3. L64
    exact hsmall_witness_left
24Construct an explicit witnessL65–68

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

  1. L65
    exists x4
  2. L66
    exists x3 + x * x6
  3. L67
    exists x6
  4. L68
    exists x5 + x * x4
25Use earlier factsL69–71

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

  1. L69
    apply balanced_bezout_euclid_step
  2. L70
    exact hdiv_witness_witness_left
  3. L71
    exact hsmall_witness_right_witness_witness_witness_witness
26Establish hbBL72–75

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

  1. L72
    have hbB : exists k. k + b = B
  2. L73
    apply le_of_succ_le_succ
  3. L74
    exact hsplit_right
  4. L75
    specialize IH b
27Establish hallL76–80

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

  1. L76
    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) /\ exists xp yp xn yn. z * xp + b * yp = d + (z * xn + b * yn))
  2. L77
    apply IH
  3. L78
    exact hbB
  4. L79
    specialize hall a
  5. L80
    exact hall

Library-wide reading audit

Original exact command ledger · 80 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. 0011rewrite hb0
  12. 0012rewrite hb0
  13. 0013specialize is_gcd_zero_right a
  14. 0014exact is_gcd_zero_right
  15. 0015exists 1
  16. 0016exists 0
  17. 0017exists 0
  18. 0018exists 0
  19. 0019rewrite hb0
  20. 0020simp [zero_add]
  21. 0021intro b
  22. 0022intro hb
  23. 0023intro a
  24. 0024specialize le_eq_or_lt b
  25. 0025specialize le_eq_or_lt (S B)
  26. 0026have hsplit : b = S B \/ exists k. k + S b = S B
  27. 0027apply le_eq_or_lt
  28. 0028exact hb
  29. 0029cases hsplit
  30. 0030have hb0 : ~(b = 0)
  31. 0031intro hzero
  32. 0032apply PA1
  33. 0033trans b
  34. 0034symm
  35. 0035exact hsplit_left
  36. 0036exact hzero
  37. 0037have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  38. 0038apply division_remainder_exists
  39. 0039exact hb0
  40. 0040cases hdiv
  41. 0041cases hdiv_witness
  42. 0042cases hdiv_witness_witness
  43. 0043have hrB : exists k. k + x1 = B
  44. 0044apply le_of_succ_le_succ
  45. 0045rewrite hsplit_left at hdiv_witness_witness_right
  46. 0046exact hdiv_witness_witness_right
  47. 0047have 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) /\ exists xp yp xn yn. b * xp + x1 * yp = d + (b * xn + x1 * yn))
  48. 0048specialize IH x1
  49. 0049have 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) /\ exists xp yp xn yn. z * xp + x1 * yp = d + (z * xn + x1 * yn))
  50. 0050apply IH
  51. 0051exact hrB
  52. 0052specialize hall b
  53. 0053exact hall
  54. 0054cases hsmall
  55. 0055cases hsmall_witness
  56. 0056cases hsmall_witness_right
  57. 0057cases hsmall_witness_right_witness
  58. 0058cases hsmall_witness_right_witness_witness
  59. 0059cases hsmall_witness_right_witness_witness_witness
  60. 0060exists x2
  61. 0061split
  62. 0062apply is_gcd_euclid_forward
  63. 0063exact hdiv_witness_witness_left
  64. 0064exact hsmall_witness_left
  65. 0065exists x4
  66. 0066exists x3 + x * x6
  67. 0067exists x6
  68. 0068exists x5 + x * x4
  69. 0069apply balanced_bezout_euclid_step
  70. 0070exact hdiv_witness_witness_left
  71. 0071exact hsmall_witness_right_witness_witness_witness_witness
  72. 0072have hbB : exists k. k + b = B
  73. 0073apply le_of_succ_le_succ
  74. 0074exact hsplit_right
  75. 0075specialize IH b
  76. 0076have 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) /\ exists xp yp xn yn. z * xp + b * yp = d + (z * xn + b * yn))
  77. 0077apply IH
  78. 0078exact hbB
  79. 0079specialize hall a
  80. 0080exact hall