MN0005

beta_matrix_minor_cell_exists

Every coordinate of an arbitrary deleted-row/deleted-column matrix minor has its exact decoded source value.

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. ∀ i. ∀ j. ∃ z. MatrixMinorCell(b,c,w,r,d,i,j,z)

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

Definition DAG

MatrixMinorCell(b,c,w,r,d,i,j,z) · 1

Actual proof prerequisites

matrix_skip_index_existsbeta_at_exists · checked external prerequisite
Original expanded first-order statement 
forall b c w r d i j. exists z. (exists ff_row_mdm_cell_cell_result ff_column_mdm_cell_cell_result. (((((exists ff_gap_mdm_lt_cell_result_row_before. ff_gap_mdm_lt_cell_result_row_before + S (i) = (r)) /\ ff_row_mdm_cell_cell_result = i) \/ ((exists ff_gap_mdm_le_cell_result_row_after. ff_gap_mdm_le_cell_result_row_after + (r) = (i)) /\ ff_row_mdm_cell_cell_result = S i))) /\ (((((exists ff_gap_mdm_lt_cell_result_column_before. ff_gap_mdm_lt_cell_result_column_before + S (j) = (d)) /\ ff_column_mdm_cell_cell_result = j) \/ ((exists ff_gap_mdm_le_cell_result_column_after. ff_gap_mdm_le_cell_result_column_after + (d) = (j)) /\ ff_column_mdm_cell_cell_result = S j))) /\ (((exists ff_h_mdm_cell_result_source. ff_h_mdm_cell_result_source + S (z) = S ((S ((ff_row_mdm_cell_cell_result) * (w) + (ff_column_mdm_cell_cell_result))) * c)) /\ exists ff_q_mdm_cell_result_source. b = ff_q_mdm_cell_result_source * S ((S ((ff_row_mdm_cell_cell_result) * (w) + (ff_column_mdm_cell_cell_result))) * c) + (z))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

31 script commands · 12 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 (1)
matrix skip index exists
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 i
  7. L7
    intro j
02Establish hrowL8–11

Establish this local claim before using it. It is not an additional assumption.

  1. L8
    have hrow : exists s. ((((exists ff_gap_mdm_lt_cell_have_row_before. ff_gap_mdm_lt_cell_have_row_before + S (i) = (r)) /\ s = i) \/ ((exists ff_gap_mdm_le_cell_have_row_after. ff_gap_mdm_le_cell_have_row_after + (r) = (i)) /\ s = S i)))
  2. L9
    specialize matrix_skip_index_exists i
  3. L10
    specialize matrix_skip_index_exists r
  4. L11
    exact matrix_skip_index_exists
03Separate the logical casesL12–12

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

  1. L12
    cases hrow
04Establish hcolumnL13–16

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hcolumn : exists s. ((((exists ff_gap_mdm_lt_cell_have_column_before. ff_gap_mdm_lt_cell_have_column_before + S (j) = (d)) /\ s = j) \/ ((exists ff_gap_mdm_le_cell_have_column_after. ff_gap_mdm_le_cell_have_column_after + (d) = (j)) /\ s = S j)))
  2. L14
    specialize matrix_skip_index_exists j
  3. L15
    specialize matrix_skip_index_exists d
  4. L16
    exact matrix_skip_index_exists
05Separate the logical casesL17–17

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

  1. L17
    cases hcolumn
06Establish hvalueL18–22

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hvalue : exists z. (((exists ff_h_mdm_cell_have_value. ff_h_mdm_cell_have_value + S (z) = S ((S (x * w + x1)) * c)) /\ exists ff_q_mdm_cell_have_value. b = ff_q_mdm_cell_have_value * S ((S (x * w + x1)) * c) + (z)))
  2. L19
    specialize beta_at_exists b
  3. L20
    specialize beta_at_exists c
  4. L21
    specialize beta_at_exists (x * w + x1)
  5. L22
    exact beta_at_exists
07Separate the logical casesL23–23

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

  1. L23
    cases hvalue
08Construct an explicit witnessL24–26

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

  1. L24
    exists x2
  2. L25
    exists x
  3. L26
    exists x1
09Separate the logical casesL27–27

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

  1. L27
    split
10Use earlier factsL28–28

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

  1. L28
    exact hrow_witness
11Separate the logical casesL29–29

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

  1. L29
    split
12Use earlier factsL30–31

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

  1. L30
    exact hcolumn_witness
  2. L31
    exact hvalue_witness

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro r
  5. 0005intro d
  6. 0006intro i
  7. 0007intro j
  8. 0008have hrow : exists s. ((((exists ff_gap_mdm_lt_cell_have_row_before. ff_gap_mdm_lt_cell_have_row_before + S (i) = (r)) /\ s = i) \/ ((exists ff_gap_mdm_le_cell_have_row_after. ff_gap_mdm_le_cell_have_row_after + (r) = (i)) /\ s = S i)))
  9. 0009specialize matrix_skip_index_exists i
  10. 0010specialize matrix_skip_index_exists r
  11. 0011exact matrix_skip_index_exists
  12. 0012cases hrow
  13. 0013have hcolumn : exists s. ((((exists ff_gap_mdm_lt_cell_have_column_before. ff_gap_mdm_lt_cell_have_column_before + S (j) = (d)) /\ s = j) \/ ((exists ff_gap_mdm_le_cell_have_column_after. ff_gap_mdm_le_cell_have_column_after + (d) = (j)) /\ s = S j)))
  14. 0014specialize matrix_skip_index_exists j
  15. 0015specialize matrix_skip_index_exists d
  16. 0016exact matrix_skip_index_exists
  17. 0017cases hcolumn
  18. 0018have hvalue : exists z. (((exists ff_h_mdm_cell_have_value. ff_h_mdm_cell_have_value + S (z) = S ((S (x * w + x1)) * c)) /\ exists ff_q_mdm_cell_have_value. b = ff_q_mdm_cell_have_value * S ((S (x * w + x1)) * c) + (z)))
  19. 0019specialize beta_at_exists b
  20. 0020specialize beta_at_exists c
  21. 0021specialize beta_at_exists (x * w + x1)
  22. 0022exact beta_at_exists
  23. 0023cases hvalue
  24. 0024exists x2
  25. 0025exists x
  26. 0026exists x1
  27. 0027split
  28. 0028exact hrow_witness
  29. 0029split
  30. 0030exact hcolumn_witness
  31. 0031exact hvalue_witness