DL0040

matrix_rank_selected_point_exists

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

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

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 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))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 50 exact native proof lines.

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

Proof neighborhood

Direct dependencies

division_remainder_exists Stable theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized

Direct dependents

DL0044 matrix_rank_selected_prefix_exists_nonzero

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

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.

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 : exists r s. i = q * r + s /\ (exists mdr_gap_point_column. mdr_gap_point_column + S (s) = (q))
  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 : exists u. ((exists ff_h_mdr_selected_row. ff_h_mdr_selected_row + S (u) = S ((S (x)) * rc)) /\ exists ff_q_mdr_selected_row. rb = ff_q_mdr_selected_row * S ((S (x)) * rc) + (u))
  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 : exists v. ((exists ff_h_mdr_selected_column. ff_h_mdr_selected_column + S (v) = S ((S (x1)) * cc)) /\ exists ff_q_mdr_selected_column. cb = ff_q_mdr_selected_column * S ((S (x1)) * cc) + (v))
  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 : exists a. ((exists ff_h_mdr_selected_source. ff_h_mdr_selected_source + S (a) = S ((S (x2 * w + x3)) * c)) /\ exists ff_q_mdr_selected_source. b = ff_q_mdr_selected_source * S ((S (x2 * w + x3)) * c) + (a))
  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 exact 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 : exists r s. i = q * r + s /\ (exists mdr_gap_point_column. mdr_gap_point_column + S (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 : exists u. ((exists ff_h_mdr_selected_row. ff_h_mdr_selected_row + S (u) = S ((S (x)) * rc)) /\ exists ff_q_mdr_selected_row. rb = ff_q_mdr_selected_row * S ((S (x)) * rc) + (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 : exists v. ((exists ff_h_mdr_selected_column. ff_h_mdr_selected_column + S (v) = S ((S (x1)) * cc)) /\ exists ff_q_mdr_selected_column. cb = ff_q_mdr_selected_column * S ((S (x1)) * cc) + (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 : exists a. ((exists ff_h_mdr_selected_source. ff_h_mdr_selected_source + S (a) = S ((S (x2 * w + x3)) * c)) /\ exists ff_q_mdr_selected_source. b = ff_q_mdr_selected_source * S ((S (x2 * w + x3)) * c) + (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