PA00DR · theorem

odd_half_division_quotient_bounded

Alpha v34 checked-use theorem · independently closed; not Stable

A division row from the first odd half has quotient at most the second half.

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

∀ p. ∀ q. ∀ h. ∀ k. ∀ i. ∀ d. ∀ r. p = 2 · h + 1 → q = 2 · k + 1 → Lt(i,h) → q · S i = p · d + r → Le(d,k)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

10 occurrences

Exact expanded native-PA statement
forall p q h k i d r. p = 2 * h + 1 -> q = 2 * k + 1 -> (exists edt_lt_gap_odd_half_quotient_index_bound. edt_lt_gap_odd_half_quotient_index_bound + S (i) = h) -> q * S i = p * d + r -> (exists edt_le_gap_odd_half_quotient_bound. edt_le_gap_odd_half_quotient_bound + (d) = k)

Proof neighborhood

Direct theorem prerequisites

PA00DQ odd_half_cross_product_gap PA003B le_or_lt PA006M mul_le_mul_left PA002S le_add_right PA000R le_trans PA003A lt_not_le

Direct theorem dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

62 script commands · 15 reading checkpoints · 8 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 (6)
odd half cross product gaple or ltmul le mul leftle add rightle translt not le
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro i
  6. L6
    intro d
  7. L7
    intro r
  8. L8
    intro hp
  9. L9
    intro hq
  10. L10
    intro hi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hdivision
03Use earlier factsL12–13

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

  1. L12
    specialize le_or_lt d
  2. L13
    specialize le_or_lt k
04Separate the logical casesL14–14

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

  1. L14
    cases le_or_lt
05Use earlier factsL15–15

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

  1. L15
    exact le_or_lt_left
06Establish hreverseL16–17

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

  1. L16
    have hreverse : Lt(k,d)Definitions: Lt(k,d)Original native command in the exact edition
  2. L17
    exact le_or_lt_right
07Establish hdivisor_leL18–23

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

  1. L18
    have hdivisor_le : Le(p · S k,p · d)Definitions: Le(p · S k,p · d)Original native command in the exact edition
  2. L19
    specialize mul_le_mul_left (S k)
  3. L20
    specialize mul_le_mul_left d
  4. L21
    specialize mul_le_mul_left p
  5. L22
    apply mul_le_mul_left
  6. L23
    exact hreverse
08Establish hdivision_leL24–28

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

  1. L24
    have hdivision_le : Le(p · d,q · S i)Definitions: Le(p · d,q · S i)Original native command in the exact edition
  2. L25
    rewrite hdivision
  3. L26
    specialize le_add_right (p * d)
  4. L27
    specialize le_add_right r
  5. L28
    exact le_add_right
09Establish hsource_leL29–34

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

  1. L29
    have hsource_le : Le(q · S i,q · h)Definitions: Le(q · S i,q · h)Original native command in the exact edition
  2. L30
    specialize mul_le_mul_left (S i)
  3. L31
    specialize mul_le_mul_left h
  4. L32
    specialize mul_le_mul_left q
  5. L33
    apply mul_le_mul_left
  6. L34
    exact hi
10Establish hcombinedL35–35

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

  1. L35
    have hcombined : Le(p · S k,q · h)Definitions: Le(p · S k,q · h)Original native command in the exact edition
11Establish htrans_allL36–40

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

  1. L36
    have htrans_all : ∀ a. ∀ b. ∀ c. Le(a,b) → Le(b,c) → Le(a,c)Definitions: Le(a,b)Le(b,c)Le(a,c)Original native command in the exact edition
  2. L37
    exact le_trans
  3. L38
    specialize le_trans (p * S k)
  4. L39
    specialize le_trans (p * d)
  5. L40
    specialize le_trans (q * S i)
12Establish hfirstL41–50

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

  1. L41
    have hfirst : Le(p · S k,q · S i)Definitions: Le(p · S k,q · S i)Original native command in the exact edition
  2. L42
    apply le_trans
  3. L43
    exact hdivisor_le
  4. L44
    exact hdivision_le
  5. L45
    specialize htrans_all (p * S k)
  6. L46
    specialize htrans_all (q * S i)
  7. L47
    specialize htrans_all (q * h)
  8. L48
    apply htrans_all
  9. L49
    exact hfirst
  10. L50
    exact hsource_le
