BT0034 · Bertrand theorem

gcd_balanced_bezout_exists_up_to

Stable checked-use theorem · independently kernel verified

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.

Statement with defined notation

∀ B. ∀ b. Le(b,B) → ∀ x. ∃ y. IsGCD(y,x,b) ∧ (∃ z. ∃ n. ∃ m. ∃ k. x · z + b · n = y + (x · m + b · k))

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0006 IsGCD

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0006 IsGCD PD0007 DivRem

7 occurrences

Exact expanded native-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))

Proof neighborhood

Direct theorem prerequisites

BT0000 zero_add BT000Y le_zero BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT001P division_remainder_exists BT002L is_gcd_zero_right BT002S is_gcd_euclid_forward BT0033 balanced_bezout_euclid_step

Direct theorem dependents

BT0035 gcd_balanced_bezout_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 ∨ Lt(b,S B)Definitions: Lt(b,S B)Original native command in the exact edition
  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 : ∃ q. ∃ r. DivRem(a,b,q,r)Definitions: DivRem(a,b,q,r)Original native command in the exact edition
  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
  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 : ∃ d. IsGCD(d,b,x1) ∧ (∃ x. ∃ y. ∃ z. ∃ n. b · x + x1 · y = d + (b · z + x1 · n))Definitions: IsGCD(d,b,x1)Original native command in the exact edition
  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 : ∀ z. ∃ d. IsGCD(d,z,x1) ∧ (∃ x. ∃ y. ∃ n. ∃ m. z · x + x1 · y = d + (z · n + x1 · m))Definitions: IsGCD(d,z,x1)Original native command in the exact edition
  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
  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 : ∀ z. ∃ d. IsGCD(d,z,b) ∧ (∃ x. ∃ y. ∃ n. ∃ m. z · x + b · y = d + (z · n + b · m))Definitions: IsGCD(d,z,b)Original native command in the exact edition
  2. L77
    apply IH
  3. L78
    exact hbB
  4. L79
    specialize hall a
  5. L80
    exact hall

Library-wide reading audit

Original defined 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 ∨ Lt(b,S B)
    Exact native replay linehave 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 : ∃ q. ∃ r. DivRem(a,b,q,r)
    Exact native replay linehave 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 : Le(x1,B)
    Exact native replay linehave 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 : ∃ d. IsGCD(d,b,x1) ∧ (∃ x. ∃ y. ∃ z. ∃ n. b · x + x1 · y = d + (b · z + x1 · n))
    Exact native replay linehave 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 : ∀ z. ∃ d. IsGCD(d,z,x1) ∧ (∃ x. ∃ y. ∃ n. ∃ m. z · x + x1 · y = d + (z · n + x1 · m))
    Exact native replay linehave 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 : Le(b,B)
    Exact native replay linehave hbB : exists k. k + b = B
  73. 0073apply le_of_succ_le_succ
  74. 0074exact hsplit_right
  75. 0075specialize IH b
  76. 0076have hall : ∀ z. ∃ d. IsGCD(d,z,b) ∧ (∃ x. ∃ y. ∃ n. ∃ m. z · x + b · y = d + (z · n + b · m))
    Exact native replay linehave 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