DL004C

matrix_rank_selected_prefix_selector_transport

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

A complete actual selected-submatrix code remains valid under equality-preserving selector recoding.

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 ub uc. (forall mdr_i_prefix_rows mdr_a_prefix_rows. (exists mdr_gap_prefix_rowsb. mdr_gap_prefix_rowsb + S (mdr_i_prefix_rows) = (q)) -> (((exists ff_h_mdr_prefix_rowso. ff_h_mdr_prefix_rowso + S (mdr_a_prefix_rows) = S ((S (mdr_i_prefix_rows)) * rc)) /\ exists ff_q_mdr_prefix_rowso. rb = ff_q_mdr_prefix_rowso * S ((S (mdr_i_prefix_rows)) * rc) + (mdr_a_prefix_rows))) -> (((exists ff_h_mdr_prefix_rowsn. ff_h_mdr_prefix_rowsn + S (mdr_a_prefix_rows) = S ((S (mdr_i_prefix_rows)) * Rc)) /\ exists ff_q_mdr_prefix_rowsn. Rb = ff_q_mdr_prefix_rowsn * S ((S (mdr_i_prefix_rows)) * Rc) + (mdr_a_prefix_rows)))) -> (forall mdr_i_prefix_columns mdr_a_prefix_columns. (exists mdr_gap_prefix_columnsb. mdr_gap_prefix_columnsb + S (mdr_i_prefix_columns) = (q)) -> (((exists ff_h_mdr_prefix_columnso. ff_h_mdr_prefix_columnso + S (mdr_a_prefix_columns) = S ((S (mdr_i_prefix_columns)) * cc)) /\ exists ff_q_mdr_prefix_columnso. cb = ff_q_mdr_prefix_columnso * S ((S (mdr_i_prefix_columns)) * cc) + (mdr_a_prefix_columns))) -> (((exists ff_h_mdr_prefix_columnsn. ff_h_mdr_prefix_columnsn + S (mdr_a_prefix_columns) = S ((S (mdr_i_prefix_columns)) * Cc)) /\ exists ff_q_mdr_prefix_columnsn. Cb = ff_q_mdr_prefix_columnsn * S ((S (mdr_i_prefix_columns)) * Cc) + (mdr_a_prefix_columns)))) -> (forall mdr_i_selected_prefix_source. (exists mdr_gap_selected_prefix_sourcebound. mdr_gap_selected_prefix_sourcebound + S (mdr_i_selected_prefix_source) = (q * q)) -> exists mdr_a_selected_prefix_source. (((exists mdr_r_selected_prefix_sourcepoint mdr_s_selected_prefix_sourcepoint mdr_u_selected_prefix_sourcepoint mdr_v_selected_prefix_sourcepoint. ((mdr_i_selected_prefix_source = (q) * mdr_r_selected_prefix_sourcepoint + mdr_s_selected_prefix_sourcepoint) /\ ((exists mdr_gap_selected_prefix_sourcepointcolumn. mdr_gap_selected_prefix_sourcepointcolumn + S (mdr_s_selected_prefix_sourcepoint) = (q)) /\ ((((exists ff_h_mdr_selected_prefix_sourcepointrow_index. ff_h_mdr_selected_prefix_sourcepointrow_index + S (mdr_u_selected_prefix_sourcepoint) = S ((S (mdr_r_selected_prefix_sourcepoint)) * rc)) /\ exists ff_q_mdr_selected_prefix_sourcepointrow_index. rb = ff_q_mdr_selected_prefix_sourcepointrow_index * S ((S (mdr_r_selected_prefix_sourcepoint)) * rc) + (mdr_u_selected_prefix_sourcepoint))) /\ ((((exists ff_h_mdr_selected_prefix_sourcepointcolumn_index. ff_h_mdr_selected_prefix_sourcepointcolumn_index + S (mdr_v_selected_prefix_sourcepoint) = S ((S (mdr_s_selected_prefix_sourcepoint)) * cc)) /\ exists ff_q_mdr_selected_prefix_sourcepointcolumn_index. cb = ff_q_mdr_selected_prefix_sourcepointcolumn_index * S ((S (mdr_s_selected_prefix_sourcepoint)) * cc) + (mdr_v_selected_prefix_sourcepoint))) /\ (((exists ff_h_mdr_selected_prefix_sourcepointsource. ff_h_mdr_selected_prefix_sourcepointsource + S (mdr_a_selected_prefix_source) = S ((S ((mdr_u_selected_prefix_sourcepoint) * (w) + (mdr_v_selected_prefix_sourcepoint))) * c)) /\ exists ff_q_mdr_selected_prefix_sourcepointsource. b = ff_q_mdr_selected_prefix_sourcepointsource * S ((S ((mdr_u_selected_prefix_sourcepoint) * (w) + (mdr_v_selected_prefix_sourcepoint))) * c) + (mdr_a_selected_prefix_source)))))))) /\ (((exists ff_h_mdr_selected_prefix_sourceoutput. ff_h_mdr_selected_prefix_sourceoutput + S (mdr_a_selected_prefix_source) = S ((S (mdr_i_selected_prefix_source)) * uc)) /\ exists ff_q_mdr_selected_prefix_sourceoutput. ub = ff_q_mdr_selected_prefix_sourceoutput * S ((S (mdr_i_selected_prefix_source)) * uc) + (mdr_a_selected_prefix_source)))))) -> (forall mdr_i_selected_prefix_target. (exists mdr_gap_selected_prefix_targetbound. mdr_gap_selected_prefix_targetbound + S (mdr_i_selected_prefix_target) = (q * q)) -> exists mdr_a_selected_prefix_target. (((exists mdr_r_selected_prefix_targetpoint mdr_s_selected_prefix_targetpoint mdr_u_selected_prefix_targetpoint mdr_v_selected_prefix_targetpoint. ((mdr_i_selected_prefix_target = (q) * mdr_r_selected_prefix_targetpoint + mdr_s_selected_prefix_targetpoint) /\ ((exists mdr_gap_selected_prefix_targetpointcolumn. mdr_gap_selected_prefix_targetpointcolumn + S (mdr_s_selected_prefix_targetpoint) = (q)) /\ ((((exists ff_h_mdr_selected_prefix_targetpointrow_index. ff_h_mdr_selected_prefix_targetpointrow_index + S (mdr_u_selected_prefix_targetpoint) = S ((S (mdr_r_selected_prefix_targetpoint)) * Rc)) /\ exists ff_q_mdr_selected_prefix_targetpointrow_index. Rb = ff_q_mdr_selected_prefix_targetpointrow_index * S ((S (mdr_r_selected_prefix_targetpoint)) * Rc) + (mdr_u_selected_prefix_targetpoint))) /\ ((((exists ff_h_mdr_selected_prefix_targetpointcolumn_index. ff_h_mdr_selected_prefix_targetpointcolumn_index + S (mdr_v_selected_prefix_targetpoint) = S ((S (mdr_s_selected_prefix_targetpoint)) * Cc)) /\ exists ff_q_mdr_selected_prefix_targetpointcolumn_index. Cb = ff_q_mdr_selected_prefix_targetpointcolumn_index * S ((S (mdr_s_selected_prefix_targetpoint)) * Cc) + (mdr_v_selected_prefix_targetpoint))) /\ (((exists ff_h_mdr_selected_prefix_targetpointsource. ff_h_mdr_selected_prefix_targetpointsource + S (mdr_a_selected_prefix_target) = S ((S ((mdr_u_selected_prefix_targetpoint) * (w) + (mdr_v_selected_prefix_targetpoint))) * c)) /\ exists ff_q_mdr_selected_prefix_targetpointsource. b = ff_q_mdr_selected_prefix_targetpointsource * S ((S ((mdr_u_selected_prefix_targetpoint) * (w) + (mdr_v_selected_prefix_targetpoint))) * c) + (mdr_a_selected_prefix_target)))))))) /\ (((exists ff_h_mdr_selected_prefix_targetoutput. ff_h_mdr_selected_prefix_targetoutput + S (mdr_a_selected_prefix_target) = S ((S (mdr_i_selected_prefix_target)) * uc)) /\ exists ff_q_mdr_selected_prefix_targetoutput. ub = ff_q_mdr_selected_prefix_targetoutput * S ((S (mdr_i_selected_prefix_target)) * uc) + (mdr_a_selected_prefix_target))))))