13Establish hcrossL51–56

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

  1. L51
    have hcross : Lt(q · h,p · S k)Definitions: Lt(q · h,p · S k)Original native command in the exact edition
  2. L52
    rewrite hp
  3. L53
    rewrite hq
  4. L54
    specialize odd_half_cross_product_gap h
  5. L55
    specialize odd_half_cross_product_gap k
  6. L56
    exact odd_half_cross_product_gap
14Separate the logical casesL57–57

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

  1. L57
    exfalso
15Use earlier factsL58–62

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

  1. L58
    specialize lt_not_le (q * h)
  2. L59
    specialize lt_not_le (p * S k)
  3. L60
    apply lt_not_le
  4. L61
    exact hcross
  5. L62
    exact hcombined

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro d
  7. 0007intro r
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hi
  11. 0011intro hdivision
  12. 0012specialize le_or_lt d
  13. 0013specialize le_or_lt k
  14. 0014cases le_or_lt
  15. 0015exact le_or_lt_left
  16. 0016have hreverse : Lt(k,d)
    Exact native replay linehave hreverse : exists edt_lt_gap_odd_half_reverse_quotient. edt_lt_gap_odd_half_reverse_quotient + S (k) = d
  17. 0017exact le_or_lt_right
  18. 0018have hdivisor_le : Le(p · S k,p · d)
    Exact native replay linehave hdivisor_le : exists edt_le_gap_odd_half_divisor_product_le. edt_le_gap_odd_half_divisor_product_le + (p * S k) = p * d
  19. 0019specialize mul_le_mul_left (S k)
  20. 0020specialize mul_le_mul_left d
  21. 0021specialize mul_le_mul_left p
  22. 0022apply mul_le_mul_left
  23. 0023exact hreverse
  24. 0024have hdivision_le : Le(p · d,q · S i)
    Exact native replay linehave hdivision_le : exists edt_le_gap_odd_half_division_product_le. edt_le_gap_odd_half_division_product_le + (p * d) = q * S i
  25. 0025rewrite hdivision
  26. 0026specialize le_add_right (p * d)
  27. 0027specialize le_add_right r
  28. 0028exact le_add_right
  29. 0029have hsource_le : Le(q · S i,q · h)
    Exact native replay linehave hsource_le : exists edt_le_gap_odd_half_source_product_le. edt_le_gap_odd_half_source_product_le + (q * S i) = q * h
  30. 0030specialize mul_le_mul_left (S i)
  31. 0031specialize mul_le_mul_left h
  32. 0032specialize mul_le_mul_left q
  33. 0033apply mul_le_mul_left
  34. 0034exact hi
  35. 0035have hcombined : Le(p · S k,q · h)
    Exact native replay linehave hcombined : exists edt_le_gap_odd_half_combined_product_le. edt_le_gap_odd_half_combined_product_le + (p * S k) = q * h
  36. 0036have htrans_all : ∀ a. ∀ b. ∀ c. Le(a,b) → Le(b,c) → Le(a,c)
    Exact native replay linehave htrans_all : forall a b c. (exists t. t + a = b) -> (exists t. t + b = c) -> exists t. t + a = c
  37. 0037exact le_trans
  38. 0038specialize le_trans (p * S k)
  39. 0039specialize le_trans (p * d)
  40. 0040specialize le_trans (q * S i)
  41. 0041have hfirst : Le(p · S k,q · S i)
    Exact native replay linehave hfirst : exists t. t + (p * S k) = q * S i
  42. 0042apply le_trans
  43. 0043exact hdivisor_le
  44. 0044exact hdivision_le
  45. 0045specialize htrans_all (p * S k)
  46. 0046specialize htrans_all (q * S i)
  47. 0047specialize htrans_all (q * h)
  48. 0048apply htrans_all
  49. 0049exact hfirst
  50. 0050exact hsource_le
  51. 0051have hcross : Lt(q · h,p · S k)
    Exact native replay linehave hcross : exists edt_lt_gap_odd_half_shaped_cross_gap. edt_lt_gap_odd_half_shaped_cross_gap + S (q * h) = p * S k
  52. 0052rewrite hp
  53. 0053rewrite hq
  54. 0054specialize odd_half_cross_product_gap h
  55. 0055specialize odd_half_cross_product_gap k
  56. 0056exact odd_half_cross_product_gap
  57. 0057exfalso
  58. 0058specialize lt_not_le (q * h)
  59. 0059specialize lt_not_le (p * S k)
  60. 0060apply lt_not_le
  61. 0061exact hcross
  62. 0062exact hcombined