MN000D

beta_signed_matrix_minor_exists

Every arbitrary-dimensional signed integer matrix has the complete exact beta-coded minor obtained by deleting any valid row and column.

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

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ q. ∀ r. ∀ d. Lt(r,S q) → Lt(d,S q) → ∃ x. ∃ y. ∃ z. ∃ n. SignedMatrixMinor(pb,pc,nb,nc,S q,r,d,q,x,y,z,n)

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

Definition DAG

SignedMatrixMinor(pb,pc,nb,nc,w,r,d,q,up,us,un,ut) · 1Lt(a,b) · 2

Actual proof prerequisites

beta_matrix_minor_exists
Original expanded first-order statement 
forall pb pc nb nc q r d. (exists ff_gap_mdm_lt_removed_row. ff_gap_mdm_lt_removed_row + S (r) = (S q)) -> (exists ff_gap_mdm_lt_removed_column. ff_gap_mdm_lt_removed_column + S (d) = (S q)) -> exists up us un ut. (((forall ff_index_mdm_prefix_signed_minor_positive. (exists ff_gap_mdm_lt_signed_minor_positive_index_bound. ff_gap_mdm_lt_signed_minor_positive_index_bound + S (ff_index_mdm_prefix_signed_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_signed_minor_positive ff_column_mdm_prefix_signed_minor_positive ff_value_mdm_prefix_signed_minor_positive. (ff_index_mdm_prefix_signed_minor_positive = (q) * ff_row_mdm_prefix_signed_minor_positive + ff_column_mdm_prefix_signed_minor_positive /\ ((exists ff_gap_mdm_lt_signed_minor_positive_column_bound. ff_gap_mdm_lt_signed_minor_positive_column_bound + S (ff_column_mdm_prefix_signed_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_signed_minor_positive_cell ff_column_mdm_cell_signed_minor_positive_cell. (((((exists ff_gap_mdm_lt_signed_minor_positive_cell_row_before. ff_gap_mdm_lt_signed_minor_positive_cell_row_before + S (ff_row_mdm_prefix_signed_minor_positive) = (r)) /\ ff_row_mdm_cell_signed_minor_positive_cell = ff_row_mdm_prefix_signed_minor_positive) \/ ((exists ff_gap_mdm_le_signed_minor_positive_cell_row_after. ff_gap_mdm_le_signed_minor_positive_cell_row_after + (r) = (ff_row_mdm_prefix_signed_minor_positive)) /\ ff_row_mdm_cell_signed_minor_positive_cell = S ff_row_mdm_prefix_signed_minor_positive))) /\ (((((exists ff_gap_mdm_lt_signed_minor_positive_cell_column_before. ff_gap_mdm_lt_signed_minor_positive_cell_column_before + S (ff_column_mdm_prefix_signed_minor_positive) = (d)) /\ ff_column_mdm_cell_signed_minor_positive_cell = ff_column_mdm_prefix_signed_minor_positive) \/ ((exists ff_gap_mdm_le_signed_minor_positive_cell_column_after. ff_gap_mdm_le_signed_minor_positive_cell_column_after + (d) = (ff_column_mdm_prefix_signed_minor_positive)) /\ ff_column_mdm_cell_signed_minor_positive_cell = S ff_column_mdm_prefix_signed_minor_positive))) /\ (((exists ff_h_mdm_signed_minor_positive_cell_source. ff_h_mdm_signed_minor_positive_cell_source + S (ff_value_mdm_prefix_signed_minor_positive) = S ((S ((ff_row_mdm_cell_signed_minor_positive_cell) * (S q) + (ff_column_mdm_cell_signed_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_signed_minor_positive_cell_source. pb = ff_q_mdm_signed_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_signed_minor_positive_cell) * (S q) + (ff_column_mdm_cell_signed_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_signed_minor_positive)))))) /\ (((exists ff_h_mdm_signed_minor_positive_target. ff_h_mdm_signed_minor_positive_target + S (ff_value_mdm_prefix_signed_minor_positive) = S ((S (ff_index_mdm_prefix_signed_minor_positive)) * us)) /\ exists ff_q_mdm_signed_minor_positive_target. up = ff_q_mdm_signed_minor_positive_target * S ((S (ff_index_mdm_prefix_signed_minor_positive)) * us) + (ff_value_mdm_prefix_signed_minor_positive))))))) /\ (forall ff_index_mdm_prefix_signed_minor_negative. (exists ff_gap_mdm_lt_signed_minor_negative_index_bound. ff_gap_mdm_lt_signed_minor_negative_index_bound + S (ff_index_mdm_prefix_signed_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_signed_minor_negative ff_column_mdm_prefix_signed_minor_negative ff_value_mdm_prefix_signed_minor_negative. (ff_index_mdm_prefix_signed_minor_negative = (q) * ff_row_mdm_prefix_signed_minor_negative + ff_column_mdm_prefix_signed_minor_negative /\ ((exists ff_gap_mdm_lt_signed_minor_negative_column_bound. ff_gap_mdm_lt_signed_minor_negative_column_bound + S (ff_column_mdm_prefix_signed_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_signed_minor_negative_cell ff_column_mdm_cell_signed_minor_negative_cell. (((((exists ff_gap_mdm_lt_signed_minor_negative_cell_row_before. ff_gap_mdm_lt_signed_minor_negative_cell_row_before + S (ff_row_mdm_prefix_signed_minor_negative) = (r)) /\ ff_row_mdm_cell_signed_minor_negative_cell = ff_row_mdm_prefix_signed_minor_negative) \/ ((exists ff_gap_mdm_le_signed_minor_negative_cell_row_after. ff_gap_mdm_le_signed_minor_negative_cell_row_after + (r) = (ff_row_mdm_prefix_signed_minor_negative)) /\ ff_row_mdm_cell_signed_minor_negative_cell = S ff_row_mdm_prefix_signed_minor_negative))) /\ (((((exists ff_gap_mdm_lt_signed_minor_negative_cell_column_before. ff_gap_mdm_lt_signed_minor_negative_cell_column_before + S (ff_column_mdm_prefix_signed_minor_negative) = (d)) /\ ff_column_mdm_cell_signed_minor_negative_cell = ff_column_mdm_prefix_signed_minor_negative) \/ ((exists ff_gap_mdm_le_signed_minor_negative_cell_column_after. ff_gap_mdm_le_signed_minor_negative_cell_column_after + (d) = (ff_column_mdm_prefix_signed_minor_negative)) /\ ff_column_mdm_cell_signed_minor_negative_cell = S ff_column_mdm_prefix_signed_minor_negative))) /\ (((exists ff_h_mdm_signed_minor_negative_cell_source. ff_h_mdm_signed_minor_negative_cell_source + S (ff_value_mdm_prefix_signed_minor_negative) = S ((S ((ff_row_mdm_cell_signed_minor_negative_cell) * (S q) + (ff_column_mdm_cell_signed_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_signed_minor_negative_cell_source. nb = ff_q_mdm_signed_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_signed_minor_negative_cell) * (S q) + (ff_column_mdm_cell_signed_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_signed_minor_negative)))))) /\ (((exists ff_h_mdm_signed_minor_negative_target. ff_h_mdm_signed_minor_negative_target + S (ff_value_mdm_prefix_signed_minor_negative) = S ((S (ff_index_mdm_prefix_signed_minor_negative)) * ut)) /\ exists ff_q_mdm_signed_minor_negative_target. un = ff_q_mdm_signed_minor_negative_target * S ((S (ff_index_mdm_prefix_signed_minor_negative)) * ut) + (ff_value_mdm_prefix_signed_minor_negative)))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

38 script commands · 8 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 (1)
beta matrix minor exists

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

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro q
  6. L6
    intro r
  7. L7
    intro d
  8. L8
    intro hrow
  9. L9
    intro hcolumn
02Establish hpositiveL10–18

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

  1. L10
    have hpositive : ∃ up. ∃ us. MatrixMinorPrefix(pb,pc,S q,r,d,up,us,q,q · q)Definitions: MatrixMinorPrefixOriginal native command in the exact edition
  2. L11
    specialize beta_matrix_minor_exists pb
  3. L12
    specialize beta_matrix_minor_exists pc
  4. L13
    specialize beta_matrix_minor_exists q
  5. L14
    specialize beta_matrix_minor_exists r
  6. L15
    specialize beta_matrix_minor_exists d
  7. L16
    apply beta_matrix_minor_exists
  8. L17
    exact hrow
  9. L18
    exact hcolumn
03Separate the logical casesL19–20

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

  1. L19
    cases hpositive
  2. L20
    cases hpositive_witness
04Establish hnegativeL21–29

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

  1. L21
    have hnegative : ∃ un. ∃ ut. MatrixMinorPrefix(nb,nc,S q,r,d,un,ut,q,q · q)Definitions: MatrixMinorPrefixOriginal native command in the exact edition
  2. L22
    specialize beta_matrix_minor_exists nb
  3. L23
    specialize beta_matrix_minor_exists nc
  4. L24
    specialize beta_matrix_minor_exists q
  5. L25
    specialize beta_matrix_minor_exists r
  6. L26
    specialize beta_matrix_minor_exists d
  7. L27
    apply beta_matrix_minor_exists
  8. L28
    exact hrow
  9. L29
    exact hcolumn
05Separate the logical casesL30–31

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

  1. L30
    cases hnegative
  2. L31
    cases hnegative_witness
06Construct an explicit witnessL32–35

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

  1. L32
    exists x
  2. L33
    exists x1
  3. L34
    exists x2
  4. L35
    exists x3
07Separate the logical casesL36–36

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

  1. L36
    split
08Use earlier factsL37–38

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

  1. L37
    exact hpositive_witness_witness
  2. L38
    exact hnegative_witness_witness

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro q
  6. 0006intro r
  7. 0007intro d
  8. 0008intro hrow
  9. 0009intro hcolumn
  10. 0010have hpositive : exists up us. (forall ff_index_mdm_prefix_signed_have_positive. (exists ff_gap_mdm_lt_signed_have_positive_index_bound. ff_gap_mdm_lt_signed_have_positive_index_bound + S (ff_index_mdm_prefix_signed_have_positive) = (q * q)) -> exists ff_row_mdm_prefix_signed_have_positive ff_column_mdm_prefix_signed_have_positive ff_value_mdm_prefix_signed_have_positive. (ff_index_mdm_prefix_signed_have_positive = (q) * ff_row_mdm_prefix_signed_have_positive + ff_column_mdm_prefix_signed_have_positive /\ ((exists ff_gap_mdm_lt_signed_have_positive_column_bound. ff_gap_mdm_lt_signed_have_positive_column_bound + S (ff_column_mdm_prefix_signed_have_positive) = (q)) /\ ((exists ff_row_mdm_cell_signed_have_positive_cell ff_column_mdm_cell_signed_have_positive_cell. (((((exists ff_gap_mdm_lt_signed_have_positive_cell_row_before. ff_gap_mdm_lt_signed_have_positive_cell_row_before + S (ff_row_mdm_prefix_signed_have_positive) = (r)) /\ ff_row_mdm_cell_signed_have_positive_cell = ff_row_mdm_prefix_signed_have_positive) \/ ((exists ff_gap_mdm_le_signed_have_positive_cell_row_after. ff_gap_mdm_le_signed_have_positive_cell_row_after + (r) = (ff_row_mdm_prefix_signed_have_positive)) /\ ff_row_mdm_cell_signed_have_positive_cell = S ff_row_mdm_prefix_signed_have_positive))) /\ (((((exists ff_gap_mdm_lt_signed_have_positive_cell_column_before. ff_gap_mdm_lt_signed_have_positive_cell_column_before + S (ff_column_mdm_prefix_signed_have_positive) = (d)) /\ ff_column_mdm_cell_signed_have_positive_cell = ff_column_mdm_prefix_signed_have_positive) \/ ((exists ff_gap_mdm_le_signed_have_positive_cell_column_after. ff_gap_mdm_le_signed_have_positive_cell_column_after + (d) = (ff_column_mdm_prefix_signed_have_positive)) /\ ff_column_mdm_cell_signed_have_positive_cell = S ff_column_mdm_prefix_signed_have_positive))) /\ (((exists ff_h_mdm_signed_have_positive_cell_source. ff_h_mdm_signed_have_positive_cell_source + S (ff_value_mdm_prefix_signed_have_positive) = S ((S ((ff_row_mdm_cell_signed_have_positive_cell) * (S q) + (ff_column_mdm_cell_signed_have_positive_cell))) * pc)) /\ exists ff_q_mdm_signed_have_positive_cell_source. pb = ff_q_mdm_signed_have_positive_cell_source * S ((S ((ff_row_mdm_cell_signed_have_positive_cell) * (S q) + (ff_column_mdm_cell_signed_have_positive_cell))) * pc) + (ff_value_mdm_prefix_signed_have_positive)))))) /\ (((exists ff_h_mdm_signed_have_positive_target. ff_h_mdm_signed_have_positive_target + S (ff_value_mdm_prefix_signed_have_positive) = S ((S (ff_index_mdm_prefix_signed_have_positive)) * us)) /\ exists ff_q_mdm_signed_have_positive_target. up = ff_q_mdm_signed_have_positive_target * S ((S (ff_index_mdm_prefix_signed_have_positive)) * us) + (ff_value_mdm_prefix_signed_have_positive)))))))
  11. 0011specialize beta_matrix_minor_exists pb
  12. 0012specialize beta_matrix_minor_exists pc
  13. 0013specialize beta_matrix_minor_exists q
  14. 0014specialize beta_matrix_minor_exists r
  15. 0015specialize beta_matrix_minor_exists d
  16. 0016apply beta_matrix_minor_exists
  17. 0017exact hrow
  18. 0018exact hcolumn
  19. 0019cases hpositive
  20. 0020cases hpositive_witness
  21. 0021have hnegative : exists un ut. (forall ff_index_mdm_prefix_signed_have_negative. (exists ff_gap_mdm_lt_signed_have_negative_index_bound. ff_gap_mdm_lt_signed_have_negative_index_bound + S (ff_index_mdm_prefix_signed_have_negative) = (q * q)) -> exists ff_row_mdm_prefix_signed_have_negative ff_column_mdm_prefix_signed_have_negative ff_value_mdm_prefix_signed_have_negative. (ff_index_mdm_prefix_signed_have_negative = (q) * ff_row_mdm_prefix_signed_have_negative + ff_column_mdm_prefix_signed_have_negative /\ ((exists ff_gap_mdm_lt_signed_have_negative_column_bound. ff_gap_mdm_lt_signed_have_negative_column_bound + S (ff_column_mdm_prefix_signed_have_negative) = (q)) /\ ((exists ff_row_mdm_cell_signed_have_negative_cell ff_column_mdm_cell_signed_have_negative_cell. (((((exists ff_gap_mdm_lt_signed_have_negative_cell_row_before. ff_gap_mdm_lt_signed_have_negative_cell_row_before + S (ff_row_mdm_prefix_signed_have_negative) = (r)) /\ ff_row_mdm_cell_signed_have_negative_cell = ff_row_mdm_prefix_signed_have_negative) \/ ((exists ff_gap_mdm_le_signed_have_negative_cell_row_after. ff_gap_mdm_le_signed_have_negative_cell_row_after + (r) = (ff_row_mdm_prefix_signed_have_negative)) /\ ff_row_mdm_cell_signed_have_negative_cell = S ff_row_mdm_prefix_signed_have_negative))) /\ (((((exists ff_gap_mdm_lt_signed_have_negative_cell_column_before. ff_gap_mdm_lt_signed_have_negative_cell_column_before + S (ff_column_mdm_prefix_signed_have_negative) = (d)) /\ ff_column_mdm_cell_signed_have_negative_cell = ff_column_mdm_prefix_signed_have_negative) \/ ((exists ff_gap_mdm_le_signed_have_negative_cell_column_after. ff_gap_mdm_le_signed_have_negative_cell_column_after + (d) = (ff_column_mdm_prefix_signed_have_negative)) /\ ff_column_mdm_cell_signed_have_negative_cell = S ff_column_mdm_prefix_signed_have_negative))) /\ (((exists ff_h_mdm_signed_have_negative_cell_source. ff_h_mdm_signed_have_negative_cell_source + S (ff_value_mdm_prefix_signed_have_negative) = S ((S ((ff_row_mdm_cell_signed_have_negative_cell) * (S q) + (ff_column_mdm_cell_signed_have_negative_cell))) * nc)) /\ exists ff_q_mdm_signed_have_negative_cell_source. nb = ff_q_mdm_signed_have_negative_cell_source * S ((S ((ff_row_mdm_cell_signed_have_negative_cell) * (S q) + (ff_column_mdm_cell_signed_have_negative_cell))) * nc) + (ff_value_mdm_prefix_signed_have_negative)))))) /\ (((exists ff_h_mdm_signed_have_negative_target. ff_h_mdm_signed_have_negative_target + S (ff_value_mdm_prefix_signed_have_negative) = S ((S (ff_index_mdm_prefix_signed_have_negative)) * ut)) /\ exists ff_q_mdm_signed_have_negative_target. un = ff_q_mdm_signed_have_negative_target * S ((S (ff_index_mdm_prefix_signed_have_negative)) * ut) + (ff_value_mdm_prefix_signed_have_negative)))))))
  22. 0022specialize beta_matrix_minor_exists nb
  23. 0023specialize beta_matrix_minor_exists nc
  24. 0024specialize beta_matrix_minor_exists q
  25. 0025specialize beta_matrix_minor_exists r
  26. 0026specialize beta_matrix_minor_exists d
  27. 0027apply beta_matrix_minor_exists
  28. 0028exact hrow
  29. 0029exact hcolumn
  30. 0030cases hnegative
  31. 0031cases hnegative_witness
  32. 0032exists x
  33. 0033exists x1
  34. 0034exists x2
  35. 0035exists x3
  36. 0036split
  37. 0037exact hpositive_witness_witness
  38. 0038exact hnegative_witness_witness