BT00W7 · Bertrand theorem

linear_square_budget

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A factorized linear budget lies below a square by an explicit gap.

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

∀ a. ∀ q. ∀ r. ∀ t. ∀ c. ∀ k. ∀ d. r = a · q + t → k = q · r + c → d + a · c = t · r → Le(a · k,r · r)

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

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a q r t c k d. r = a * q + t -> k = q * r + c -> d + a * c = t * r -> (exists bqb_le_gap_hj32_linear_square_budget. bqb_le_gap_hj32_linear_square_budget + (a * k) = (r * r))

Proof neighborhood

Direct theorem prerequisites

BT0007 mul_add BT0008 mul_assoc BT0003 add_assoc BT0002 add_comm BT000B add_mul

Direct theorem dependents

BT00W8 bertrand_scaled_budget_root_32 BT00W9 bertrand_scaled_budget_root_33 BT00WA bertrand_scaled_budget_root_34 BT00WB bertrand_scaled_budget_root_35 BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37

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

61 script commands · 11 reading checkpoints · 8 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 (5)
mul addmul assocadd assocadd commadd mul
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro q
  3. L3
    intro r
  4. L4
    intro t
  5. L5
    intro c
  6. L6
    intro k
  7. L7
    intro d
  8. L8
    intro hr
  9. L9
    intro hk
  10. L10
    intro hd
02Construct an explicit witnessL11–11

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

  1. L11
    exists d
03Calculate and transport equalitiesL12–12

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

  1. L12
    rewrite hk
04Establish hmul_addL13–18

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

  1. L13
    have hmul_add : a * (q * r + c) = a * (q * r) + a * c
  2. L14
    specialize mul_add a
  3. L15
    specialize mul_add (q * r)
  4. L16
    specialize mul_add c
  5. L17
    apply mul_add
  6. L18
    rewrite hmul_add
05Establish hassoc_oneL19–25

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

  1. L19
    have hassoc_one : d + (a * (q * r) + a * c) = (d + a * (q * r)) + a * c
  2. L20
    symm
  3. L21
    specialize add_assoc d
  4. L22
    specialize add_assoc (a * (q * r))
  5. L23
    specialize add_assoc (a * c)
  6. L24
    apply add_assoc
  7. L25
    rewrite hassoc_one
06Establish hcomm_oneL26–30

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

  1. L26
    have hcomm_one : d + a * (q * r) = a * (q * r) + d
  2. L27
    specialize add_comm d
  3. L28
    specialize add_comm (a * (q * r))
  4. L29
    apply add_comm
  5. L30
    rewrite hcomm_one
07Establish hassoc_twoL31–36

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

  1. L31
    have hassoc_two : (a * (q * r) + d) + a * c = a * (q * r) + (d + a * c)
  2. L32
    specialize add_assoc (a * (q * r))
  3. L33
    specialize add_assoc d
  4. L34
    specialize add_assoc (a * c)
  5. L35
    apply add_assoc
  6. L36
    rewrite hassoc_two
08Establish hcomm_twoL37–42

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

  1. L37
    have hcomm_two : a * (q * r) + (d + a * c) = (d + a * c) + a * (q * r)
  2. L38
    specialize add_comm (a * (q * r))
  3. L39
    specialize add_comm (d + a * c)
  4. L40
    apply add_comm
  5. L41
    rewrite hcomm_two
  6. L42
    rewrite hd
09Establish hmul_assocL43–48

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

  1. L43
    have hmul_assoc : (a * q) * r = a * (q * r)
  2. L44
    specialize mul_assoc a
  3. L45
    specialize mul_assoc q
  4. L46
    specialize mul_assoc r
  5. L47
    apply mul_assoc
  6. L48
    rewrite <- hmul_assoc
10Establish hadd_mulL49–54

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

  1. L49
    have hadd_mul : (t + a * q) * r = t * r + (a * q) * r
  2. L50
    specialize add_mul t
  3. L51
    specialize add_mul (a * q)
  4. L52
    specialize add_mul r
  5. L53
    apply add_mul
  6. L54
    rewrite <- hadd_mul
11Establish hcomm_threeL55–61

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

  1. L55
    have hcomm_three : t + a * q = a * q + t
  2. L56
    specialize add_comm t
  3. L57
    specialize add_comm (a * q)
  4. L58
    apply add_comm
  5. L59
    rewrite hcomm_three
  6. L60
    rewrite <- hr
  7. L61
    refl

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro a
  2. 0002intro q
  3. 0003intro r
  4. 0004intro t
  5. 0005intro c
  6. 0006intro k
  7. 0007intro d
  8. 0008intro hr
  9. 0009intro hk
  10. 0010intro hd
  11. 0011exists d
  12. 0012rewrite hk
  13. 0013have hmul_add : a * (q * r + c) = a * (q * r) + a * c
  14. 0014specialize mul_add a
  15. 0015specialize mul_add (q * r)
  16. 0016specialize mul_add c
  17. 0017apply mul_add
  18. 0018rewrite hmul_add
  19. 0019have hassoc_one : d + (a * (q * r) + a * c) = (d + a * (q * r)) + a * c
  20. 0020symm
  21. 0021specialize add_assoc d
  22. 0022specialize add_assoc (a * (q * r))
  23. 0023specialize add_assoc (a * c)
  24. 0024apply add_assoc
  25. 0025rewrite hassoc_one
  26. 0026have hcomm_one : d + a * (q * r) = a * (q * r) + d
  27. 0027specialize add_comm d
  28. 0028specialize add_comm (a * (q * r))
  29. 0029apply add_comm
  30. 0030rewrite hcomm_one
  31. 0031have hassoc_two : (a * (q * r) + d) + a * c = a * (q * r) + (d + a * c)
  32. 0032specialize add_assoc (a * (q * r))
  33. 0033specialize add_assoc d
  34. 0034specialize add_assoc (a * c)
  35. 0035apply add_assoc
  36. 0036rewrite hassoc_two
  37. 0037have hcomm_two : a * (q * r) + (d + a * c) = (d + a * c) + a * (q * r)
  38. 0038specialize add_comm (a * (q * r))
  39. 0039specialize add_comm (d + a * c)
  40. 0040apply add_comm
  41. 0041rewrite hcomm_two
  42. 0042rewrite hd
  43. 0043have hmul_assoc : (a * q) * r = a * (q * r)
  44. 0044specialize mul_assoc a
  45. 0045specialize mul_assoc q
  46. 0046specialize mul_assoc r
  47. 0047apply mul_assoc
  48. 0048rewrite <- hmul_assoc
  49. 0049have hadd_mul : (t + a * q) * r = t * r + (a * q) * r
  50. 0050specialize add_mul t
  51. 0051specialize add_mul (a * q)
  52. 0052specialize add_mul r
  53. 0053apply add_mul
  54. 0054rewrite <- hadd_mul
  55. 0055have hcomm_three : t + a * q = a * q + t
  56. 0056specialize add_comm t
  57. 0057specialize add_comm (a * q)
  58. 0058apply add_comm
  59. 0059rewrite hcomm_three
  60. 0060rewrite <- hr
  61. 0061refl