MN0009

beta_matrix_minor_prefix_exists_nonzero

Every finite prefix of a nonempty arbitrary-dimensional cofactor minor has one complete beta code.

Alpha v34 checked-use · first admitted v24 · 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.

Historical partial components only: this chapter proves arbitrary signed cofactor minors and exact signed determinants through dimension four. T13 is now closed by the separate Alpha-v27 integer-linear-algebra branch: arbitrary determinant data, rank, and integer column spans, without a claim of lattice index or normal forms. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ w. ∀ r. ∀ d. ∀ q. ∀ l. ¬q = 0 → ∃ x. ∃ y. MatrixMinorPrefix(b,c,w,r,d,x,y,q,l)

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

Definition DAG

MatrixMinorPrefix(b,c,w,r,d,u,v,q,l) · 1

Actual proof prerequisites

add_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisitebeta_matrix_minor_point_existsbeta_matrix_minor_prefix_extend
Original expanded first-order statement 
forall b c w r d q l. ~(q = 0) -> exists u v. (forall ff_index_mdm_prefix_prefix_result. (exists ff_gap_mdm_lt_prefix_result_index_bound. ff_gap_mdm_lt_prefix_result_index_bound + S (ff_index_mdm_prefix_prefix_result) = (l)) -> exists ff_row_mdm_prefix_prefix_result ff_column_mdm_prefix_prefix_result ff_value_mdm_prefix_prefix_result. (ff_index_mdm_prefix_prefix_result = (q) * ff_row_mdm_prefix_prefix_result + ff_column_mdm_prefix_prefix_result /\ ((exists ff_gap_mdm_lt_prefix_result_column_bound. ff_gap_mdm_lt_prefix_result_column_bound + S (ff_column_mdm_prefix_prefix_result) = (q)) /\ ((exists ff_row_mdm_cell_prefix_result_cell ff_column_mdm_cell_prefix_result_cell. (((((exists ff_gap_mdm_lt_prefix_result_cell_row_before. ff_gap_mdm_lt_prefix_result_cell_row_before + S (ff_row_mdm_prefix_prefix_result) = (r)) /\ ff_row_mdm_cell_prefix_result_cell = ff_row_mdm_prefix_prefix_result) \/ ((exists ff_gap_mdm_le_prefix_result_cell_row_after. ff_gap_mdm_le_prefix_result_cell_row_after + (r) = (ff_row_mdm_prefix_prefix_result)) /\ ff_row_mdm_cell_prefix_result_cell = S ff_row_mdm_prefix_prefix_result))) /\ (((((exists ff_gap_mdm_lt_prefix_result_cell_column_before. ff_gap_mdm_lt_prefix_result_cell_column_before + S (ff_column_mdm_prefix_prefix_result) = (d)) /\ ff_column_mdm_cell_prefix_result_cell = ff_column_mdm_prefix_prefix_result) \/ ((exists ff_gap_mdm_le_prefix_result_cell_column_after. ff_gap_mdm_le_prefix_result_cell_column_after + (d) = (ff_column_mdm_prefix_prefix_result)) /\ ff_column_mdm_cell_prefix_result_cell = S ff_column_mdm_prefix_prefix_result))) /\ (((exists ff_h_mdm_prefix_result_cell_source. ff_h_mdm_prefix_result_cell_source + S (ff_value_mdm_prefix_prefix_result) = S ((S ((ff_row_mdm_cell_prefix_result_cell) * (w) + (ff_column_mdm_cell_prefix_result_cell))) * c)) /\ exists ff_q_mdm_prefix_result_cell_source. b = ff_q_mdm_prefix_result_cell_source * S ((S ((ff_row_mdm_cell_prefix_result_cell) * (w) + (ff_column_mdm_cell_prefix_result_cell))) * c) + (ff_value_mdm_prefix_prefix_result)))))) /\ (((exists ff_h_mdm_prefix_result_target. ff_h_mdm_prefix_result_target + S (ff_value_mdm_prefix_prefix_result) = S ((S (ff_index_mdm_prefix_prefix_result)) * v)) /\ exists ff_q_mdm_prefix_result_target. u = ff_q_mdm_prefix_result_target * S ((S (ff_index_mdm_prefix_prefix_result)) * v) + (ff_value_mdm_prefix_prefix_result)))))))

