BT00X1

six_block_window_decomposition_above_thirty_two

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

Every s>=32 is a six-step iterate of one base root in the exact window 32..37.

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 s. (exists bqb_le_gap_hjas_decomposition_source. bqb_le_gap_hjas_decomposition_source + (32) = (s)) -> exists b k. (((exists bqb_le_gap_hjas_decomposition_base_lower. bqb_le_gap_hjas_decomposition_base_lower + (32) = (b)) /\ (exists bqb_le_gap_hjas_decomposition_base_upper. bqb_le_gap_hjas_decomposition_base_upper + (b) = (37))) /\ s = b + 6 * k)

Structural proof guide

Every s>=32 is a six-step iterate of one base root in the exact window 32..37.

Direct prerequisites: division_remainder_exists, succ_ne_zero, le_of_succ_le_succ, le_add_right, add_le_add_left, add_assoc, add_comm. The authored body proceeds by case analysis (4), intermediate claims (4), equality transport (1), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT001P division_remainder_exists BT000C succ_ne_zero BT0017 le_of_succ_le_succ BT0013 le_add_right BT0015 add_le_add_left BT0003 add_assoc BT0002 add_comm

Direct dependents

BT00X3 bertrand_hj_envelope_thirty_two

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

57 script commands · 14 reading checkpoints · 4 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)
division remainder existssucc ne zerole of succ le succle add rightadd le add leftadd assocadd comm
01Fix variables and assumptionsL1–2

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

  1. L1
    intro s
  2. L2
    intro hsource
02Separate the logical casesL3–3

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

  1. L3
    cases hsource
03Establish hdivisionL4–11

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

  1. L4
    have hdivision : exists q r. x = 6 * q + r /\ exists h. h + S r = 6
  2. L5
    specialize division_remainder_exists 6
  3. L6
    specialize division_remainder_exists x
  4. L7
    apply division_remainder_exists
  5. L8
    intro hzero
  6. L9
    specialize succ_ne_zero 5
  7. L10
    apply succ_ne_zero
  8. L11
    exact hzero
04Separate the logical casesL12–14

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

  1. L12
    cases hdivision
  2. L13
    cases hdivision_witness
  3. L14
    cases hdivision_witness_witness
05Construct an explicit witnessL15–16

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

  1. L15
    exists 32 + x2
  2. L16
    exists x1
06Separate the logical casesL17–18

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

  1. L17
    split
  2. L18
    split
07Use earlier factsL19–21

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

  1. L19
    specialize le_add_right 32
  2. L20
    specialize le_add_right x2
  3. L21
    exact le_add_right
08Establish hremainderL22–26

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

  1. L22
    have hremainder : exists bqb_le_gap_hjas_decomposition_remainder_le. bqb_le_gap_hjas_decomposition_remainder_le + (x2) = (5)
  2. L23
    specialize le_of_succ_le_succ x2
  3. L24
    specialize le_of_succ_le_succ 5
  4. L25
    apply le_of_succ_le_succ
  5. L26
    exact hdivision_witness_witness_right
09Establish hliftedL27–32

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

  1. L27
    have hlifted : exists bqb_le_gap_hjas_decomposition_lifted_upper. bqb_le_gap_hjas_decomposition_lifted_upper + (32 + x2) = (32 + 5)
  2. L28
    specialize add_le_add_left x2
  3. L29
    specialize add_le_add_left 5
  4. L30
    specialize add_le_add_left 32
  5. L31
    apply add_le_add_left
  6. L32
    exact hremainder
10Establish hthirty_sevenL33–42

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

  1. L33
    have hthirty_seven : 32 + 5 = 37
  2. L34
    norm_num
  3. L35
    rewrite hthirty_seven at hlifted
  4. L36
    exact hlifted
  5. L37
    trans x + 32
  6. L38
    symm
  7. L39
    exact hsource_witness
  8. L40
    trans (6 * x1 + x2) + 32
  9. L41
    congr
  10. L42
    exact hdivision_witness_witness_left
11Calculate and transport equalitiesL43–44

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

  1. L43
    refl
  2. L44
    trans 6 * x1 + (x2 + 32)
12Use earlier factsL45–48

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

  1. L45
    specialize add_assoc (6 * x1)
  2. L46
    specialize add_assoc x2
  3. L47
    specialize add_assoc 32
  4. L48
    apply add_assoc
13Calculate and transport equalitiesL49–51

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

  1. L49
    trans 6 * x1 + (32 + x2)
  2. L50
    congr
  3. L51
    refl
14Use earlier factsL52–57

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

  1. L52
    specialize add_comm x2
  2. L53
    specialize add_comm 32
  3. L54
    apply add_comm
  4. L55
    specialize add_comm (6 * x1)
  5. L56
    specialize add_comm (32 + x2)
  6. L57
    apply add_comm

Library-wide reading audit

Original exact command ledger · 57 lines
  1. 0001intro s
  2. 0002intro hsource
  3. 0003cases hsource
  4. 0004have hdivision : exists q r. x = 6 * q + r /\ exists h. h + S r = 6
  5. 0005specialize division_remainder_exists 6
  6. 0006specialize division_remainder_exists x
  7. 0007apply division_remainder_exists
  8. 0008intro hzero
  9. 0009specialize succ_ne_zero 5
  10. 0010apply succ_ne_zero
  11. 0011exact hzero
  12. 0012cases hdivision
  13. 0013cases hdivision_witness
  14. 0014cases hdivision_witness_witness
  15. 0015exists 32 + x2
  16. 0016exists x1
  17. 0017split
  18. 0018split
  19. 0019specialize le_add_right 32
  20. 0020specialize le_add_right x2
  21. 0021exact le_add_right
  22. 0022have hremainder : exists bqb_le_gap_hjas_decomposition_remainder_le. bqb_le_gap_hjas_decomposition_remainder_le + (x2) = (5)
  23. 0023specialize le_of_succ_le_succ x2
  24. 0024specialize le_of_succ_le_succ 5
  25. 0025apply le_of_succ_le_succ
  26. 0026exact hdivision_witness_witness_right
  27. 0027have hlifted : exists bqb_le_gap_hjas_decomposition_lifted_upper. bqb_le_gap_hjas_decomposition_lifted_upper + (32 + x2) = (32 + 5)
  28. 0028specialize add_le_add_left x2
  29. 0029specialize add_le_add_left 5
  30. 0030specialize add_le_add_left 32
  31. 0031apply add_le_add_left
  32. 0032exact hremainder
  33. 0033have hthirty_seven : 32 + 5 = 37
  34. 0034norm_num
  35. 0035rewrite hthirty_seven at hlifted
  36. 0036exact hlifted
  37. 0037trans x + 32
  38. 0038symm
  39. 0039exact hsource_witness
  40. 0040trans (6 * x1 + x2) + 32
  41. 0041congr
  42. 0042exact hdivision_witness_witness_left
  43. 0043refl
  44. 0044trans 6 * x1 + (x2 + 32)
  45. 0045specialize add_assoc (6 * x1)
  46. 0046specialize add_assoc x2
  47. 0047specialize add_assoc 32
  48. 0048apply add_assoc
  49. 0049trans 6 * x1 + (32 + x2)
  50. 0050congr
  51. 0051refl
  52. 0052specialize add_comm x2
  53. 0053specialize add_comm 32
  54. 0054apply add_comm
  55. 0055specialize add_comm (6 * x1)
  56. 0056specialize add_comm (32 + x2)
  57. 0057apply add_comm