DL003F

matrix_rank_selector_empty

The empty row or column selector is valid even when its ambient dimension is zero.

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

∀ b. ∀ c. ∀ B. FiniteMatrixSelector(b,c,0,B)

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

Definition DAG

FiniteMatrixSelector(b,c,l,B) · 1

Actual proof prerequisites

matrix_rank_bounded_prefix_emptymatrix_rank_no_index_below_zero
Original expanded first-order statement 
forall b c B. (((forall fom_index_mrf_selector_emptybound. (exists fom_gap_mrf_selector_emptybound_index_bound. fom_gap_mrf_selector_emptybound_index_bound + S (fom_index_mrf_selector_emptybound) = 0) -> exists fom_value_mrf_selector_emptybound. ((((exists fom_beta_height_mrf_selector_emptybound_entry. fom_beta_height_mrf_selector_emptybound_entry + S (fom_value_mrf_selector_emptybound) = S ((S (fom_index_mrf_selector_emptybound)) * c)) /\ exists fom_beta_quotient_mrf_selector_emptybound_entry. b = fom_beta_quotient_mrf_selector_emptybound_entry * S ((S (fom_index_mrf_selector_emptybound)) * c) + (fom_value_mrf_selector_emptybound))) /\ (exists fom_gap_mrf_selector_emptybound_value_bound. fom_gap_mrf_selector_emptybound_value_bound + S (fom_value_mrf_selector_emptybound) = B))) /\ (forall mdr_i_selector_emptydistinct mdr_j_selector_emptydistinct mdr_a_selector_emptydistinct. (exists mdr_gap_selector_emptydistincti. mdr_gap_selector_emptydistincti + S (mdr_i_selector_emptydistinct) = (0)) -> (exists mdr_gap_selector_emptydistinctj. mdr_gap_selector_emptydistinctj + S (mdr_j_selector_emptydistinct) = (0)) -> (((exists ff_h_mdr_selector_emptydistinctfirst. ff_h_mdr_selector_emptydistinctfirst + S (mdr_a_selector_emptydistinct) = S ((S (mdr_i_selector_emptydistinct)) * c)) /\ exists ff_q_mdr_selector_emptydistinctfirst. b = ff_q_mdr_selector_emptydistinctfirst * S ((S (mdr_i_selector_emptydistinct)) * c) + (mdr_a_selector_emptydistinct))) -> (((exists ff_h_mdr_selector_emptydistinctsecond. ff_h_mdr_selector_emptydistinctsecond + S (mdr_a_selector_emptydistinct) = S ((S (mdr_j_selector_emptydistinct)) * c)) /\ exists ff_q_mdr_selector_emptydistinctsecond. b = ff_q_mdr_selector_emptydistinctsecond * S ((S (mdr_j_selector_emptydistinct)) * c) + (mdr_a_selector_emptydistinct))) -> mdr_i_selector_emptydistinct = mdr_j_selector_emptydistinct)))

Complete tactic proof in conservative notation

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

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

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

Named ingredients (2)
matrix rank bounded prefix emptymatrix rank no index below zero
01Fix variables and assumptionsL1–3

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro B
02Separate the logical casesL4–4

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

  1. L4
    split
03Use earlier factsL5–8

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

  1. L5
    specialize matrix_rank_bounded_prefix_empty (b)
  2. L6
    specialize matrix_rank_bounded_prefix_empty (c)
  3. L7
    specialize matrix_rank_bounded_prefix_empty (B)
  4. L8
    apply matrix_rank_bounded_prefix_empty
04Fix variables and assumptionsL9–15

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

  1. L9
    intro i
  2. L10
    intro j
  3. L11
    intro a
  4. L12
    intro hi
  5. L13
    intro hj
  6. L14
    intro ha
  7. L15
    intro hb
05Separate the logical casesL16–16

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

  1. L16
    exfalso
06Use earlier factsL17–19

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

  1. L17
    specialize matrix_rank_no_index_below_zero (i)
  2. L18
    apply matrix_rank_no_index_below_zero
  3. L19
    exact hi

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro B
  4. 0004split
  5. 0005specialize matrix_rank_bounded_prefix_empty (b)
  6. 0006specialize matrix_rank_bounded_prefix_empty (c)
  7. 0007specialize matrix_rank_bounded_prefix_empty (B)
  8. 0008apply matrix_rank_bounded_prefix_empty
  9. 0009intro i
  10. 0010intro j
  11. 0011intro a
  12. 0012intro hi
  13. 0013intro hj
  14. 0014intro ha
  15. 0015intro hb
  16. 0016exfalso
  17. 0017specialize matrix_rank_no_index_below_zero (i)
  18. 0018apply matrix_rank_no_index_below_zero
  19. 0019exact hi