DL0044

matrix_rank_selected_prefix_exists_nonzero

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

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

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

Definition DAG

Lt(a,b) · 5BetaAt(b,c,i,x) · 11

Actual proof prerequisites

matrix_rank_selected_prefix_emptymatrix_rank_selected_point_existsmatrix_rank_selected_prefix_extend
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
matrix rank selected prefix emptymatrix rank selected point existsmatrix rank selected prefix extend
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: Lt(x,l)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)Original native command in the exact edition
  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: 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)Original native command in the exact edition
  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 defined 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 : ∃ 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)
  26. 0026apply IH
  27. 0027exact hq
  28. 0028cases hprevious
  29. 0029cases hprevious_witness
  30. 0030have 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))))
  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