BT00VS

odd_positive_prefix_predecessor_bound

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

The positive prefix half of an odd successor is smaller.

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 n k. S n = 2 * k + 1 -> (exists h. k = S h) -> (exists bcf_le_gap_boppb_result. bcf_le_gap_boppb_result + (S k) = n)

Structural proof guide

The positive prefix half of an odd successor is smaller.

Direct prerequisites: two_mul_eq_add_self, add_succ_left. The authored body proceeds by structural induction (1), case analysis (1).

Proof neighborhood

Direct dependencies

BT00QU two_mul_eq_add_self BT0001 add_succ_left

Direct dependents

BT00VV primorial_le_four_pow_bounded

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

17 script commands · 11 reading checkpoints · 0 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–1

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

  1. L1
    intro n
02Induction on kL2–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction k
  2. L3
    intro heq
  3. L4
    intro hpositive
03Separate the logical casesL5–6

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

  1. L5
    cases hpositive
  2. L6
    exfalso
04Use earlier factsL7–7

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

  1. L7
    apply PA1
05Calculate and transport equalitiesL8–8

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

  1. L8
    symm
06Use earlier factsL9–9

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

  1. L9
    exact hpositive_witness
07Fix variables and assumptionsL10–11

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

  1. L10
    intro heq
  2. L11
    intro hpositive
08Construct an explicit witnessL12–12

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

  1. L12
    exists k
09Use earlier factsL13–13

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

  1. L13
    apply PA2
10Calculate and transport equalitiesL14–16

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

  1. L14
    trans 2 * S k + 1
  2. L15
    simp [two_mul_eq_add_self, add_succ_left]
  3. L16
    symm
11Use earlier factsL17–17

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

  1. L17
    exact heq

Library-wide reading audit

Original exact command ledger · 17 lines
  1. 0001intro n
  2. 0002induction k
  3. 0003intro heq
  4. 0004intro hpositive
  5. 0005cases hpositive
  6. 0006exfalso
  7. 0007apply PA1
  8. 0008symm
  9. 0009exact hpositive_witness
  10. 0010intro heq
  11. 0011intro hpositive
  12. 0012exists k
  13. 0013apply PA2
  14. 0014trans 2 * S k + 1
  15. 0015simp [two_mul_eq_add_self, add_succ_left]
  16. 0016symm
  17. 0017exact heq