MN000B

beta_matrix_minor_prefix_exists

Every arbitrary finite rectangular deleted-row/deleted-column matrix prefix is beta-coded, including width zero.

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. ∀ h. ∃ u. ∃ v. MatrixMinorPrefix(b,c,w,r,d,u,v,q,h · q)

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

eq_decidable · checked external prerequisitebeta_matrix_minor_prefix_empty_existsbeta_matrix_minor_prefix_exists_nonzero
Original expanded first-order statement 
forall b c w r d q h. exists u v. (forall ff_index_mdm_prefix_prefix_full. (exists ff_gap_mdm_lt_prefix_full_index_bound. ff_gap_mdm_lt_prefix_full_index_bound + S (ff_index_mdm_prefix_prefix_full) = (h * q)) -> exists ff_row_mdm_prefix_prefix_full ff_column_mdm_prefix_prefix_full ff_value_mdm_prefix_prefix_full. (ff_index_mdm_prefix_prefix_full = (q) * ff_row_mdm_prefix_prefix_full + ff_column_mdm_prefix_prefix_full /\ ((exists ff_gap_mdm_lt_prefix_full_column_bound. ff_gap_mdm_lt_prefix_full_column_bound + S (ff_column_mdm_prefix_prefix_full) = (q)) /\ ((exists ff_row_mdm_cell_prefix_full_cell ff_column_mdm_cell_prefix_full_cell. (((((exists ff_gap_mdm_lt_prefix_full_cell_row_before. ff_gap_mdm_lt_prefix_full_cell_row_before + S (ff_row_mdm_prefix_prefix_full) = (r)) /\ ff_row_mdm_cell_prefix_full_cell = ff_row_mdm_prefix_prefix_full) \/ ((exists ff_gap_mdm_le_prefix_full_cell_row_after. ff_gap_mdm_le_prefix_full_cell_row_after + (r) = (ff_row_mdm_prefix_prefix_full)) /\ ff_row_mdm_cell_prefix_full_cell = S ff_row_mdm_prefix_prefix_full))) /\ (((((exists ff_gap_mdm_lt_prefix_full_cell_column_before. ff_gap_mdm_lt_prefix_full_cell_column_before + S (ff_column_mdm_prefix_prefix_full) = (d)) /\ ff_column_mdm_cell_prefix_full_cell = ff_column_mdm_prefix_prefix_full) \/ ((exists ff_gap_mdm_le_prefix_full_cell_column_after. ff_gap_mdm_le_prefix_full_cell_column_after + (d) = (ff_column_mdm_prefix_prefix_full)) /\ ff_column_mdm_cell_prefix_full_cell = S ff_column_mdm_prefix_prefix_full))) /\ (((exists ff_h_mdm_prefix_full_cell_source. ff_h_mdm_prefix_full_cell_source + S (ff_value_mdm_prefix_prefix_full) = S ((S ((ff_row_mdm_cell_prefix_full_cell) * (w) + (ff_column_mdm_cell_prefix_full_cell))) * c)) /\ exists ff_q_mdm_prefix_full_cell_source. b = ff_q_mdm_prefix_full_cell_source * S ((S ((ff_row_mdm_cell_prefix_full_cell) * (w) + (ff_column_mdm_cell_prefix_full_cell))) * c) + (ff_value_mdm_prefix_prefix_full)))))) /\ (((exists ff_h_mdm_prefix_full_target. ff_h_mdm_prefix_full_target + S (ff_value_mdm_prefix_prefix_full) = S ((S (ff_index_mdm_prefix_prefix_full)) * v)) /\ exists ff_q_mdm_prefix_full_target. u = ff_q_mdm_prefix_full_target * S ((S (ff_index_mdm_prefix_prefix_full)) * v) + (ff_value_mdm_prefix_prefix_full)))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

30 script commands · 5 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.

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 prefix empty existsbeta matrix minor prefix exists nonzero
01Fix variables and assumptionsL1–7

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
  7. L7
    intro h
02Use earlier factsL8–9

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

  1. L8
    specialize eq_decidable q
  2. L9
    specialize eq_decidable 0
03Separate the logical casesL10–10

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

  1. L10
    cases eq_decidable
04Establish hlengthL11–20

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

  1. L11
    have hlength : h * q = 0
  2. L12
    rewrite eq_decidable_left
  3. L13
    apply PA5
  4. L14
    rewrite hlength
  5. L15
    specialize beta_matrix_minor_prefix_empty_exists b
  6. L16
    specialize beta_matrix_minor_prefix_empty_exists c
  7. L17
    specialize beta_matrix_minor_prefix_empty_exists w
  8. L18
    specialize beta_matrix_minor_prefix_empty_exists r
  9. L19
    specialize beta_matrix_minor_prefix_empty_exists d
  10. L20
    specialize beta_matrix_minor_prefix_empty_exists q
05Use earlier factsL21–30

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

  1. L21
    exact beta_matrix_minor_prefix_empty_exists
  2. L22
    specialize beta_matrix_minor_prefix_exists_nonzero b
  3. L23
    specialize beta_matrix_minor_prefix_exists_nonzero c
  4. L24
    specialize beta_matrix_minor_prefix_exists_nonzero w
  5. L25
    specialize beta_matrix_minor_prefix_exists_nonzero r
  6. L26
    specialize beta_matrix_minor_prefix_exists_nonzero d
  7. L27
    specialize beta_matrix_minor_prefix_exists_nonzero q
  8. L28
    specialize beta_matrix_minor_prefix_exists_nonzero (h * q)
  9. L29
    apply beta_matrix_minor_prefix_exists_nonzero
  10. L30
    exact eq_decidable_right

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro r
  5. 0005intro d
  6. 0006intro q
  7. 0007intro h
  8. 0008specialize eq_decidable q
  9. 0009specialize eq_decidable 0
  10. 0010cases eq_decidable
  11. 0011have hlength : h * q = 0
  12. 0012rewrite eq_decidable_left
  13. 0013apply PA5
  14. 0014rewrite hlength
  15. 0015specialize beta_matrix_minor_prefix_empty_exists b
  16. 0016specialize beta_matrix_minor_prefix_empty_exists c
  17. 0017specialize beta_matrix_minor_prefix_empty_exists w
  18. 0018specialize beta_matrix_minor_prefix_empty_exists r
  19. 0019specialize beta_matrix_minor_prefix_empty_exists d
  20. 0020specialize beta_matrix_minor_prefix_empty_exists q
  21. 0021exact beta_matrix_minor_prefix_empty_exists
  22. 0022specialize beta_matrix_minor_prefix_exists_nonzero b
  23. 0023specialize beta_matrix_minor_prefix_exists_nonzero c
  24. 0024specialize beta_matrix_minor_prefix_exists_nonzero w
  25. 0025specialize beta_matrix_minor_prefix_exists_nonzero r
  26. 0026specialize beta_matrix_minor_prefix_exists_nonzero d
  27. 0027specialize beta_matrix_minor_prefix_exists_nonzero q
  28. 0028specialize beta_matrix_minor_prefix_exists_nonzero (h * q)
  29. 0029apply beta_matrix_minor_prefix_exists_nonzero
  30. 0030exact eq_decidable_right