BT0120

bertrand_cover_eighty_three_one_hundred_sixty_three

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

The compact checked cover from 83 to 163.

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

exists bpr_le_gap_bb8c_eighty_three_one_sixty_three. bpr_le_gap_bb8c_eighty_three_one_sixty_three + (13 * 12 + 7) = (9 * 9 + 2 + (9 * 9 + 2))

Structural proof guide

The compact checked cover from 83 to 163.

Direct prerequisites: add_mul, add_assoc, add_comm. The authored body proceeds by intermediate claims (6), equality transport (7), closed numeral normalization (5).

Proof neighborhood

Direct dependencies

BT000B add_mul BT0003 add_assoc BT0002 add_comm

Direct dependents

BT0124 bertrand_small_closed_upper

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

40 script commands · 16 reading checkpoints · 6 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 (3)
add muladd assocadd comm
01Establish h13L1–2

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

  1. L1
    have h13 : 13 = 9 + 4
  2. L2
    norm_num
02Establish h9twelveL3–4

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

  1. L3
    have h9twelve : 9 * 12 = 9 * 9 + 27
  2. L4
    norm_num
03Establish h4twelveL5–6

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

  1. L5
    have h4twelve : 4 * 12 = 48
  2. L6
    norm_num
04Establish hcarrierL7–16

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

  1. L7
    have hcarrier : 13 * 12 + 7 = (9 * 9 + 2) + (8 * 10)
  2. L8
    rewrite h13
  3. L9
    specialize add_mul 9
  4. L10
    specialize add_mul 4
  5. L11
    specialize add_mul 12
  6. L12
    rewrite add_mul
  7. L13
    rewrite h9twelve
  8. L14
    rewrite h4twelve
  9. L15
    trans (9 * 9 + (27 + 48)) + 7
  10. L16
    congr
05Use earlier factsL17–17

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

  1. L17
    apply add_assoc
06Calculate and transport equalitiesL18–19

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

  1. L18
    refl
  2. L19
    trans 9 * 9 + ((27 + 48) + 7)
07Use earlier factsL20–20

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

  1. L20
    apply add_assoc
08Establish htailL21–25

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

  1. L21
    have htail : (27 + 48) + 7 = 2 + (8 * 10)
  2. L22
    norm_num
  3. L23
    rewrite htail
  4. L24
    symm
  5. L25
    apply add_assoc
09Construct an explicit witnessL26–26

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

  1. L26
    exists 3
10Calculate and transport equalitiesL27–29

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

  1. L27
    rewrite hcarrier
  2. L28
    trans (3 + (9 * 9 + 2)) + (8 * 10)
  3. L29
    symm
11Use earlier factsL30–30

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

  1. L30
    apply add_assoc
12Calculate and transport equalitiesL31–32

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

  1. L31
    trans ((9 * 9 + 2) + 3) + (8 * 10)
  2. L32
    congr
13Use earlier factsL33–33

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

  1. L33
    apply add_comm
14Calculate and transport equalitiesL34–35

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

  1. L34
    refl
  2. L35
    trans (9 * 9 + 2) + (3 + (8 * 10))
15Use earlier factsL36–36

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

  1. L36
    apply add_assoc
16Establish hgapL37–40

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

  1. L37
    have hgap : 3 + (8 * 10) = 9 * 9 + 2
  2. L38
    norm_num
  3. L39
    rewrite hgap
  4. L40
    refl

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001have h13 : 13 = 9 + 4
  2. 0002norm_num
  3. 0003have h9twelve : 9 * 12 = 9 * 9 + 27
  4. 0004norm_num
  5. 0005have h4twelve : 4 * 12 = 48
  6. 0006norm_num
  7. 0007have hcarrier : 13 * 12 + 7 = (9 * 9 + 2) + (8 * 10)
  8. 0008rewrite h13
  9. 0009specialize add_mul 9
  10. 0010specialize add_mul 4
  11. 0011specialize add_mul 12
  12. 0012rewrite add_mul
  13. 0013rewrite h9twelve
  14. 0014rewrite h4twelve
  15. 0015trans (9 * 9 + (27 + 48)) + 7
  16. 0016congr
  17. 0017apply add_assoc
  18. 0018refl
  19. 0019trans 9 * 9 + ((27 + 48) + 7)
  20. 0020apply add_assoc
  21. 0021have htail : (27 + 48) + 7 = 2 + (8 * 10)
  22. 0022norm_num
  23. 0023rewrite htail
  24. 0024symm
  25. 0025apply add_assoc
  26. 0026exists 3
  27. 0027rewrite hcarrier
  28. 0028trans (3 + (9 * 9 + 2)) + (8 * 10)
  29. 0029symm
  30. 0030apply add_assoc
  31. 0031trans ((9 * 9 + 2) + 3) + (8 * 10)
  32. 0032congr
  33. 0033apply add_comm
  34. 0034refl
  35. 0035trans (9 * 9 + 2) + (3 + (8 * 10))
  36. 0036apply add_assoc
  37. 0037have hgap : 3 + (8 * 10) = 9 * 9 + 2
  38. 0038norm_num
  39. 0039rewrite hgap
  40. 0040refl