PC0021

binary_split_half_lower_bound

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

Alpha v34 checked-use · first admitted v27 · 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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ N. ∀ h. ∀ d. ∀ m. d = 0 ∨ d = 1 → N = h + h + d → Le(m + m,N) → Le(m,h)

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

Definition DAG

Le(a,b) · 3Lt(a,b) · 1

Actual proof prerequisites

pairing_double_equals_two_mul · checked external prerequisitele_or_lt · checked external prerequisitedoubling_floor_above_implies_double_above_half · checked external prerequisitelt_not_le · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

All 43 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Le(m,h) ∨ Lt(h,m)Definitions: Le(m,h)Lt(h,m)Original native command in the exact edition
  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 defined 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 : Le(m,h) ∨ Lt(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