Constructive proof overview

Generated structural guide

A complete actual selected-submatrix code remains valid under equality-preserving selector recoding.

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

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

Proof neighborhood

Direct dependencies

DL004B matrix_rank_selected_point_selector_transport

Direct dependents

DL004D matrix_rank_signed_selected_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

47 script commands · 8 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 rank selected point selector transport

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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

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

  1. L11
    intro Cb
  2. L12
    intro Cc
  3. L13
    intro ub
  4. L14
    intro uc
  5. L15
    intro hrows
  6. L16
    intro hcolumns
  7. L17
    intro hselected
  8. L18
    intro i
  9. L19
    intro hi
03Establish hentryL20–23

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

  1. L20
    have hentry : ∃ a. (∃ x. ∃ y. ∃ z. ∃ n. i = q · x + y ∧ (Lt(y,q) ∧ (BetaAt(rb,rc,x,z) ∧ (BetaAt(cb,cc,y,n) ∧ BetaAt(b,c,z · w + n,a))))) ∧ BetaAt(ub,uc,i,a)Definitions: LtBetaAt
  2. L21
    specialize hselected (i)
  3. L22
    apply hselected
  4. L23
    exact hi
04Separate the logical casesL24–25

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

  1. L24
    cases hentry
  2. L25
    cases hentry_witness
05Construct an explicit witnessL26–26

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

  1. L26
    exists x
06Separate the logical casesL27–27

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

  1. L27
    split
