PC0021

binary_split_half_lower_bound

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

A lower bound on a doubled input reflects to its actual binary quotient, including either remainder bit.

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 N h d m. (d = 0 \/ d = 1) -> N = (h + h) + d -> (exists pc_le_half_lower_input. pc_le_half_lower_input + (m + m) = (N)) -> (exists pc_le_half_lower_result. pc_le_half_lower_result + (m) = (h))

Constructive proof overview

Generated structural guide

A lower bound on a doubled input reflects to its actual binary quotient, including either remainder bit.

The unchanged tactic script uses 4 declared prerequisites and contains 43 exact native proof lines.

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

Proof neighborhood

Direct dependencies

pairing_double_equals_two_mul Alpha theorem; checked-use authorized le_or_lt Stable theorem; checked-use authorized doubling_floor_above_implies_double_above_half Alpha theorem; checked-use authorized lt_not_le Stable theorem; checked-use authorized

Direct dependents

PC0026 binary_half_scale_bounds PC002F prime_count_chebyshev_lower_large

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

43 script commands · 13 reading checkpoints · 4 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.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro N
  2. L2
    intro h
  3. L3
    intro d
  4. L4
    intro m
  5. L5
    intro hd
  6. L6
    intro hN
  7. L7
    intro hm
02Establish heqL8–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pairing double equals two mul.

  1. L8
    have heq : h + h = 2 * h
  2. L9
    specialize pairing_double_equals_two_mul h
  3. L10
    apply pairing_double_equals_two_mul
03Establish hrepL11–11

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

  1. L11
    have hrep : N = 2 * h \/ N = 2 * h + 1
04Separate the logical casesL12–13

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

  1. L12
    cases hd
  2. L13
    left
05Calculate and transport equalitiesL14–17

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

  1. L14
    rewrite hN
  2. L15
    rewrite hd_left
  3. L16
    rewrite heq
  4. L17
    simp
06Separate the logical casesL18–18

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

  1. L18
    right
07Calculate and transport equalitiesL19–22

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

  1. L19
    rewrite hN
  2. L20
    rewrite hd_right
  3. L21
    rewrite heq
  4. L22
    refl
08Establish hsL23–26

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

  1. L23
    have hs : (exists g. g + m = h) \/ (exists g. g + S h = m)
  2. L24
    specialize le_or_lt m
  3. L25
    specialize le_or_lt h
  4. L26
    apply le_or_lt
09Separate the logical casesL27–27

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

  1. L27
    cases hs
10Use earlier factsL28–28

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

  1. L28
    exact hs_left
11Separate the logical casesL29–29

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

  1. L29
    exfalso
12Use earlier factsL30–38

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

  1. L30
    specialize lt_not_le N
  2. L31
    specialize lt_not_le (2 * m)
  3. L32
    apply lt_not_le
  4. L33
    specialize doubling_floor_above_implies_double_above_half N
  5. L34
    specialize doubling_floor_above_implies_double_above_half h
  6. L35
    specialize doubling_floor_above_implies_double_above_half m
  7. L36
    apply doubling_floor_above_implies_double_above_half
  8. L37
    exact hrep
  9. L38
    exact hs_right
13Establish hmeqL39–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pairing double equals two mul.

  1. L39
    have hmeq : m + m = 2 * m
  2. L40
    specialize pairing_double_equals_two_mul m
  3. L41
    apply pairing_double_equals_two_mul
  4. L42
    rewrite hmeq at hm
  5. L43
    exact hm

Library-wide reading audit

Original exact command ledger · 43 lines
  1. 0001intro N
  2. 0002intro h
  3. 0003intro d
  4. 0004intro m
  5. 0005intro hd
  6. 0006intro hN
  7. 0007intro hm
  8. 0008have heq : h + h = 2 * h
  9. 0009specialize pairing_double_equals_two_mul h
  10. 0010apply pairing_double_equals_two_mul
  11. 0011have hrep : N = 2 * h \/ N = 2 * h + 1
  12. 0012cases hd
  13. 0013left
  14. 0014rewrite hN
  15. 0015rewrite hd_left
  16. 0016rewrite heq
  17. 0017simp
  18. 0018right
  19. 0019rewrite hN
  20. 0020rewrite hd_right
  21. 0021rewrite heq
  22. 0022refl
  23. 0023have hs : (exists g. g + m = h) \/ (exists g. g + S h = m)
  24. 0024specialize le_or_lt m
  25. 0025specialize le_or_lt h
  26. 0026apply le_or_lt
  27. 0027cases hs
  28. 0028exact hs_left
  29. 0029exfalso
  30. 0030specialize lt_not_le N
  31. 0031specialize lt_not_le (2 * m)
  32. 0032apply lt_not_le
  33. 0033specialize doubling_floor_above_implies_double_above_half N
  34. 0034specialize doubling_floor_above_implies_double_above_half h
  35. 0035specialize doubling_floor_above_implies_double_above_half m
  36. 0036apply doubling_floor_above_implies_double_above_half
  37. 0037exact hrep
  38. 0038exact hs_right
  39. 0039have hmeq : m + m = 2 * m
  40. 0040specialize pairing_double_equals_two_mul m
  41. 0041apply pairing_double_equals_two_mul
  42. 0042rewrite hmeq at hm
  43. 0043exact hm