DL005A

matrix_rank_le_successor_cases

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

A natural number bounded by a successor is either that successor or is bounded by its predecessor.

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 j K. (exists mdr_gap_successor_bound. mdr_gap_successor_bound + (j) = (S K)) -> j = S K \/ (exists mdr_gap_previous_bound. mdr_gap_previous_bound + (j) = (K))

Constructive proof overview

Generated structural guide

A natural number bounded by a successor is either that successor or is bounded by its predecessor.

The unchanged tactic script uses 3 declared prerequisites and contains 21 exact native proof lines.

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

Proof neighborhood

Direct dependencies

succ_le_succ Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized

Direct dependents

DL005B matrix_rank_maximal_nonzero_prefix_exists

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

21 script commands · 7 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro j
  2. L2
    intro K
  3. L3
    intro hj
02Establish hstrictL4–8

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

  1. L4
    have hstrict : exists mdr_gap_strict_successor. mdr_gap_strict_successor + S (j) = (S (S K))
  2. L5
    specialize succ_le_succ (j)
  3. L6
    specialize succ_le_succ (S K)
  4. L7
    apply succ_le_succ
  5. L8
    exact hj
03Establish hcaseL9–13

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

  1. L9
    have hcase : j = S K \/ (exists mdr_gap_previous_strict. mdr_gap_previous_strict + S (j) = (S K))
  2. L10
    specialize finite_lt_succ_eq_or_lt (S K)
  3. L11
    specialize finite_lt_succ_eq_or_lt (j)
  4. L12
    apply finite_lt_succ_eq_or_lt
  5. L13
    exact hstrict
04Separate the logical casesL14–15

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

  1. L14
    cases hcase
  2. L15
    left
05Use earlier factsL16–16

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

  1. L16
    exact hcase_left
06Separate the logical casesL17–17

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

  1. L17
    right
07Use earlier factsL18–21

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

  1. L18
    specialize le_of_succ_le_succ (j)
  2. L19
    specialize le_of_succ_le_succ (K)
  3. L20
    apply le_of_succ_le_succ
  4. L21
    exact hcase_right

Library-wide reading audit

Original exact command ledger · 21 lines
  1. 0001intro j
  2. 0002intro K
  3. 0003intro hj
  4. 0004have hstrict : exists mdr_gap_strict_successor. mdr_gap_strict_successor + S (j) = (S (S K))
  5. 0005specialize succ_le_succ (j)
  6. 0006specialize succ_le_succ (S K)
  7. 0007apply succ_le_succ
  8. 0008exact hj
  9. 0009have hcase : j = S K \/ (exists mdr_gap_previous_strict. mdr_gap_previous_strict + S (j) = (S K))
  10. 0010specialize finite_lt_succ_eq_or_lt (S K)
  11. 0011specialize finite_lt_succ_eq_or_lt (j)
  12. 0012apply finite_lt_succ_eq_or_lt
  13. 0013exact hstrict
  14. 0014cases hcase
  15. 0015left
  16. 0016exact hcase_left
  17. 0017right
  18. 0018specialize le_of_succ_le_succ (j)
  19. 0019specialize le_of_succ_le_succ (K)
  20. 0020apply le_of_succ_le_succ
  21. 0021exact hcase_right