Complete unchanged native tactic proof

All 50 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

50 script commands · 11 reading checkpoints · 3 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 (2)
beta matrix minor point existsbeta matrix minor 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–6

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 r
  5. L5
    intro d
  6. L6
    intro q
02Induction on lL7–8

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

  1. L7
    induction l
  2. L8
    intro hq
03Construct an explicit witnessL9–10

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

  1. L9
    exists 0
  2. L10
    exists 0
04Fix variables and assumptionsL11–12

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

  1. L11
    intro k
  2. L12
    intro hk
05Separate the logical casesL13–14

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

  1. L13
    exfalso
  2. L14
    cases hk
06Establish hzeroL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L15
    have hzero : S k = 0
  2. L16
    specialize add_eq_zero_right x
  3. L17
    specialize add_eq_zero_right (S k)
  4. L18
    apply add_eq_zero_right
  5. L19
    exact hk_witness
  6. L20
    specialize succ_ne_zero k
  7. L21
    apply succ_ne_zero
  8. L22
    exact hzero
  9. L23
    intro hq
07Establish hpreviousL24–26

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

  1. L24
    have hprevious : ∃ u. ∃ v. MatrixMinorPrefix(b,c,w,r,d,u,v,q,l)Definitions: MatrixMinorPrefixOriginal native command in the exact edition
  2. L25
    apply IH
  3. L26
    exact hq
08Separate the logical casesL27–28

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

  1. L27
    cases hprevious
  2. L28
    cases hprevious_witness
09Establish hpointL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta matrix minor point exists.

  1. L29
    have hpoint : ∃ ff_row_mdm_point_exists_have_point. ∃ ff_column_mdm_point_exists_have_point. ∃ ff_value_mdm_point_exists_have_point. l = q · ff_row_mdm_point_exists_have_point + ff_column_mdm_point_exists_have_point ∧ (Lt(ff_column_mdm_point_exists_have_point,q) ∧ MatrixMinorCell(b,c,w,r,d,ff_row_mdm_point_exists_have_point,ff_column_mdm_point_exists_have_point,ff_value_mdm_point_exists_have_point))Definitions: MatrixMinorCellLtOriginal native command in the exact edition
  2. L30
    specialize beta_matrix_minor_point_exists b
  3. L31
    specialize beta_matrix_minor_point_exists c
  4. L32
    specialize beta_matrix_minor_point_exists w
  5. L33
    specialize beta_matrix_minor_point_exists r
  6. L34
    specialize beta_matrix_minor_point_exists d
  7. L35
    specialize beta_matrix_minor_point_exists q
  8. L36
    specialize beta_matrix_minor_point_exists l
  9. L37
    apply beta_matrix_minor_point_exists
  10. L38
    exact hq
10Use earlier factsL39–48

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

  1. L39
    specialize beta_matrix_minor_prefix_extend b
  2. L40
    specialize beta_matrix_minor_prefix_extend c
  3. L41
    specialize beta_matrix_minor_prefix_extend w
  4. L42
    specialize beta_matrix_minor_prefix_extend r
  5. L43
    specialize beta_matrix_minor_prefix_extend d
  6. L44
    specialize beta_matrix_minor_prefix_extend x
  7. L45
    specialize beta_matrix_minor_prefix_extend x1
  8. L46
    specialize beta_matrix_minor_prefix_extend q
  9. L47
    specialize beta_matrix_minor_prefix_extend l
  10. L48
    apply beta_matrix_minor_prefix_extend
