DL005A

matrix_rank_le_successor_cases

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

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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ j. ∀ K. Le(j,S K) → j = S K ∨ Le(j,K)

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

Definition DAG

Le(a,b) · 2Lt(a,b) · 2

Actual proof prerequisites

succ_le_succ · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

All 21 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

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.

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–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 : Lt(j,S S K)Definitions: Lt(j,S S K)Original native command in the exact edition
  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 ∨ Lt(j,S K)Definitions: Lt(j,S K)Original native command in the exact edition
  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 defined command ledger · 21 lines
  1. 0001intro j
  2. 0002intro K
  3. 0003intro hj
  4. 0004have hstrict : Lt(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 ∨ Lt(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