DL0044

matrix_rank_selected_prefix_exists_nonzero

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

HA induction constructs arbitrary finite prefixes of actual selected matrices whenever the selected row width is positive.

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 l. ~(q = 0) -> exists ub uc. (forall mdr_i_prefix_exists. (exists mdr_gap_prefix_existsbound. mdr_gap_prefix_existsbound + S (mdr_i_prefix_exists) = (l)) -> exists mdr_a_prefix_exists. (((exists mdr_r_prefix_existspoint mdr_s_prefix_existspoint mdr_u_prefix_existspoint mdr_v_prefix_existspoint. ((mdr_i_prefix_exists = (q) * mdr_r_prefix_existspoint + mdr_s_prefix_existspoint) /\ ((exists mdr_gap_prefix_existspointcolumn. mdr_gap_prefix_existspointcolumn + S (mdr_s_prefix_existspoint) = (q)) /\ ((((exists ff_h_mdr_prefix_existspointrow_index. ff_h_mdr_prefix_existspointrow_index + S (mdr_u_prefix_existspoint) = S ((S (mdr_r_prefix_existspoint)) * rc)) /\ exists ff_q_mdr_prefix_existspointrow_index. rb = ff_q_mdr_prefix_existspointrow_index * S ((S (mdr_r_prefix_existspoint)) * rc) + (mdr_u_prefix_existspoint))) /\ ((((exists ff_h_mdr_prefix_existspointcolumn_index. ff_h_mdr_prefix_existspointcolumn_index + S (mdr_v_prefix_existspoint) = S ((S (mdr_s_prefix_existspoint)) * cc)) /\ exists ff_q_mdr_prefix_existspointcolumn_index. cb = ff_q_mdr_prefix_existspointcolumn_index * S ((S (mdr_s_prefix_existspoint)) * cc) + (mdr_v_prefix_existspoint))) /\ (((exists ff_h_mdr_prefix_existspointsource. ff_h_mdr_prefix_existspointsource + S (mdr_a_prefix_exists) = S ((S ((mdr_u_prefix_existspoint) * (w) + (mdr_v_prefix_existspoint))) * c)) /\ exists ff_q_mdr_prefix_existspointsource. b = ff_q_mdr_prefix_existspointsource * S ((S ((mdr_u_prefix_existspoint) * (w) + (mdr_v_prefix_existspoint))) * c) + (mdr_a_prefix_exists)))))))) /\ (((exists ff_h_mdr_prefix_existsoutput. ff_h_mdr_prefix_existsoutput + S (mdr_a_prefix_exists) = S ((S (mdr_i_prefix_exists)) * uc)) /\ exists ff_q_mdr_prefix_existsoutput. ub = ff_q_mdr_prefix_existsoutput * S ((S (mdr_i_prefix_exists)) * uc) + (mdr_a_prefix_exists))))))

Constructive proof overview

Generated structural guide

HA induction constructs arbitrary finite prefixes of actual selected matrices whenever the selected row width is positive.

The unchanged tactic script uses 3 declared prerequisites and contains 57 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL0042 matrix_rank_selected_prefix_empty DL0040 matrix_rank_selected_point_exists DL0043 matrix_rank_selected_prefix_extend

Direct dependents

DL0045 matrix_rank_selected_square_exists

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

57 script commands · 13 reading checkpoints · 2 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 (3)
matrix rank selected prefix emptymatrix rank selected point existsmatrix rank selected prefix extend

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

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
02Induction on lL9–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L9
    induction l
  2. L10
    intro hq
03Construct an explicit witnessL11–12

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

  1. L11
    exists 0
  2. L12
    exists 0
