DL004B

matrix_rank_selected_point_selector_transport

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

The genuine source cell is unchanged by extensionally equal finite row and column selectors; both selector coordinates are proved in range.

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 Rb Rc Cb Cc i a. (forall mdr_i_point_rows mdr_a_point_rows. (exists mdr_gap_point_rowsb. mdr_gap_point_rowsb + S (mdr_i_point_rows) = (q)) -> (((exists ff_h_mdr_point_rowso. ff_h_mdr_point_rowso + S (mdr_a_point_rows) = S ((S (mdr_i_point_rows)) * rc)) /\ exists ff_q_mdr_point_rowso. rb = ff_q_mdr_point_rowso * S ((S (mdr_i_point_rows)) * rc) + (mdr_a_point_rows))) -> (((exists ff_h_mdr_point_rowsn. ff_h_mdr_point_rowsn + S (mdr_a_point_rows) = S ((S (mdr_i_point_rows)) * Rc)) /\ exists ff_q_mdr_point_rowsn. Rb = ff_q_mdr_point_rowsn * S ((S (mdr_i_point_rows)) * Rc) + (mdr_a_point_rows)))) -> (forall mdr_i_point_columns mdr_a_point_columns. (exists mdr_gap_point_columnsb. mdr_gap_point_columnsb + S (mdr_i_point_columns) = (q)) -> (((exists ff_h_mdr_point_columnso. ff_h_mdr_point_columnso + S (mdr_a_point_columns) = S ((S (mdr_i_point_columns)) * cc)) /\ exists ff_q_mdr_point_columnso. cb = ff_q_mdr_point_columnso * S ((S (mdr_i_point_columns)) * cc) + (mdr_a_point_columns))) -> (((exists ff_h_mdr_point_columnsn. ff_h_mdr_point_columnsn + S (mdr_a_point_columns) = S ((S (mdr_i_point_columns)) * Cc)) /\ exists ff_q_mdr_point_columnsn. Cb = ff_q_mdr_point_columnsn * S ((S (mdr_i_point_columns)) * Cc) + (mdr_a_point_columns)))) -> (exists mdr_gap_point_index. mdr_gap_point_index + S (i) = (q * q)) -> (exists mdr_r_point_source mdr_s_point_source mdr_u_point_source mdr_v_point_source. ((i = (q) * mdr_r_point_source + mdr_s_point_source) /\ ((exists mdr_gap_point_sourcecolumn. mdr_gap_point_sourcecolumn + S (mdr_s_point_source) = (q)) /\ ((((exists ff_h_mdr_point_sourcerow_index. ff_h_mdr_point_sourcerow_index + S (mdr_u_point_source) = S ((S (mdr_r_point_source)) * rc)) /\ exists ff_q_mdr_point_sourcerow_index. rb = ff_q_mdr_point_sourcerow_index * S ((S (mdr_r_point_source)) * rc) + (mdr_u_point_source))) /\ ((((exists ff_h_mdr_point_sourcecolumn_index. ff_h_mdr_point_sourcecolumn_index + S (mdr_v_point_source) = S ((S (mdr_s_point_source)) * cc)) /\ exists ff_q_mdr_point_sourcecolumn_index. cb = ff_q_mdr_point_sourcecolumn_index * S ((S (mdr_s_point_source)) * cc) + (mdr_v_point_source))) /\ (((exists ff_h_mdr_point_sourcesource. ff_h_mdr_point_sourcesource + S (a) = S ((S ((mdr_u_point_source) * (w) + (mdr_v_point_source))) * c)) /\ exists ff_q_mdr_point_sourcesource. b = ff_q_mdr_point_sourcesource * S ((S ((mdr_u_point_source) * (w) + (mdr_v_point_source))) * c) + (a)))))))) -> (exists mdr_r_point_target mdr_s_point_target mdr_u_point_target mdr_v_point_target. ((i = (q) * mdr_r_point_target + mdr_s_point_target) /\ ((exists mdr_gap_point_targetcolumn. mdr_gap_point_targetcolumn + S (mdr_s_point_target) = (q)) /\ ((((exists ff_h_mdr_point_targetrow_index. ff_h_mdr_point_targetrow_index + S (mdr_u_point_target) = S ((S (mdr_r_point_target)) * Rc)) /\ exists ff_q_mdr_point_targetrow_index. Rb = ff_q_mdr_point_targetrow_index * S ((S (mdr_r_point_target)) * Rc) + (mdr_u_point_target))) /\ ((((exists ff_h_mdr_point_targetcolumn_index. ff_h_mdr_point_targetcolumn_index + S (mdr_v_point_target) = S ((S (mdr_s_point_target)) * Cc)) /\ exists ff_q_mdr_point_targetcolumn_index. Cb = ff_q_mdr_point_targetcolumn_index * S ((S (mdr_s_point_target)) * Cc) + (mdr_v_point_target))) /\ (((exists ff_h_mdr_point_targetsource. ff_h_mdr_point_targetsource + S (a) = S ((S ((mdr_u_point_target) * (w) + (mdr_v_point_target))) * c)) /\ exists ff_q_mdr_point_targetsource. b = ff_q_mdr_point_targetsource * S ((S ((mdr_u_point_target) * (w) + (mdr_v_point_target))) * c) + (a))))))))

Constructive proof overview

Generated structural guide

The genuine source cell is unchanged by extensionally equal finite row and column selectors; both selector coordinates are proved in range.

