MN0008

beta_matrix_minor_prefix_extend

Extend one exact row-major beta-coded cofactor minor while preserving every earlier skipped-source entry.

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. ∀ u. ∀ v. ∀ q. ∀ l. MatrixMinorPrefix(b,c,w,r,d,u,v,q,l) → (∃ x. ∃ y. ∃ z. l = q · x + y ∧ (Lt(y,q) ∧ MatrixMinorCell(b,c,w,r,d,x,y,z))) → ∃ x. ∃ y. MatrixMinorPrefix(b,c,w,r,d,x,y,q,S l)

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

Definition DAG

MatrixMinorCell(b,c,w,r,d,i,j,z) · 1MatrixMinorPrefix(b,c,w,r,d,u,v,q,l) · 2Lt(a,b) · 1

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall b c w r d u v q l. (forall ff_index_mdm_prefix_prefix_before. (exists ff_gap_mdm_lt_prefix_before_index_bound. ff_gap_mdm_lt_prefix_before_index_bound + S (ff_index_mdm_prefix_prefix_before) = (l)) -> exists ff_row_mdm_prefix_prefix_before ff_column_mdm_prefix_prefix_before ff_value_mdm_prefix_prefix_before. (ff_index_mdm_prefix_prefix_before = (q) * ff_row_mdm_prefix_prefix_before + ff_column_mdm_prefix_prefix_before /\ ((exists ff_gap_mdm_lt_prefix_before_column_bound. ff_gap_mdm_lt_prefix_before_column_bound + S (ff_column_mdm_prefix_prefix_before) = (q)) /\ ((exists ff_row_mdm_cell_prefix_before_cell ff_column_mdm_cell_prefix_before_cell. (((((exists ff_gap_mdm_lt_prefix_before_cell_row_before. ff_gap_mdm_lt_prefix_before_cell_row_before + S (ff_row_mdm_prefix_prefix_before) = (r)) /\ ff_row_mdm_cell_prefix_before_cell = ff_row_mdm_prefix_prefix_before) \/ ((exists ff_gap_mdm_le_prefix_before_cell_row_after. ff_gap_mdm_le_prefix_before_cell_row_after + (r) = (ff_row_mdm_prefix_prefix_before)) /\ ff_row_mdm_cell_prefix_before_cell = S ff_row_mdm_prefix_prefix_before))) /\ (((((exists ff_gap_mdm_lt_prefix_before_cell_column_before. ff_gap_mdm_lt_prefix_before_cell_column_before + S (ff_column_mdm_prefix_prefix_before) = (d)) /\ ff_column_mdm_cell_prefix_before_cell = ff_column_mdm_prefix_prefix_before) \/ ((exists ff_gap_mdm_le_prefix_before_cell_column_after. ff_gap_mdm_le_prefix_before_cell_column_after + (d) = (ff_column_mdm_prefix_prefix_before)) /\ ff_column_mdm_cell_prefix_before_cell = S ff_column_mdm_prefix_prefix_before))) /\ (((exists ff_h_mdm_prefix_before_cell_source. ff_h_mdm_prefix_before_cell_source + S (ff_value_mdm_prefix_prefix_before) = S ((S ((ff_row_mdm_cell_prefix_before_cell) * (w) + (ff_column_mdm_cell_prefix_before_cell))) * c)) /\ exists ff_q_mdm_prefix_before_cell_source. b = ff_q_mdm_prefix_before_cell_source * S ((S ((ff_row_mdm_cell_prefix_before_cell) * (w) + (ff_column_mdm_cell_prefix_before_cell))) * c) + (ff_value_mdm_prefix_prefix_before)))))) /\ (((exists ff_h_mdm_prefix_before_target. ff_h_mdm_prefix_before_target + S (ff_value_mdm_prefix_prefix_before) = S ((S (ff_index_mdm_prefix_prefix_before)) * v)) /\ exists ff_q_mdm_prefix_before_target. u = ff_q_mdm_prefix_before_target * S ((S (ff_index_mdm_prefix_prefix_before)) * v) + (ff_value_mdm_prefix_prefix_before))))))) -> (exists ff_row_mdm_point_prefix_last ff_column_mdm_point_prefix_last ff_value_mdm_point_prefix_last. (l = (q) * ff_row_mdm_point_prefix_last + ff_column_mdm_point_prefix_last /\ ((exists ff_gap_mdm_lt_prefix_last_column_bound. ff_gap_mdm_lt_prefix_last_column_bound + S (ff_column_mdm_point_prefix_last) = (q)) /\ (exists ff_row_mdm_cell_prefix_last_cell ff_column_mdm_cell_prefix_last_cell. (((((exists ff_gap_mdm_lt_prefix_last_cell_row_before. ff_gap_mdm_lt_prefix_last_cell_row_before + S (ff_row_mdm_point_prefix_last) = (r)) /\ ff_row_mdm_cell_prefix_last_cell = ff_row_mdm_point_prefix_last) \/ ((exists ff_gap_mdm_le_prefix_last_cell_row_after. ff_gap_mdm_le_prefix_last_cell_row_after + (r) = (ff_row_mdm_point_prefix_last)) /\ ff_row_mdm_cell_prefix_last_cell = S ff_row_mdm_point_prefix_last))) /\ (((((exists ff_gap_mdm_lt_prefix_last_cell_column_before. ff_gap_mdm_lt_prefix_last_cell_column_before + S (ff_column_mdm_point_prefix_last) = (d)) /\ ff_column_mdm_cell_prefix_last_cell = ff_column_mdm_point_prefix_last) \/ ((exists ff_gap_mdm_le_prefix_last_cell_column_after. ff_gap_mdm_le_prefix_last_cell_column_after + (d) = (ff_column_mdm_point_prefix_last)) /\ ff_column_mdm_cell_prefix_last_cell = S ff_column_mdm_point_prefix_last))) /\ (((exists ff_h_mdm_prefix_last_cell_source. ff_h_mdm_prefix_last_cell_source + S (ff_value_mdm_point_prefix_last) = S ((S ((ff_row_mdm_cell_prefix_last_cell) * (w) + (ff_column_mdm_cell_prefix_last_cell))) * c)) /\ exists ff_q_mdm_prefix_last_cell_source. b = ff_q_mdm_prefix_last_cell_source * S ((S ((ff_row_mdm_cell_prefix_last_cell) * (w) + (ff_column_mdm_cell_prefix_last_cell))) * c) + (ff_value_mdm_point_prefix_last))))))))) -> exists z e. (forall ff_index_mdm_prefix_prefix_after. (exists ff_gap_mdm_lt_prefix_after_index_bound. ff_gap_mdm_lt_prefix_after_index_bound + S (ff_index_mdm_prefix_prefix_after) = (S l)) -> exists ff_row_mdm_prefix_prefix_after ff_column_mdm_prefix_prefix_after ff_value_mdm_prefix_prefix_after. (ff_index_mdm_prefix_prefix_after = (q) * ff_row_mdm_prefix_prefix_after + ff_column_mdm_prefix_prefix_after /\ ((exists ff_gap_mdm_lt_prefix_after_column_bound. ff_gap_mdm_lt_prefix_after_column_bound + S (ff_column_mdm_prefix_prefix_after) = (q)) /\ ((exists ff_row_mdm_cell_prefix_after_cell ff_column_mdm_cell_prefix_after_cell. (((((exists ff_gap_mdm_lt_prefix_after_cell_row_before. ff_gap_mdm_lt_prefix_after_cell_row_before + S (ff_row_mdm_prefix_prefix_after) = (r)) /\ ff_row_mdm_cell_prefix_after_cell = ff_row_mdm_prefix_prefix_after) \/ ((exists ff_gap_mdm_le_prefix_after_cell_row_after. ff_gap_mdm_le_prefix_after_cell_row_after + (r) = (ff_row_mdm_prefix_prefix_after)) /\ ff_row_mdm_cell_prefix_after_cell = S ff_row_mdm_prefix_prefix_after))) /\ (((((exists ff_gap_mdm_lt_prefix_after_cell_column_before. ff_gap_mdm_lt_prefix_after_cell_column_before + S (ff_column_mdm_prefix_prefix_after) = (d)) /\ ff_column_mdm_cell_prefix_after_cell = ff_column_mdm_prefix_prefix_after) \/ ((exists ff_gap_mdm_le_prefix_after_cell_column_after. ff_gap_mdm_le_prefix_after_cell_column_after + (d) = (ff_column_mdm_prefix_prefix_after)) /\ ff_column_mdm_cell_prefix_after_cell = S ff_column_mdm_prefix_prefix_after))) /\ (((exists ff_h_mdm_prefix_after_cell_source. ff_h_mdm_prefix_after_cell_source + S (ff_value_mdm_prefix_prefix_after) = S ((S ((ff_row_mdm_cell_prefix_after_cell) * (w) + (ff_column_mdm_cell_prefix_after_cell))) * c)) /\ exists ff_q_mdm_prefix_after_cell_source. b = ff_q_mdm_prefix_after_cell_source * S ((S ((ff_row_mdm_cell_prefix_after_cell) * (w) + (ff_column_mdm_cell_prefix_after_cell))) * c) + (ff_value_mdm_prefix_prefix_after)))))) /\ (((exists ff_h_mdm_prefix_after_target. ff_h_mdm_prefix_after_target + S (ff_value_mdm_prefix_prefix_after) = S ((S (ff_index_mdm_prefix_prefix_after)) * e)) /\ exists ff_q_mdm_prefix_after_target. z = ff_q_mdm_prefix_after_target * S ((S (ff_index_mdm_prefix_prefix_after)) * e) + (ff_value_mdm_prefix_prefix_after)))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

70 script commands · 28 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.

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

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 u
  7. L7
    intro v
  8. L8
    intro q
  9. L9
    intro l
  10. L10
    intro hprevious
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hpoint
03Separate the logical casesL12–16

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

  1. L12
    cases hpoint
  2. L13
    cases hpoint_witness
  3. L14
    cases hpoint_witness_witness
  4. L15
    cases hpoint_witness_witness_witness
  5. L16
    cases hpoint_witness_witness_witness_right
04Use earlier factsL17–20

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

  1. L17
    specialize beta_prefix_extend l
  2. L18
    specialize beta_prefix_extend u
  3. L19
    specialize beta_prefix_extend v
  4. L20
    specialize beta_prefix_extend x2
05Separate the logical casesL21–23

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

  1. L21
    cases beta_prefix_extend
  2. L22
    cases beta_prefix_extend_witness
  3. L23
    cases beta_prefix_extend_witness_witness
06Construct an explicit witnessL24–25

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

  1. L24
    exists x3
  2. L25
    exists x4
07Fix variables and assumptionsL26–27

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

  1. L26
    intro k
  2. L27
    intro hk
08Establish hsplitL28–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L28
    have hsplit : k = l \/ exists gap. gap + S k = l
  2. L29
    specialize finite_lt_succ_eq_or_lt l
  3. L30
    specialize finite_lt_succ_eq_or_lt k
  4. L31
    apply finite_lt_succ_eq_or_lt
  5. L32
    exact hk
09Separate the logical casesL33–33

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

  1. L33
    cases hsplit
10Construct an explicit witnessL34–36

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

  1. L34
    exists x
  2. L35
    exists x1
  3. L36
    exists x2
11Separate the logical casesL37–37

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

  1. L37
    split
12Calculate and transport equalitiesL38–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L38
    rewrite hsplit_left
13Use earlier factsL39–39

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

  1. L39
    exact hpoint_witness_witness_witness_left
14Separate the logical casesL40–40

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

  1. L40
    split
15Use earlier factsL41–41

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

  1. L41
    exact hpoint_witness_witness_witness_right_left
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–43

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

  1. L43
    exact hpoint_witness_witness_witness_right_right
18Calculate and transport equalitiesL44–45

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L44
    rewrite hsplit_left
  2. L45
    rewrite hsplit_left
19Use earlier factsL46–46

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

  1. L46
    exact beta_prefix_extend_witness_witness_left
20Establish holdL47–50

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

  1. L47
    have hold : ∃ i. ∃ j. ∃ z. k = q · i + j ∧ (Lt(j,q) ∧ (MatrixMinorCell(b,c,w,r,d,i,j,z) ∧ Beta(u,v,k,z)))Definitions: BetaMatrixMinorCellLtOriginal native command in the exact edition
  2. L48
    specialize hprevious k
  3. L49
    apply hprevious
  4. L50
    exact hsplit_right
21Separate the logical casesL51–56

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

  1. L51
    cases hold
  2. L52
    cases hold_witness
  3. L53
    cases hold_witness_witness
  4. L54
    cases hold_witness_witness_witness
  5. L55
    cases hold_witness_witness_witness_right
  6. L56
    cases hold_witness_witness_witness_right_right
22Construct an explicit witnessL57–59

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

  1. L57
    exists x5
  2. L58
    exists x6
  3. L59
    exists x7
23Separate the logical casesL60–60

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

  1. L60
    split
24Use earlier factsL61–61

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

  1. L61
    exact hold_witness_witness_witness_left
25Separate the logical casesL62–62

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

  1. L62
    split
26Use earlier factsL63–63

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

  1. L63
    exact hold_witness_witness_witness_right_left
27Separate the logical casesL64–64

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

  1. L64
    split
28Use earlier factsL65–70

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

  1. L65
    exact hold_witness_witness_witness_right_right_left
  2. L66
    specialize beta_prefix_extend_witness_witness_right k
  3. L67
    specialize beta_prefix_extend_witness_witness_right x7
  4. L68
    apply beta_prefix_extend_witness_witness_right
  5. L69
    exact hsplit_right
  6. L70
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro r
  5. 0005intro d
  6. 0006intro u
  7. 0007intro v
  8. 0008intro q
  9. 0009intro l
  10. 0010intro hprevious
  11. 0011intro hpoint
  12. 0012cases hpoint
  13. 0013cases hpoint_witness
  14. 0014cases hpoint_witness_witness
  15. 0015cases hpoint_witness_witness_witness
  16. 0016cases hpoint_witness_witness_witness_right
  17. 0017specialize beta_prefix_extend l
  18. 0018specialize beta_prefix_extend u
  19. 0019specialize beta_prefix_extend v
  20. 0020specialize beta_prefix_extend x2
  21. 0021cases beta_prefix_extend
  22. 0022cases beta_prefix_extend_witness
  23. 0023cases beta_prefix_extend_witness_witness
  24. 0024exists x3
  25. 0025exists x4
  26. 0026intro k
  27. 0027intro hk
  28. 0028have hsplit : k = l \/ exists gap. gap + S k = l
  29. 0029specialize finite_lt_succ_eq_or_lt l
  30. 0030specialize finite_lt_succ_eq_or_lt k
  31. 0031apply finite_lt_succ_eq_or_lt
  32. 0032exact hk
  33. 0033cases hsplit
  34. 0034exists x
  35. 0035exists x1
  36. 0036exists x2
  37. 0037split
  38. 0038rewrite hsplit_left
  39. 0039exact hpoint_witness_witness_witness_left
  40. 0040split
  41. 0041exact hpoint_witness_witness_witness_right_left
  42. 0042split
  43. 0043exact hpoint_witness_witness_witness_right_right
  44. 0044rewrite hsplit_left
  45. 0045rewrite hsplit_left
  46. 0046exact beta_prefix_extend_witness_witness_left
  47. 0047have hold : exists i j z. (k = q * i + j /\ ((exists ff_gap_mdm_lt_extend_old_column. ff_gap_mdm_lt_extend_old_column + S (j) = (q)) /\ ((exists ff_row_mdm_cell_extend_old_cell ff_column_mdm_cell_extend_old_cell. (((((exists ff_gap_mdm_lt_extend_old_cell_row_before. ff_gap_mdm_lt_extend_old_cell_row_before + S (i) = (r)) /\ ff_row_mdm_cell_extend_old_cell = i) \/ ((exists ff_gap_mdm_le_extend_old_cell_row_after. ff_gap_mdm_le_extend_old_cell_row_after + (r) = (i)) /\ ff_row_mdm_cell_extend_old_cell = S i))) /\ (((((exists ff_gap_mdm_lt_extend_old_cell_column_before. ff_gap_mdm_lt_extend_old_cell_column_before + S (j) = (d)) /\ ff_column_mdm_cell_extend_old_cell = j) \/ ((exists ff_gap_mdm_le_extend_old_cell_column_after. ff_gap_mdm_le_extend_old_cell_column_after + (d) = (j)) /\ ff_column_mdm_cell_extend_old_cell = S j))) /\ (((exists ff_h_mdm_extend_old_cell_source. ff_h_mdm_extend_old_cell_source + S (z) = S ((S ((ff_row_mdm_cell_extend_old_cell) * (w) + (ff_column_mdm_cell_extend_old_cell))) * c)) /\ exists ff_q_mdm_extend_old_cell_source. b = ff_q_mdm_extend_old_cell_source * S ((S ((ff_row_mdm_cell_extend_old_cell) * (w) + (ff_column_mdm_cell_extend_old_cell))) * c) + (z)))))) /\ (((exists ff_h_mdm_extend_old_output. ff_h_mdm_extend_old_output + S (z) = S ((S (k)) * v)) /\ exists ff_q_mdm_extend_old_output. u = ff_q_mdm_extend_old_output * S ((S (k)) * v) + (z))))))
  48. 0048specialize hprevious k
  49. 0049apply hprevious
  50. 0050exact hsplit_right
  51. 0051cases hold
  52. 0052cases hold_witness
  53. 0053cases hold_witness_witness
  54. 0054cases hold_witness_witness_witness
  55. 0055cases hold_witness_witness_witness_right
  56. 0056cases hold_witness_witness_witness_right_right
  57. 0057exists x5
  58. 0058exists x6
  59. 0059exists x7
  60. 0060split
  61. 0061exact hold_witness_witness_witness_left
  62. 0062split
  63. 0063exact hold_witness_witness_witness_right_left
  64. 0064split
  65. 0065exact hold_witness_witness_witness_right_right_left
  66. 0066specialize beta_prefix_extend_witness_witness_right k
  67. 0067specialize beta_prefix_extend_witness_witness_right x7
  68. 0068apply beta_prefix_extend_witness_witness_right
  69. 0069exact hsplit_right
  70. 0070exact hold_witness_witness_witness_right_right_right