04Use earlier factsL13–22

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

  1. L13
    specialize matrix_rank_selected_prefix_empty (b)
  2. L14
    specialize matrix_rank_selected_prefix_empty (c)
  3. L15
    specialize matrix_rank_selected_prefix_empty (w)
  4. L16
    specialize matrix_rank_selected_prefix_empty (rb)
  5. L17
    specialize matrix_rank_selected_prefix_empty (rc)
  6. L18
    specialize matrix_rank_selected_prefix_empty (cb)
  7. L19
    specialize matrix_rank_selected_prefix_empty (cc)
  8. L20
    specialize matrix_rank_selected_prefix_empty (q)
  9. L21
    specialize matrix_rank_selected_prefix_empty (0)
  10. L22
    specialize matrix_rank_selected_prefix_empty (0)
05Use earlier factsL23–23

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

  1. L23
    apply matrix_rank_selected_prefix_empty
06Fix variables and assumptionsL24–24

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

  1. L24
    intro hq
07Establish hpreviousL25–27

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

  1. L25
    have hprevious : ∃ ub. ∃ uc. ∀ x. Lt(x,l) → ∃ y. (∃ z. ∃ n. ∃ m. ∃ k. x = q · z + n ∧ (Lt(n,q) ∧ (BetaAt(rb,rc,z,m) ∧ (BetaAt(cb,cc,n,k) ∧ BetaAt(b,c,m · w + k,y))))) ∧ BetaAt(ub,uc,x,y)Definitions: LtBetaAt
  2. L26
    apply IH
  3. L27
    exact hq
08Separate the logical casesL28–29

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

  1. L28
    cases hprevious
  2. L29
    cases hprevious_witness
09Establish hpointL30–39

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have hpoint : ∃ a. ∃ mdr_r_next_point_exists. ∃ mdr_s_next_point_exists. ∃ mdr_u_next_point_exists. ∃ mdr_v_next_point_exists. l = q · mdr_r_next_point_exists + mdr_s_next_point_exists ∧ (Lt(mdr_s_next_point_exists,q) ∧ (BetaAt(rb,rc,mdr_r_next_point_exists,mdr_u_next_point_exists) ∧ (BetaAt(cb,cc,mdr_s_next_point_exists,mdr_v_next_point_exists) ∧ BetaAt(b,c,mdr_u_next_point_exists · w + mdr_v_next_point_exists,a))))Definitions: LtBetaAt
  2. L31
    specialize matrix_rank_selected_point_exists (b)
  3. L32
    specialize matrix_rank_selected_point_exists (c)
  4. L33
    specialize matrix_rank_selected_point_exists (w)
  5. L34
    specialize matrix_rank_selected_point_exists (rb)
  6. L35
    specialize matrix_rank_selected_point_exists (rc)
  7. L36
    specialize matrix_rank_selected_point_exists (cb)
  8. L37
    specialize matrix_rank_selected_point_exists (cc)
  9. L38
    specialize matrix_rank_selected_point_exists (q)
  10. L39
    specialize matrix_rank_selected_point_exists (l)
10Use earlier factsL40–41

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

  1. L40
    apply matrix_rank_selected_point_exists
  2. L41
    exact hq
11Separate the logical casesL42–42

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

  1. L42
    cases hpoint
12Use earlier factsL43–52

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

  1. L43
    specialize matrix_rank_selected_prefix_extend (b)
  2. L44
    specialize matrix_rank_selected_prefix_extend (c)
  3. L45
    specialize matrix_rank_selected_prefix_extend (w)
  4. L46
    specialize matrix_rank_selected_prefix_extend (rb)
  5. L47
    specialize matrix_rank_selected_prefix_extend (rc)
  6. L48
    specialize matrix_rank_selected_prefix_extend (cb)
  7. L49
    specialize matrix_rank_selected_prefix_extend (cc)
  8. L50
    specialize matrix_rank_selected_prefix_extend (q)
  9. L51
    specialize matrix_rank_selected_prefix_extend (x)
  10. L52
    specialize matrix_rank_selected_prefix_extend (x1)