07Use earlier factsL28–37

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

  1. L28
    specialize matrix_rank_selected_point_selector_transport (b)
  2. L29
    specialize matrix_rank_selected_point_selector_transport (c)
  3. L30
    specialize matrix_rank_selected_point_selector_transport (w)
  4. L31
    specialize matrix_rank_selected_point_selector_transport (rb)
  5. L32
    specialize matrix_rank_selected_point_selector_transport (rc)
  6. L33
    specialize matrix_rank_selected_point_selector_transport (cb)
  7. L34
    specialize matrix_rank_selected_point_selector_transport (cc)
  8. L35
    specialize matrix_rank_selected_point_selector_transport (q)
  9. L36
    specialize matrix_rank_selected_point_selector_transport (Rb)
  10. L37
    specialize matrix_rank_selected_point_selector_transport (Rc)
08Use earlier factsL38–47

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

  1. L38
    specialize matrix_rank_selected_point_selector_transport (Cb)
  2. L39
    specialize matrix_rank_selected_point_selector_transport (Cc)
  3. L40
    specialize matrix_rank_selected_point_selector_transport (i)
  4. L41
    specialize matrix_rank_selected_point_selector_transport (x)
  5. L42
    apply matrix_rank_selected_point_selector_transport
  6. L43
    exact hrows
  7. L44
    exact hcolumns
  8. L45
    exact hi
  9. L46
    exact hentry_witness_left
  10. L47
    exact hentry_witness_right

Library-wide reading audit

Original exact command ledger · 47 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 ub
  14. 0014intro uc
  15. 0015intro hrows
  16. 0016intro hcolumns
  17. 0017intro hselected
  18. 0018intro i
  19. 0019intro hi
  20. 0020have hentry : exists a. ((exists mdr_r_transported_point mdr_s_transported_point mdr_u_transported_point mdr_v_transported_point. ((i = (q) * mdr_r_transported_point + mdr_s_transported_point) /\ ((exists mdr_gap_transported_pointcolumn. mdr_gap_transported_pointcolumn + S (mdr_s_transported_point) = (q)) /\ ((((exists ff_h_mdr_transported_pointrow_index. ff_h_mdr_transported_pointrow_index + S (mdr_u_transported_point) = S ((S (mdr_r_transported_point)) * rc)) /\ exists ff_q_mdr_transported_pointrow_index. rb = ff_q_mdr_transported_pointrow_index * S ((S (mdr_r_transported_point)) * rc) + (mdr_u_transported_point))) /\ ((((exists ff_h_mdr_transported_pointcolumn_index. ff_h_mdr_transported_pointcolumn_index + S (mdr_v_transported_point) = S ((S (mdr_s_transported_point)) * cc)) /\ exists ff_q_mdr_transported_pointcolumn_index. cb = ff_q_mdr_transported_pointcolumn_index * S ((S (mdr_s_transported_point)) * cc) + (mdr_v_transported_point))) /\ (((exists ff_h_mdr_transported_pointsource. ff_h_mdr_transported_pointsource + S (a) = S ((S ((mdr_u_transported_point) * (w) + (mdr_v_transported_point))) * c)) /\ exists ff_q_mdr_transported_pointsource. b = ff_q_mdr_transported_pointsource * S ((S ((mdr_u_transported_point) * (w) + (mdr_v_transported_point))) * c) + (a)))))))) /\ (((exists ff_h_mdr_transported_output. ff_h_mdr_transported_output + S (a) = S ((S (i)) * uc)) /\ exists ff_q_mdr_transported_output. ub = ff_q_mdr_transported_output * S ((S (i)) * uc) + (a))))
  21. 0021specialize hselected (i)
  22. 0022apply hselected
  23. 0023exact hi
  24. 0024cases hentry
  25. 0025cases hentry_witness
  26. 0026exists x
  27. 0027split
  28. 0028specialize matrix_rank_selected_point_selector_transport (b)
  29. 0029specialize matrix_rank_selected_point_selector_transport (c)
  30. 0030specialize matrix_rank_selected_point_selector_transport (w)
  31. 0031specialize matrix_rank_selected_point_selector_transport (rb)
  32. 0032specialize matrix_rank_selected_point_selector_transport (rc)
  33. 0033specialize matrix_rank_selected_point_selector_transport (cb)
  34. 0034specialize matrix_rank_selected_point_selector_transport (cc)
  35. 0035specialize matrix_rank_selected_point_selector_transport (q)
  36. 0036specialize matrix_rank_selected_point_selector_transport (Rb)
  37. 0037specialize matrix_rank_selected_point_selector_transport (Rc)
  38. 0038specialize matrix_rank_selected_point_selector_transport (Cb)
  39. 0039specialize matrix_rank_selected_point_selector_transport (Cc)
  40. 0040specialize matrix_rank_selected_point_selector_transport (i)
  41. 0041specialize matrix_rank_selected_point_selector_transport (x)
  42. 0042apply matrix_rank_selected_point_selector_transport
  43. 0043exact hrows
  44. 0044exact hcolumns
  45. 0045exact hi
  46. 0046exact hentry_witness_left
  47. 0047exact hentry_witness_right