BT00W8 · Bertrand theorem

bertrand_scaled_budget_root_32

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

The factorized RFC-v1 H budget at root 32 lies below its square.

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

Le(6 · (4 · 13 + 1 + 4 · 29),32 · 32)

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
exists bqb_le_gap_hj32_scaled_budget_root_32. bqb_le_gap_hj32_scaled_budget_root_32 + (6 * ((4 * 13 + 1) + 4 * 29)) = (32 * 32)

Proof neighborhood

Direct theorem prerequisites

BT00W7 linear_square_budget BT0007 mul_add BT0003 add_assoc BT0002 add_comm

Direct theorem dependents

BT00WP bertrand_h_root_32_from_total

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

60 script commands · 12 reading checkpoints · 10 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 (4)
linear square budgetmul addadd assocadd comm
01Use earlier factsL1–8

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

  1. L1
    specialize linear_square_budget 6
  2. L2
    specialize linear_square_budget 5
  3. L3
    specialize linear_square_budget 32
  4. L4
    specialize linear_square_budget 2
  5. L5
    specialize linear_square_budget 9
  6. L6
    specialize linear_square_budget ((4 * 13 + 1) + 4 * 29)
  7. L7
    specialize linear_square_budget (10)
  8. L8
    apply linear_square_budget
02Calculate and transport equalitiesL9–9

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

  1. L9
    norm_num
03Establish hk_part_oneL10–12

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

  1. L10
    have hk_part_one : 4 * 13 + 1 = 5 * 10 + 3
  2. L11
    norm_num
  3. L12
    rewrite hk_part_one
04Establish hk_part_twoL13–15

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

  1. L13
    have hk_part_two : 4 * 29 = 5 * 22 + 6
  2. L14
    norm_num
  3. L15
    rewrite hk_part_two
05Establish hk_assoc_oneL16–21

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

  1. L16
    have hk_assoc_one : (5 * 10 + 3) + (5 * 22 + 6) = 5 * 10 + (3 + (5 * 22 + 6))
  2. L17
    specialize add_assoc (5 * 10)
  3. L18
    specialize add_assoc 3
  4. L19
    specialize add_assoc (5 * 22 + 6)
  5. L20
    apply add_assoc
  6. L21
    rewrite hk_assoc_one
06Establish hk_assoc_twoL22–28

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

  1. L22
    have hk_assoc_two : 3 + (5 * 22 + 6) = (3 + 5 * 22) + 6
  2. L23
    symm
  3. L24
    specialize add_assoc 3
  4. L25
    specialize add_assoc (5 * 22)
  5. L26
    specialize add_assoc 6
  6. L27
    apply add_assoc
  7. L28
    rewrite hk_assoc_two
07Establish hk_commL29–33

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

  1. L29
    have hk_comm : 3 + 5 * 22 = 5 * 22 + 3
  2. L30
    specialize add_comm 3
  3. L31
    specialize add_comm (5 * 22)
  4. L32
    apply add_comm
  5. L33
    rewrite hk_comm
08Establish hk_assoc_threeL34–39

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

  1. L34
    have hk_assoc_three : (5 * 22 + 3) + 6 = 5 * 22 + (3 + 6)
  2. L35
    specialize add_assoc (5 * 22)
  3. L36
    specialize add_assoc 3
  4. L37
    specialize add_assoc 6
  5. L38
    apply add_assoc
  6. L39
    rewrite hk_assoc_three
09Establish hk_assoc_fourL40–46

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

  1. L40
    have hk_assoc_four : 5 * 10 + (5 * 22 + (3 + 6)) = (5 * 10 + 5 * 22) + (3 + 6)
  2. L41
    symm
  3. L42
    specialize add_assoc (5 * 10)
  4. L43
    specialize add_assoc (5 * 22)
  5. L44
    specialize add_assoc (3 + 6)
  6. L45
    apply add_assoc
  7. L46
    rewrite hk_assoc_four
10Establish hk_factorL47–52

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

  1. L47
    have hk_factor : 5 * (10 + 22) = 5 * 10 + 5 * 22
  2. L48
    specialize mul_add 5
  3. L49
    specialize mul_add 10
  4. L50
    specialize mul_add 22
  5. L51
    apply mul_add
  6. L52
    rewrite <- hk_factor
11Establish hk_rootL53–55

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

  1. L53
    have hk_root : 10 + 22 = 32
  2. L54
    norm_num
  3. L55
    rewrite hk_root
12Establish hk_remainderL56–60

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

  1. L56
    have hk_remainder : 3 + 6 = 9
  2. L57
    norm_num
  3. L58
    rewrite hk_remainder
  4. L59
    refl
  5. L60
    norm_num

Library-wide reading audit

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