PA00DR

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.

Exact expanded 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)

Structural proof guide

Generated structural guide

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

Use the direct prerequisites odd_half_cross_product_gap, le_or_lt, mul_le_mul_left, le_add_right, le_trans, lt_not_le as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (8), equality transport (3).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

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 : exists edt_lt_gap_odd_half_reverse_quotient. edt_lt_gap_odd_half_reverse_quotient + S (k) = d
  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 : exists edt_le_gap_odd_half_divisor_product_le. edt_le_gap_odd_half_divisor_product_le + (p * S k) = p * d
  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 : exists edt_le_gap_odd_half_division_product_le. edt_le_gap_odd_half_division_product_le + (p * d) = q * S i
  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 : exists edt_le_gap_odd_half_source_product_le. edt_le_gap_odd_half_source_product_le + (q * S i) = q * h
  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 : exists edt_le_gap_odd_half_combined_product_le. edt_le_gap_odd_half_combined_product_le + (p * S k) = q * h
11Establish htrans_allL36–40

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

  1. L36
    have htrans_all : forall a b c. (exists t. t + a = b) -> (exists t. t + b = c) -> exists t. t + a = c
  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 : exists t. t + (p * S k) = q * S i
  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 : exists edt_lt_gap_odd_half_shaped_cross_gap. edt_lt_gap_odd_half_shaped_cross_gap + S (q * h) = p * S k
  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 exact 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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