MN000B

beta_matrix_minor_prefix_exists

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

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

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 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)))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized MN000A beta_matrix_minor_prefix_empty_exists MN0009 beta_matrix_minor_prefix_exists_nonzero

Direct dependents

MN000C beta_matrix_minor_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

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.

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 exact 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

Separate complete second-wave branches: Full T13 proof · Alpha v27.