The unchanged tactic script uses 1 declared prerequisite and contains 55 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL001B matrix_recursive_quotient_row_bound

Direct dependents

DL004C matrix_rank_selected_prefix_selector_transport

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

55 script commands · 13 reading checkpoints · 1 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.

Named ingredients (1)
matrix recursive quotient row bound
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 Rb
  10. L10
    intro Rc
02Fix variables and assumptionsL11–18

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

  1. L11
    intro Cb
  2. L12
    intro Cc
  3. L13
    intro i
  4. L14
    intro a
  5. L15
    intro hrows
  6. L16
    intro hcolumns
  7. L17
    intro hi
  8. L18
    intro hpoint
03Separate the logical casesL19–26

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

  1. L19
    cases hpoint
  2. L20
    cases hpoint_witness
  3. L21
    cases hpoint_witness_witness
  4. L22
    cases hpoint_witness_witness_witness
  5. L23
    cases hpoint_witness_witness_witness_witness
  6. L24
    cases hpoint_witness_witness_witness_witness_right
  7. L25
    cases hpoint_witness_witness_witness_witness_right_right
  8. L26
    cases hpoint_witness_witness_witness_witness_right_right_right
04Establish hrL27–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix recursive quotient row bound.

  1. L27
    have hr : exists mdr_gap_transport_row_bound. mdr_gap_transport_row_bound + S (x) = (q)
  2. L28
    specialize matrix_recursive_quotient_row_bound (q)
  3. L29
    specialize matrix_recursive_quotient_row_bound (i)
  4. L30
    specialize matrix_recursive_quotient_row_bound (x)
  5. L31
    specialize matrix_recursive_quotient_row_bound (x1)
  6. L32
    apply matrix_recursive_quotient_row_bound
  7. L33
    exact hpoint_witness_witness_witness_witness_left
  8. L34
    exact hi
05Construct an explicit witnessL35–38

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

  1. L35
    exists x
  2. L36
    exists x1
  3. L37
    exists x2
  4. L38
    exists x3
06Separate the logical casesL39–39

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

  1. L39
    split
07Use earlier factsL40–40

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

  1. L40
    exact hpoint_witness_witness_witness_witness_left
08Separate the logical casesL41–41

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

  1. L41
    split
09Use earlier factsL42–42

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

  1. L42
    exact hpoint_witness_witness_witness_witness_right_left
10Separate the logical casesL43–43

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

  1. L43
    split
11Use earlier factsL44–48

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

  1. L44
    specialize hrows (x)
  2. L45
    specialize hrows (x2)
  3. L46
    apply hrows
  4. L47
    exact hr
  5. L48
    exact hpoint_witness_witness_witness_witness_right_right_left
12Separate the logical casesL49–49

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

  1. L49
    split
13Use earlier factsL50–55

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

  1. L50
    specialize hcolumns (x1)
  2. L51
    specialize hcolumns (x3)
  3. L52
    apply hcolumns
  4. L53
    exact hpoint_witness_witness_witness_witness_right_left
  5. L54
    exact hpoint_witness_witness_witness_witness_right_right_right_left
  6. L55
    exact hpoint_witness_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original exact command ledger · 55 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 Rb
  10. 0010intro Rc
  11. 0011intro Cb
  12. 0012intro Cc
  13. 0013intro i
  14. 0014intro a
  15. 0015intro hrows
  16. 0016intro hcolumns
  17. 0017intro hi
  18. 0018intro hpoint
  19. 0019cases hpoint
  20. 0020cases hpoint_witness
  21. 0021cases hpoint_witness_witness
  22. 0022cases hpoint_witness_witness_witness
  23. 0023cases hpoint_witness_witness_witness_witness
  24. 0024cases hpoint_witness_witness_witness_witness_right
  25. 0025cases hpoint_witness_witness_witness_witness_right_right
  26. 0026cases hpoint_witness_witness_witness_witness_right_right_right
  27. 0027have hr : exists mdr_gap_transport_row_bound. mdr_gap_transport_row_bound + S (x) = (q)
  28. 0028specialize matrix_recursive_quotient_row_bound (q)
  29. 0029specialize matrix_recursive_quotient_row_bound (i)
  30. 0030specialize matrix_recursive_quotient_row_bound (x)
  31. 0031specialize matrix_recursive_quotient_row_bound (x1)
  32. 0032apply matrix_recursive_quotient_row_bound
  33. 0033exact hpoint_witness_witness_witness_witness_left
  34. 0034exact hi
  35. 0035exists x
  36. 0036exists x1
  37. 0037exists x2
  38. 0038exists x3
  39. 0039split
  40. 0040exact hpoint_witness_witness_witness_witness_left
  41. 0041split
  42. 0042exact hpoint_witness_witness_witness_witness_right_left
  43. 0043split
  44. 0044specialize hrows (x)
  45. 0045specialize hrows (x2)
  46. 0046apply hrows
  47. 0047exact hr
  48. 0048exact hpoint_witness_witness_witness_witness_right_right_left
  49. 0049split
  50. 0050specialize hcolumns (x1)
  51. 0051specialize hcolumns (x3)
  52. 0052apply hcolumns
  53. 0053exact hpoint_witness_witness_witness_witness_right_left
  54. 0054exact hpoint_witness_witness_witness_witness_right_right_right_left
  55. 0055exact hpoint_witness_witness_witness_witness_right_right_right_right