BT00Y9

division_quotient_two_of_bounds

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

Bounds between two and three divisors force quotient two.

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 d n. (exists bcf_le_gap_bdqtb_lower. bcf_le_gap_bdqtb_lower + (d + d) = n) -> (exists bcf_lt_gap_bdqtb_upper. bcf_lt_gap_bdqtb_upper + S (n) = (d + d) + d) -> exists r. (((n) = (d) * (2) + (r) /\ (exists bcf_lt_gap_bdqtb_result_bound. bcf_lt_gap_bdqtb_result_bound + S (r) = d)))

Structural proof guide

Bounds between two and three divisors force quotient two.

Direct prerequisites: add_comm, mul_one, add_lt_cancel_left. The authored body proceeds by case analysis (1), intermediate claims (2), equality transport (3).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT000A mul_one BT00XC add_lt_cancel_left

Direct dependents

BT00YB division_first_two_of_two_three_range

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

28 script commands · 12 reading checkpoints · 2 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 (3)
add commmul oneadd lt cancel left
01Fix variables and assumptionsL1–4

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro hlower
  4. L4
    intro hupper
02Separate the logical casesL5–5

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

  1. L5
    cases hlower
03Establish hsumL6–9

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

  1. L6
    have hsum : (d + d) + x = n
  2. L7
    trans x + (d + d)
  3. L8
    apply add_comm
  4. L9
    exact hlower_witness
04Establish hremainderL10–16

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

  1. L10
    have hremainder : exists bcf_lt_gap_bdqtb_remainder. bcf_lt_gap_bdqtb_remainder + S (x) = d
  2. L11
    rewrite <- hsum at hupper
  3. L12
    specialize add_lt_cancel_left (d + d)
  4. L13
    specialize add_lt_cancel_left x
  5. L14
    specialize add_lt_cancel_left d
  6. L15
    apply add_lt_cancel_left
  7. L16
    exact hupper
05Construct an explicit witnessL17–17

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

  1. L17
    exists x
06Separate the logical casesL18–18

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

  1. L18
    split
07Calculate and transport equalitiesL19–20

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

  1. L19
    trans (d + d) + x
  2. L20
    symm
08Use earlier factsL21–21

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

  1. L21
    exact hsum
09Calculate and transport equalitiesL22–23

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

  1. L22
    congr
  2. L23
    rewrite PA6
10Use earlier factsL24–24

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

  1. L24
    specialize mul_one d
11Calculate and transport equalitiesL25–27

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

  1. L25
    rewrite mul_one
  2. L26
    refl
  3. L27
    refl
12Use earlier factsL28–28

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

  1. L28
    exact hremainder

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro hlower
  4. 0004intro hupper
  5. 0005cases hlower
  6. 0006have hsum : (d + d) + x = n
  7. 0007trans x + (d + d)
  8. 0008apply add_comm
  9. 0009exact hlower_witness
  10. 0010have hremainder : exists bcf_lt_gap_bdqtb_remainder. bcf_lt_gap_bdqtb_remainder + S (x) = d
  11. 0011rewrite <- hsum at hupper
  12. 0012specialize add_lt_cancel_left (d + d)
  13. 0013specialize add_lt_cancel_left x
  14. 0014specialize add_lt_cancel_left d
  15. 0015apply add_lt_cancel_left
  16. 0016exact hupper
  17. 0017exists x
  18. 0018split
  19. 0019trans (d + d) + x
  20. 0020symm
  21. 0021exact hsum
  22. 0022congr
  23. 0023rewrite PA6
  24. 0024specialize mul_one d
  25. 0025rewrite mul_one
  26. 0026refl
  27. 0027refl
  28. 0028exact hremainder