MN0005

beta_matrix_minor_cell_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 31 exact native proof lines.

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

Proof neighborhood

Direct dependencies

MN0001 matrix_skip_index_exists beta_at_exists Stable theorem; checked-use authorized

Direct dependents

MN0007 beta_matrix_minor_point_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

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.

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

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