EC0006

euclidean_two_step_halving

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

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

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.

G101 was OPEN when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: the actual anchored Euclidean history, terminal gcd, and exact bound steps≤2*BitLen(b)+1 are proved.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ q. ∀ r. ∀ Q. ∀ t. EuclideanDivision(a,b,q,r) → EuclideanDivision(b,r,Q,t) → EuclideanHalving(b,t)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

EuclideanDivision(a,b,q,r) · 2EuclideanHalving(b,r) · 1

Actual proof prerequisites

euclidean_two_step_quotient_nonzeroeuclidean_add_right_preserves_ltone_le_of_ne_zero · checked external prerequisitele_mul_of_one_le_right · checked external prerequisiteadd_le_add_right · checked external prerequisitelt_of_lt_of_le · checked external prerequisite
Original expanded first-order 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)

Complete unchanged native tactic proof

All 49 lines are the exact independently kernel-checked original script.

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.

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 (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 defined 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