DL0040

matrix_rank_selected_point_exists

Decode a genuine row selector, column selector, and parent entry at every flattened selected-matrix index.

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. ∀ w. ∀ rb. ∀ rc. ∀ cb. ∀ cc. ∀ q. ∀ i. ¬q = 0 → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. i = q · y + z ∧ (Lt(z,q) ∧ (BetaAt(rb,rc,y,n) ∧ (BetaAt(cb,cc,z,m) ∧ BetaAt(b,c,n · w + m,x))))

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

Definition DAG

Lt(a,b) · 2BetaAt(b,c,i,x) · 6

Actual proof prerequisites

division_remainder_exists · checked external prerequisitebeta_at_exists · checked external prerequisite
Original expanded first-order statement 
forall b c w rb rc cb cc q i. ~(q = 0) -> exists a. (exists mdr_r_point_exists mdr_s_point_exists mdr_u_point_exists mdr_v_point_exists. ((i = (q) * mdr_r_point_exists + mdr_s_point_exists) /\ ((exists mdr_gap_point_existscolumn. mdr_gap_point_existscolumn + S (mdr_s_point_exists) = (q)) /\ ((((exists ff_h_mdr_point_existsrow_index. ff_h_mdr_point_existsrow_index + S (mdr_u_point_exists) = S ((S (mdr_r_point_exists)) * rc)) /\ exists ff_q_mdr_point_existsrow_index. rb = ff_q_mdr_point_existsrow_index * S ((S (mdr_r_point_exists)) * rc) + (mdr_u_point_exists))) /\ ((((exists ff_h_mdr_point_existscolumn_index. ff_h_mdr_point_existscolumn_index + S (mdr_v_point_exists) = S ((S (mdr_s_point_exists)) * cc)) /\ exists ff_q_mdr_point_existscolumn_index. cb = ff_q_mdr_point_existscolumn_index * S ((S (mdr_s_point_exists)) * cc) + (mdr_v_point_exists))) /\ (((exists ff_h_mdr_point_existssource. ff_h_mdr_point_existssource + S (a) = S ((S ((mdr_u_point_exists) * (w) + (mdr_v_point_exists))) * c)) /\ exists ff_q_mdr_point_existssource. b = ff_q_mdr_point_existssource * S ((S ((mdr_u_point_exists) * (w) + (mdr_v_point_exists))) * c) + (a))))))))

Complete tactic proof in conservative notation

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

50 script commands · 18 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–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro w
  4. L4
    intro rb
  5. L5
    intro rc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro q
  9. L9
    intro i
  10. L10
    intro hq
02Establish hcoordinatesL11–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L11
    have hcoordinates : ∃ r. ∃ s. i = q · r + s ∧ Lt(s,q)Definitions: Lt(s,q)Original native command in the exact edition
  2. L12
    specialize division_remainder_exists (q)
  3. L13
    specialize division_remainder_exists (i)
  4. L14
    apply division_remainder_exists
  5. L15
    exact hq
03Separate the logical casesL16–18

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

  1. L16
    cases hcoordinates
  2. L17
    cases hcoordinates_witness
  3. L18
    cases hcoordinates_witness_witness
04Establish hrowL19–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L19
    have hrow : ∃ u. BetaAt(rb,rc,x,u)Definitions: BetaAt(rb,rc,x,u)Original native command in the exact edition
  2. L20
    specialize beta_at_exists (rb)
  3. L21
    specialize beta_at_exists (rc)
  4. L22
    specialize beta_at_exists (x)
  5. L23
    apply beta_at_exists
05Separate the logical casesL24–24

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

  1. L24
    cases hrow
06Establish hcolumnL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L25
    have hcolumn : ∃ v. BetaAt(cb,cc,x1,v)Definitions: BetaAt(cb,cc,x1,v)Original native command in the exact edition
  2. L26
    specialize beta_at_exists (cb)
  3. L27
    specialize beta_at_exists (cc)
  4. L28
    specialize beta_at_exists (x1)
  5. L29
    apply beta_at_exists
07Separate the logical casesL30–30

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

  1. L30
    cases hcolumn
08Establish hentryL31–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L31
    have hentry : ∃ a. BetaAt(b,c,x2 · w + x3,a)Definitions: BetaAt(b,c,x2 · w + x3,a)Original native command in the exact edition
  2. L32
    specialize beta_at_exists (b)
  3. L33
    specialize beta_at_exists (c)
  4. L34
    specialize beta_at_exists (x2 * w + x3)
  5. L35
    apply beta_at_exists
09Separate the logical casesL36–36

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

  1. L36
    cases hentry
10Construct an explicit witnessL37–41

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

  1. L37
    exists x4
  2. L38
    exists x
  3. L39
    exists x1
  4. L40
    exists x2
  5. L41
    exists x3
11Separate the logical casesL42–42

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

  1. L42
    split
12Use earlier factsL43–43

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

  1. L43
    exact hcoordinates_witness_witness_left
13Separate the logical casesL44–44

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

  1. L44
    split
14Use earlier factsL45–45

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

  1. L45
    exact hcoordinates_witness_witness_right
15Separate the logical casesL46–46

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

  1. L46
    split
16Use earlier factsL47–47

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

  1. L47
    exact hrow_witness
17Separate the logical casesL48–48

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

  1. L48
    split
18Use earlier factsL49–50

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

  1. L49
    exact hcolumn_witness
  2. L50
    exact hentry_witness

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro q
  9. 0009intro i
  10. 0010intro hq
  11. 0011have hcoordinates : ∃ r. ∃ s. i = q · r + s ∧ Lt(s,q)
  12. 0012specialize division_remainder_exists (q)
  13. 0013specialize division_remainder_exists (i)
  14. 0014apply division_remainder_exists
  15. 0015exact hq
  16. 0016cases hcoordinates
  17. 0017cases hcoordinates_witness
  18. 0018cases hcoordinates_witness_witness
  19. 0019have hrow : ∃ u. BetaAt(rb,rc,x,u)
  20. 0020specialize beta_at_exists (rb)
  21. 0021specialize beta_at_exists (rc)
  22. 0022specialize beta_at_exists (x)
  23. 0023apply beta_at_exists
  24. 0024cases hrow
  25. 0025have hcolumn : ∃ v. BetaAt(cb,cc,x1,v)
  26. 0026specialize beta_at_exists (cb)
  27. 0027specialize beta_at_exists (cc)
  28. 0028specialize beta_at_exists (x1)
  29. 0029apply beta_at_exists
  30. 0030cases hcolumn
  31. 0031have hentry : ∃ a. BetaAt(b,c,x2 · w + x3,a)
  32. 0032specialize beta_at_exists (b)
  33. 0033specialize beta_at_exists (c)
  34. 0034specialize beta_at_exists (x2 * w + x3)
  35. 0035apply beta_at_exists
  36. 0036cases hentry
  37. 0037exists x4
  38. 0038exists x
  39. 0039exists x1
  40. 0040exists x2
  41. 0041exists x3
  42. 0042split
  43. 0043exact hcoordinates_witness_witness_left
  44. 0044split
  45. 0045exact hcoordinates_witness_witness_right
  46. 0046split
  47. 0047exact hrow_witness
  48. 0048split
  49. 0049exact hcolumn_witness
  50. 0050exact hentry_witness