11Use earlier factsL49–50

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

  1. L49
    exact hprevious_witness_witness
  2. L50
    exact hpoint

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro r
  5. 0005intro d
  6. 0006intro q
  7. 0007induction l
  8. 0008intro hq
  9. 0009exists 0
  10. 0010exists 0
  11. 0011intro k
  12. 0012intro hk
  13. 0013exfalso
  14. 0014cases hk
  15. 0015have hzero : S k = 0
  16. 0016specialize add_eq_zero_right x
  17. 0017specialize add_eq_zero_right (S k)
  18. 0018apply add_eq_zero_right
  19. 0019exact hk_witness
  20. 0020specialize succ_ne_zero k
  21. 0021apply succ_ne_zero
  22. 0022exact hzero
  23. 0023intro hq
  24. 0024have hprevious : exists u v. (forall ff_index_mdm_prefix_prefix_previous. (exists ff_gap_mdm_lt_prefix_previous_index_bound. ff_gap_mdm_lt_prefix_previous_index_bound + S (ff_index_mdm_prefix_prefix_previous) = (l)) -> exists ff_row_mdm_prefix_prefix_previous ff_column_mdm_prefix_prefix_previous ff_value_mdm_prefix_prefix_previous. (ff_index_mdm_prefix_prefix_previous = (q) * ff_row_mdm_prefix_prefix_previous + ff_column_mdm_prefix_prefix_previous /\ ((exists ff_gap_mdm_lt_prefix_previous_column_bound. ff_gap_mdm_lt_prefix_previous_column_bound + S (ff_column_mdm_prefix_prefix_previous) = (q)) /\ ((exists ff_row_mdm_cell_prefix_previous_cell ff_column_mdm_cell_prefix_previous_cell. (((((exists ff_gap_mdm_lt_prefix_previous_cell_row_before. ff_gap_mdm_lt_prefix_previous_cell_row_before + S (ff_row_mdm_prefix_prefix_previous) = (r)) /\ ff_row_mdm_cell_prefix_previous_cell = ff_row_mdm_prefix_prefix_previous) \/ ((exists ff_gap_mdm_le_prefix_previous_cell_row_after. ff_gap_mdm_le_prefix_previous_cell_row_after + (r) = (ff_row_mdm_prefix_prefix_previous)) /\ ff_row_mdm_cell_prefix_previous_cell = S ff_row_mdm_prefix_prefix_previous))) /\ (((((exists ff_gap_mdm_lt_prefix_previous_cell_column_before. ff_gap_mdm_lt_prefix_previous_cell_column_before + S (ff_column_mdm_prefix_prefix_previous) = (d)) /\ ff_column_mdm_cell_prefix_previous_cell = ff_column_mdm_prefix_prefix_previous) \/ ((exists ff_gap_mdm_le_prefix_previous_cell_column_after. ff_gap_mdm_le_prefix_previous_cell_column_after + (d) = (ff_column_mdm_prefix_prefix_previous)) /\ ff_column_mdm_cell_prefix_previous_cell = S ff_column_mdm_prefix_prefix_previous))) /\ (((exists ff_h_mdm_prefix_previous_cell_source. ff_h_mdm_prefix_previous_cell_source + S (ff_value_mdm_prefix_prefix_previous) = S ((S ((ff_row_mdm_cell_prefix_previous_cell) * (w) + (ff_column_mdm_cell_prefix_previous_cell))) * c)) /\ exists ff_q_mdm_prefix_previous_cell_source. b = ff_q_mdm_prefix_previous_cell_source * S ((S ((ff_row_mdm_cell_prefix_previous_cell) * (w) + (ff_column_mdm_cell_prefix_previous_cell))) * c) + (ff_value_mdm_prefix_prefix_previous)))))) /\ (((exists ff_h_mdm_prefix_previous_target. ff_h_mdm_prefix_previous_target + S (ff_value_mdm_prefix_prefix_previous) = S ((S (ff_index_mdm_prefix_prefix_previous)) * v)) /\ exists ff_q_mdm_prefix_previous_target. u = ff_q_mdm_prefix_previous_target * S ((S (ff_index_mdm_prefix_prefix_previous)) * v) + (ff_value_mdm_prefix_prefix_previous)))))))
  25. 0025apply IH
  26. 0026exact hq
  27. 0027cases hprevious
  28. 0028cases hprevious_witness
  29. 0029have hpoint : exists ff_row_mdm_point_exists_have_point ff_column_mdm_point_exists_have_point ff_value_mdm_point_exists_have_point. (l = (q) * ff_row_mdm_point_exists_have_point + ff_column_mdm_point_exists_have_point /\ ((exists ff_gap_mdm_lt_exists_have_point_column_bound. ff_gap_mdm_lt_exists_have_point_column_bound + S (ff_column_mdm_point_exists_have_point) = (q)) /\ (exists ff_row_mdm_cell_exists_have_point_cell ff_column_mdm_cell_exists_have_point_cell. (((((exists ff_gap_mdm_lt_exists_have_point_cell_row_before. ff_gap_mdm_lt_exists_have_point_cell_row_before + S (ff_row_mdm_point_exists_have_point) = (r)) /\ ff_row_mdm_cell_exists_have_point_cell = ff_row_mdm_point_exists_have_point) \/ ((exists ff_gap_mdm_le_exists_have_point_cell_row_after. ff_gap_mdm_le_exists_have_point_cell_row_after + (r) = (ff_row_mdm_point_exists_have_point)) /\ ff_row_mdm_cell_exists_have_point_cell = S ff_row_mdm_point_exists_have_point))) /\ (((((exists ff_gap_mdm_lt_exists_have_point_cell_column_before. ff_gap_mdm_lt_exists_have_point_cell_column_before + S (ff_column_mdm_point_exists_have_point) = (d)) /\ ff_column_mdm_cell_exists_have_point_cell = ff_column_mdm_point_exists_have_point) \/ ((exists ff_gap_mdm_le_exists_have_point_cell_column_after. ff_gap_mdm_le_exists_have_point_cell_column_after + (d) = (ff_column_mdm_point_exists_have_point)) /\ ff_column_mdm_cell_exists_have_point_cell = S ff_column_mdm_point_exists_have_point))) /\ (((exists ff_h_mdm_exists_have_point_cell_source. ff_h_mdm_exists_have_point_cell_source + S (ff_value_mdm_point_exists_have_point) = S ((S ((ff_row_mdm_cell_exists_have_point_cell) * (w) + (ff_column_mdm_cell_exists_have_point_cell))) * c)) /\ exists ff_q_mdm_exists_have_point_cell_source. b = ff_q_mdm_exists_have_point_cell_source * S ((S ((ff_row_mdm_cell_exists_have_point_cell) * (w) + (ff_column_mdm_cell_exists_have_point_cell))) * c) + (ff_value_mdm_point_exists_have_point))))))))
  30. 0030specialize beta_matrix_minor_point_exists b
  31. 0031specialize beta_matrix_minor_point_exists c
  32. 0032specialize beta_matrix_minor_point_exists w
  33. 0033specialize beta_matrix_minor_point_exists r
  34. 0034specialize beta_matrix_minor_point_exists d
  35. 0035specialize beta_matrix_minor_point_exists q
  36. 0036specialize beta_matrix_minor_point_exists l
  37. 0037apply beta_matrix_minor_point_exists
  38. 0038exact hq
  39. 0039specialize beta_matrix_minor_prefix_extend b
  40. 0040specialize beta_matrix_minor_prefix_extend c
  41. 0041specialize beta_matrix_minor_prefix_extend w
  42. 0042specialize beta_matrix_minor_prefix_extend r
  43. 0043specialize beta_matrix_minor_prefix_extend d
  44. 0044specialize beta_matrix_minor_prefix_extend x
  45. 0045specialize beta_matrix_minor_prefix_extend x1
  46. 0046specialize beta_matrix_minor_prefix_extend q
  47. 0047specialize beta_matrix_minor_prefix_extend l
  48. 0048apply beta_matrix_minor_prefix_extend
  49. 0049exact hprevious_witness_witness
  50. 0050exact hpoint