EC0006

euclidean_two_step_halving

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Any two consecutive genuine bounded Euclidean divisions strictly halve the starting divisor: twice the second remainder is smaller.

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 first-order arithmetic statement

forall a b q r Q t. ((a = b * q + r /\ (exists ff_lt_ec_first_division. ff_lt_ec_first_division + S r = b))) -> ((b = r * Q + t /\ (exists ff_lt_ec_second_division. ff_lt_ec_second_division + S t = r))) -> (exists ff_lt_ec_two_step_halving. ff_lt_ec_two_step_halving + S (t + t) = b)

Constructive proof overview

Generated structural guide

Any two consecutive genuine bounded Euclidean divisions strictly halve the starting divisor: twice the second remainder is smaller.

The unchanged tactic script uses 6 declared prerequisites and contains 49 exact native proof lines.

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

EC0005 euclidean_two_step_quotient_nonzero EC0004 euclidean_add_right_preserves_lt one_le_of_ne_zero Stable theorem; checked-use authorized le_mul_of_one_le_right Alpha theorem; checked-use authorized add_le_add_right Stable theorem; checked-use authorized lt_of_lt_of_le Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

49 script commands · 11 reading checkpoints · 5 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 (2)
euclidean two step quotient nonzeroeuclidean add right preserves lt
01Fix variables and assumptionsL1–8

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro Q
  6. L6
    intro t
  7. L7
    intro hfirst
  8. L8
    intro hsecond
02Establish hqL9–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean two step quotient nonzero.

  1. L9
    have hq : ~(Q = 0)
  2. L10
    specialize euclidean_two_step_quotient_nonzero a
  3. L11
    specialize euclidean_two_step_quotient_nonzero b
  4. L12
    specialize euclidean_two_step_quotient_nonzero q
  5. L13
    specialize euclidean_two_step_quotient_nonzero r
  6. L14
    specialize euclidean_two_step_quotient_nonzero Q
  7. L15
    specialize euclidean_two_step_quotient_nonzero t
  8. L16
    intro hzero
  9. L17
    apply euclidean_two_step_quotient_nonzero
  10. L18
    exact hfirst
03Use earlier factsL19–20

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

  1. L19
    exact hsecond
  2. L20
    exact hzero
04Separate the logical casesL21–21

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

  1. L21
    cases hsecond
05Establish honeL22–25

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

  1. L22
    have hone : exists gap. gap + 1 = Q
  2. L23
    specialize one_le_of_ne_zero Q
  3. L24
    apply one_le_of_ne_zero
  4. L25
    exact hq
06Establish hproductL26–30

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

  1. L26
    have hproduct : exists gap. gap + r = r * Q
  2. L27
    specialize le_mul_of_one_le_right r
  3. L28
    specialize le_mul_of_one_le_right Q
  4. L29
    apply le_mul_of_one_le_right
  5. L30
    exact hone
07Establish hsumL31–36

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

  1. L31
    have hsum : exists gap. gap + (r + t) = r * Q + t
  2. L32
    specialize add_le_add_right r
  3. L33
    specialize add_le_add_right (r * Q)
  4. L34
    specialize add_le_add_right t
  5. L35
    apply add_le_add_right
  6. L36
    exact hproduct
08Establish hstrictL37–46

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

  1. L37
    have hstrict : exists gap. gap + S (t + t) = r + t
  2. L38
    specialize euclidean_add_right_preserves_lt t
  3. L39
    specialize euclidean_add_right_preserves_lt r
  4. L40
    specialize euclidean_add_right_preserves_lt t
  5. L41
    apply euclidean_add_right_preserves_lt
  6. L42
    exact hsecond_right
  7. L43
    specialize lt_of_lt_of_le (t + t)
  8. L44
    specialize lt_of_lt_of_le (r + t)
  9. L45
    specialize lt_of_lt_of_le b
  10. L46
    apply lt_of_lt_of_le
09Use earlier factsL47–47

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

  1. L47
    exact hstrict
10Calculate and transport equalitiesL48–48

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

  1. L48
    rewrite hsecond_left
11Use earlier factsL49–49

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

  1. L49
    exact hsum

Library-wide reading audit

Original exact command ledger · 49 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro Q
  6. 0006intro t
  7. 0007intro hfirst
  8. 0008intro hsecond
  9. 0009have hq : ~(Q = 0)
  10. 0010specialize euclidean_two_step_quotient_nonzero a
  11. 0011specialize euclidean_two_step_quotient_nonzero b
  12. 0012specialize euclidean_two_step_quotient_nonzero q
  13. 0013specialize euclidean_two_step_quotient_nonzero r
  14. 0014specialize euclidean_two_step_quotient_nonzero Q
  15. 0015specialize euclidean_two_step_quotient_nonzero t
  16. 0016intro hzero
  17. 0017apply euclidean_two_step_quotient_nonzero
  18. 0018exact hfirst
  19. 0019exact hsecond
  20. 0020exact hzero
  21. 0021cases hsecond
  22. 0022have hone : exists gap. gap + 1 = Q
  23. 0023specialize one_le_of_ne_zero Q
  24. 0024apply one_le_of_ne_zero
  25. 0025exact hq
  26. 0026have hproduct : exists gap. gap + r = r * Q
  27. 0027specialize le_mul_of_one_le_right r
  28. 0028specialize le_mul_of_one_le_right Q
  29. 0029apply le_mul_of_one_le_right
  30. 0030exact hone
  31. 0031have hsum : exists gap. gap + (r + t) = r * Q + t
  32. 0032specialize add_le_add_right r
  33. 0033specialize add_le_add_right (r * Q)
  34. 0034specialize add_le_add_right t
  35. 0035apply add_le_add_right
  36. 0036exact hproduct
  37. 0037have hstrict : exists gap. gap + S (t + t) = r + t
  38. 0038specialize euclidean_add_right_preserves_lt t
  39. 0039specialize euclidean_add_right_preserves_lt r
  40. 0040specialize euclidean_add_right_preserves_lt t
  41. 0041apply euclidean_add_right_preserves_lt
  42. 0042exact hsecond_right
  43. 0043specialize lt_of_lt_of_le (t + t)
  44. 0044specialize lt_of_lt_of_le (r + t)
  45. 0045specialize lt_of_lt_of_le b
  46. 0046apply lt_of_lt_of_le
  47. 0047exact hstrict
  48. 0048rewrite hsecond_left
  49. 0049exact hsum