13Use earlier factsL53–57

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

  1. L53
    specialize matrix_rank_selected_prefix_extend (l)
  2. L54
    specialize matrix_rank_selected_prefix_extend (x2)
  3. L55
    apply matrix_rank_selected_prefix_extend
  4. L56
    exact hprevious_witness_witness
  5. L57
    exact hpoint_witness

Library-wide reading audit

Original exact command ledger · 57 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. 0009induction l
  10. 0010intro hq
  11. 0011exists 0
  12. 0012exists 0
  13. 0013specialize matrix_rank_selected_prefix_empty (b)
  14. 0014specialize matrix_rank_selected_prefix_empty (c)
  15. 0015specialize matrix_rank_selected_prefix_empty (w)
  16. 0016specialize matrix_rank_selected_prefix_empty (rb)
  17. 0017specialize matrix_rank_selected_prefix_empty (rc)
  18. 0018specialize matrix_rank_selected_prefix_empty (cb)
  19. 0019specialize matrix_rank_selected_prefix_empty (cc)
  20. 0020specialize matrix_rank_selected_prefix_empty (q)
  21. 0021specialize matrix_rank_selected_prefix_empty (0)
  22. 0022specialize matrix_rank_selected_prefix_empty (0)
  23. 0023apply matrix_rank_selected_prefix_empty
  24. 0024intro hq
  25. 0025have hprevious : exists ub uc. (forall mdr_i_prefix_previous_exists. (exists mdr_gap_prefix_previous_existsbound. mdr_gap_prefix_previous_existsbound + S (mdr_i_prefix_previous_exists) = (l)) -> exists mdr_a_prefix_previous_exists. (((exists mdr_r_prefix_previous_existspoint mdr_s_prefix_previous_existspoint mdr_u_prefix_previous_existspoint mdr_v_prefix_previous_existspoint. ((mdr_i_prefix_previous_exists = (q) * mdr_r_prefix_previous_existspoint + mdr_s_prefix_previous_existspoint) /\ ((exists mdr_gap_prefix_previous_existspointcolumn. mdr_gap_prefix_previous_existspointcolumn + S (mdr_s_prefix_previous_existspoint) = (q)) /\ ((((exists ff_h_mdr_prefix_previous_existspointrow_index. ff_h_mdr_prefix_previous_existspointrow_index + S (mdr_u_prefix_previous_existspoint) = S ((S (mdr_r_prefix_previous_existspoint)) * rc)) /\ exists ff_q_mdr_prefix_previous_existspointrow_index. rb = ff_q_mdr_prefix_previous_existspointrow_index * S ((S (mdr_r_prefix_previous_existspoint)) * rc) + (mdr_u_prefix_previous_existspoint))) /\ ((((exists ff_h_mdr_prefix_previous_existspointcolumn_index. ff_h_mdr_prefix_previous_existspointcolumn_index + S (mdr_v_prefix_previous_existspoint) = S ((S (mdr_s_prefix_previous_existspoint)) * cc)) /\ exists ff_q_mdr_prefix_previous_existspointcolumn_index. cb = ff_q_mdr_prefix_previous_existspointcolumn_index * S ((S (mdr_s_prefix_previous_existspoint)) * cc) + (mdr_v_prefix_previous_existspoint))) /\ (((exists ff_h_mdr_prefix_previous_existspointsource. ff_h_mdr_prefix_previous_existspointsource + S (mdr_a_prefix_previous_exists) = S ((S ((mdr_u_prefix_previous_existspoint) * (w) + (mdr_v_prefix_previous_existspoint))) * c)) /\ exists ff_q_mdr_prefix_previous_existspointsource. b = ff_q_mdr_prefix_previous_existspointsource * S ((S ((mdr_u_prefix_previous_existspoint) * (w) + (mdr_v_prefix_previous_existspoint))) * c) + (mdr_a_prefix_previous_exists)))))))) /\ (((exists ff_h_mdr_prefix_previous_existsoutput. ff_h_mdr_prefix_previous_existsoutput + S (mdr_a_prefix_previous_exists) = S ((S (mdr_i_prefix_previous_exists)) * uc)) /\ exists ff_q_mdr_prefix_previous_existsoutput. ub = ff_q_mdr_prefix_previous_existsoutput * S ((S (mdr_i_prefix_previous_exists)) * uc) + (mdr_a_prefix_previous_exists))))))
  26. 0026apply IH
  27. 0027exact hq
  28. 0028cases hprevious
  29. 0029cases hprevious_witness
  30. 0030have hpoint : exists a. exists mdr_r_next_point_exists mdr_s_next_point_exists mdr_u_next_point_exists mdr_v_next_point_exists. ((l = (q) * mdr_r_next_point_exists + mdr_s_next_point_exists) /\ ((exists mdr_gap_next_point_existscolumn. mdr_gap_next_point_existscolumn + S (mdr_s_next_point_exists) = (q)) /\ ((((exists ff_h_mdr_next_point_existsrow_index. ff_h_mdr_next_point_existsrow_index + S (mdr_u_next_point_exists) = S ((S (mdr_r_next_point_exists)) * rc)) /\ exists ff_q_mdr_next_point_existsrow_index. rb = ff_q_mdr_next_point_existsrow_index * S ((S (mdr_r_next_point_exists)) * rc) + (mdr_u_next_point_exists))) /\ ((((exists ff_h_mdr_next_point_existscolumn_index. ff_h_mdr_next_point_existscolumn_index + S (mdr_v_next_point_exists) = S ((S (mdr_s_next_point_exists)) * cc)) /\ exists ff_q_mdr_next_point_existscolumn_index. cb = ff_q_mdr_next_point_existscolumn_index * S ((S (mdr_s_next_point_exists)) * cc) + (mdr_v_next_point_exists))) /\ (((exists ff_h_mdr_next_point_existssource. ff_h_mdr_next_point_existssource + S (a) = S ((S ((mdr_u_next_point_exists) * (w) + (mdr_v_next_point_exists))) * c)) /\ exists ff_q_mdr_next_point_existssource. b = ff_q_mdr_next_point_existssource * S ((S ((mdr_u_next_point_exists) * (w) + (mdr_v_next_point_exists))) * c) + (a)))))))
  31. 0031specialize matrix_rank_selected_point_exists (b)
  32. 0032specialize matrix_rank_selected_point_exists (c)
  33. 0033specialize matrix_rank_selected_point_exists (w)
  34. 0034specialize matrix_rank_selected_point_exists (rb)
  35. 0035specialize matrix_rank_selected_point_exists (rc)
  36. 0036specialize matrix_rank_selected_point_exists (cb)
  37. 0037specialize matrix_rank_selected_point_exists (cc)
  38. 0038specialize matrix_rank_selected_point_exists (q)
  39. 0039specialize matrix_rank_selected_point_exists (l)
  40. 0040apply matrix_rank_selected_point_exists
  41. 0041exact hq
  42. 0042cases hpoint
  43. 0043specialize matrix_rank_selected_prefix_extend (b)
  44. 0044specialize matrix_rank_selected_prefix_extend (c)
  45. 0045specialize matrix_rank_selected_prefix_extend (w)
  46. 0046specialize matrix_rank_selected_prefix_extend (rb)
  47. 0047specialize matrix_rank_selected_prefix_extend (rc)
  48. 0048specialize matrix_rank_selected_prefix_extend (cb)
  49. 0049specialize matrix_rank_selected_prefix_extend (cc)
  50. 0050specialize matrix_rank_selected_prefix_extend (q)
  51. 0051specialize matrix_rank_selected_prefix_extend (x)
  52. 0052specialize matrix_rank_selected_prefix_extend (x1)
  53. 0053specialize matrix_rank_selected_prefix_extend (l)
  54. 0054specialize matrix_rank_selected_prefix_extend (x2)
  55. 0055apply matrix_rank_selected_prefix_extend
  56. 0056exact hprevious_witness_witness
  57. 0057exact hpoint_witness