DL008E

matrix_integer_minor_cell_balance

All four actual cofactor component cells satisfy the parent signed-integer equality at one genuinely shared in-range source position.

Alpha v34 checked-use · first admitted v27 · 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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ q. ∀ j. ∀ r. ∀ s. ∀ a. ∀ b. ∀ c. ∀ d. IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,S q,S q) → Lt(r,q) → Lt(s,q) → MatrixMinorCell(ab,ac,S q,0,j,r,s,a) → MatrixMinorCell(bb,bc,S q,0,j,r,s,b) → MatrixMinorCell(eb,ec,S q,0,j,r,s,c) → MatrixMinorCell(fb,fc,S q,0,j,r,s,d) → a + d = c + b

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

Definition DAG

MatrixMinorCell(b,c,w,r,d,i,j,z) · 4IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,r,w) · 1Lt(a,b) · 4

Actual proof prerequisites

matrix_skip_index_bounded · checked external prerequisitematrix_recursive_flattened_index_boundmatrix_integer_minor_cell_at_source
Original expanded first-order statement 
forall ab ac bb bc eb ec fb fc q j r s a b c d. (forall ics_index_minor_parent_equal ics_value0_minor_parent_equal ics_value1_minor_parent_equal ics_value2_minor_parent_equal ics_value3_minor_parent_equal. (exists ics_gap_minor_parent_equal_bound. ics_gap_minor_parent_equal_bound + S (ics_index_minor_parent_equal) = ((S q) * (S q))) -> (((exists fs_h_ics_minor_parent_equal_at0. fs_h_ics_minor_parent_equal_at0 + S (ics_value0_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * ac)) /\ exists fs_q_ics_minor_parent_equal_at0. ab = fs_q_ics_minor_parent_equal_at0 * S ((S (ics_index_minor_parent_equal)) * ac) + (ics_value0_minor_parent_equal))) -> (((exists fs_h_ics_minor_parent_equal_at1. fs_h_ics_minor_parent_equal_at1 + S (ics_value1_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * bc)) /\ exists fs_q_ics_minor_parent_equal_at1. bb = fs_q_ics_minor_parent_equal_at1 * S ((S (ics_index_minor_parent_equal)) * bc) + (ics_value1_minor_parent_equal))) -> (((exists fs_h_ics_minor_parent_equal_at2. fs_h_ics_minor_parent_equal_at2 + S (ics_value2_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * ec)) /\ exists fs_q_ics_minor_parent_equal_at2. eb = fs_q_ics_minor_parent_equal_at2 * S ((S (ics_index_minor_parent_equal)) * ec) + (ics_value2_minor_parent_equal))) -> (((exists fs_h_ics_minor_parent_equal_at3. fs_h_ics_minor_parent_equal_at3 + S (ics_value3_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * fc)) /\ exists fs_q_ics_minor_parent_equal_at3. fb = fs_q_ics_minor_parent_equal_at3 * S ((S (ics_index_minor_parent_equal)) * fc) + (ics_value3_minor_parent_equal))) -> ics_value0_minor_parent_equal + ics_value3_minor_parent_equal = ics_value2_minor_parent_equal + ics_value1_minor_parent_equal) -> (exists mdr_gap_minor_row_bound. mdr_gap_minor_row_bound + S (r) = (q)) -> (exists mdr_gap_minor_col_bound. mdr_gap_minor_col_bound + S (s) = (q)) -> (exists ff_row_mdm_cell_mdre_minor_cell_ap ff_column_mdm_cell_mdre_minor_cell_ap. (((((exists ff_gap_mdm_lt_mdre_minor_cell_ap_row_before. ff_gap_mdm_lt_mdre_minor_cell_ap_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_ap = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_ap_row_after. ff_gap_mdm_le_mdre_minor_cell_ap_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_ap = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_ap_column_before. ff_gap_mdm_lt_mdre_minor_cell_ap_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_ap = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_ap_column_after. ff_gap_mdm_le_mdre_minor_cell_ap_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_ap = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_ap_source. ff_h_mdm_mdre_minor_cell_ap_source + S (a) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_ap) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_ap))) * ac)) /\ exists ff_q_mdm_mdre_minor_cell_ap_source. ab = ff_q_mdm_mdre_minor_cell_ap_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_ap) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_ap))) * ac) + (a)))))) -> (exists ff_row_mdm_cell_mdre_minor_cell_an ff_column_mdm_cell_mdre_minor_cell_an. (((((exists ff_gap_mdm_lt_mdre_minor_cell_an_row_before. ff_gap_mdm_lt_mdre_minor_cell_an_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_an = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_an_row_after. ff_gap_mdm_le_mdre_minor_cell_an_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_an = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_an_column_before. ff_gap_mdm_lt_mdre_minor_cell_an_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_an = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_an_column_after. ff_gap_mdm_le_mdre_minor_cell_an_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_an = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_an_source. ff_h_mdm_mdre_minor_cell_an_source + S (b) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_an) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_an))) * bc)) /\ exists ff_q_mdm_mdre_minor_cell_an_source. bb = ff_q_mdm_mdre_minor_cell_an_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_an) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_an))) * bc) + (b)))))) -> (exists ff_row_mdm_cell_mdre_minor_cell_bp ff_column_mdm_cell_mdre_minor_cell_bp. (((((exists ff_gap_mdm_lt_mdre_minor_cell_bp_row_before. ff_gap_mdm_lt_mdre_minor_cell_bp_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_bp = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bp_row_after. ff_gap_mdm_le_mdre_minor_cell_bp_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_bp = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_bp_column_before. ff_gap_mdm_lt_mdre_minor_cell_bp_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_bp = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bp_column_after. ff_gap_mdm_le_mdre_minor_cell_bp_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_bp = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_bp_source. ff_h_mdm_mdre_minor_cell_bp_source + S (c) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_bp) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bp))) * ec)) /\ exists ff_q_mdm_mdre_minor_cell_bp_source. eb = ff_q_mdm_mdre_minor_cell_bp_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_bp) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bp))) * ec) + (c)))))) -> (exists ff_row_mdm_cell_mdre_minor_cell_bn ff_column_mdm_cell_mdre_minor_cell_bn. (((((exists ff_gap_mdm_lt_mdre_minor_cell_bn_row_before. ff_gap_mdm_lt_mdre_minor_cell_bn_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_bn = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bn_row_after. ff_gap_mdm_le_mdre_minor_cell_bn_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_bn = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_bn_column_before. ff_gap_mdm_lt_mdre_minor_cell_bn_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_bn = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bn_column_after. ff_gap_mdm_le_mdre_minor_cell_bn_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_bn = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_bn_source. ff_h_mdm_mdre_minor_cell_bn_source + S (d) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_bn) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bn))) * fc)) /\ exists ff_q_mdm_mdre_minor_cell_bn_source. fb = ff_q_mdm_mdre_minor_cell_bn_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_bn) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bn))) * fc) + (d)))))) -> a + d = c + b

Complete tactic proof in conservative notation

All 95 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

95 script commands · 11 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 (2)
matrix recursive flattened index boundmatrix integer minor cell at source
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro bb
  4. L4
    intro bc
  5. L5
    intro eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro q
  10. L10
    intro j
02Fix variables and assumptionsL11–20

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

  1. L11
    intro r
  2. L12
    intro s
  3. L13
    intro a
  4. L14
    intro b
  5. L15
    intro c
  6. L16
    intro d
  7. L17
    intro hequal
  8. L18
    intro hr
  9. L19
    intro hs
  10. L20
    intro hap
03Fix variables and assumptionsL21–23

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

  1. L21
    intro han
  2. L22
    intro hbp
  3. L23
    intro hbn
04Separate the logical casesL24–27

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

  1. L24
    cases hap
  2. L25
    cases hap_witness
  3. L26
    cases hap_witness_witness
  4. L27
    cases hap_witness_witness_right
05Establish hrowL28–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix skip index bounded.

  1. L28
  2. L29
    specialize matrix_skip_index_bounded (r)
  3. L30
    specialize matrix_skip_index_bounded (0)
  4. L31
    specialize matrix_skip_index_bounded (x)
  5. L32
    specialize matrix_skip_index_bounded (q)
  6. L33
    apply matrix_skip_index_bounded
  7. L34
    exact hap_witness_witness_left
  8. L35
    exact hr
06Establish hcolumnL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix skip index bounded.

  1. L36
    have hcolumn : Lt(x1,S q)Definitions: Lt(x1,S q)Original native command in the exact edition
  2. L37
    specialize matrix_skip_index_bounded (s)
  3. L38
    specialize matrix_skip_index_bounded (j)
  4. L39
    specialize matrix_skip_index_bounded (x1)
  5. L40
    specialize matrix_skip_index_bounded (q)
  6. L41
    apply matrix_skip_index_bounded
  7. L42
    exact hap_witness_witness_right_left
  8. L43
    exact hs
  9. L44
    specialize hequal (x * (S q) + x1)
  10. L45
    specialize hequal (a)
07Use earlier factsL46–55

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

  1. L46
    specialize hequal (b)
  2. L47
    specialize hequal (c)
  3. L48
    specialize hequal (d)
  4. L49
    apply hequal
  5. L50
    specialize matrix_recursive_flattened_index_bound (S q)
  6. L51
    specialize matrix_recursive_flattened_index_bound (x)
  7. L52
    specialize matrix_recursive_flattened_index_bound (x1)
  8. L53
    apply matrix_recursive_flattened_index_bound
  9. L54
    exact hrow
  10. L55
    exact hcolumn
08Use earlier factsL56–65

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

  1. L56
    exact hap_witness_witness_right_right
  2. L57
    specialize matrix_integer_minor_cell_at_source (bb)
  3. L58
    specialize matrix_integer_minor_cell_at_source (bc)
  4. L59
    specialize matrix_integer_minor_cell_at_source (q)
  5. L60
    specialize matrix_integer_minor_cell_at_source (j)
  6. L61
    specialize matrix_integer_minor_cell_at_source (r)
  7. L62
    specialize matrix_integer_minor_cell_at_source (s)
  8. L63
    specialize matrix_integer_minor_cell_at_source (x)
  9. L64
    specialize matrix_integer_minor_cell_at_source (x1)
  10. L65
    specialize matrix_integer_minor_cell_at_source (b)
09Use earlier factsL66–75

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

  1. L66
    apply matrix_integer_minor_cell_at_source
  2. L67
    exact hap_witness_witness_left
  3. L68
    exact hap_witness_witness_right_left
  4. L69
    exact han
  5. L70
    specialize matrix_integer_minor_cell_at_source (eb)
  6. L71
    specialize matrix_integer_minor_cell_at_source (ec)
  7. L72
    specialize matrix_integer_minor_cell_at_source (q)
  8. L73
    specialize matrix_integer_minor_cell_at_source (j)
  9. L74
    specialize matrix_integer_minor_cell_at_source (r)
  10. L75
    specialize matrix_integer_minor_cell_at_source (s)
10Use earlier factsL76–85

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

  1. L76
    specialize matrix_integer_minor_cell_at_source (x)
  2. L77
    specialize matrix_integer_minor_cell_at_source (x1)
  3. L78
    specialize matrix_integer_minor_cell_at_source (c)
  4. L79
    apply matrix_integer_minor_cell_at_source
  5. L80
    exact hap_witness_witness_left
  6. L81
    exact hap_witness_witness_right_left
  7. L82
    exact hbp
  8. L83
    specialize matrix_integer_minor_cell_at_source (fb)
  9. L84
    specialize matrix_integer_minor_cell_at_source (fc)
  10. L85
    specialize matrix_integer_minor_cell_at_source (q)
11Use earlier factsL86–95

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

  1. L86
    specialize matrix_integer_minor_cell_at_source (j)
  2. L87
    specialize matrix_integer_minor_cell_at_source (r)
  3. L88
    specialize matrix_integer_minor_cell_at_source (s)
  4. L89
    specialize matrix_integer_minor_cell_at_source (x)
  5. L90
    specialize matrix_integer_minor_cell_at_source (x1)
  6. L91
    specialize matrix_integer_minor_cell_at_source (d)
  7. L92
    apply matrix_integer_minor_cell_at_source
  8. L93
    exact hap_witness_witness_left
  9. L94
    exact hap_witness_witness_right_left
  10. L95
    exact hbn

Library-wide reading audit

Original defined command ledger · 95 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro q
  10. 0010intro j
  11. 0011intro r
  12. 0012intro s
  13. 0013intro a
  14. 0014intro b
  15. 0015intro c
  16. 0016intro d
  17. 0017intro hequal
  18. 0018intro hr
  19. 0019intro hs
  20. 0020intro hap
  21. 0021intro han
  22. 0022intro hbp
  23. 0023intro hbn
  24. 0024cases hap
  25. 0025cases hap_witness
  26. 0026cases hap_witness_witness
  27. 0027cases hap_witness_witness_right
  28. 0028have hrow : Lt(x,S q)
  29. 0029specialize matrix_skip_index_bounded (r)
  30. 0030specialize matrix_skip_index_bounded (0)
  31. 0031specialize matrix_skip_index_bounded (x)
  32. 0032specialize matrix_skip_index_bounded (q)
  33. 0033apply matrix_skip_index_bounded
  34. 0034exact hap_witness_witness_left
  35. 0035exact hr
  36. 0036have hcolumn : Lt(x1,S q)
  37. 0037specialize matrix_skip_index_bounded (s)
  38. 0038specialize matrix_skip_index_bounded (j)
  39. 0039specialize matrix_skip_index_bounded (x1)
  40. 0040specialize matrix_skip_index_bounded (q)
  41. 0041apply matrix_skip_index_bounded
  42. 0042exact hap_witness_witness_right_left
  43. 0043exact hs
  44. 0044specialize hequal (x * (S q) + x1)
  45. 0045specialize hequal (a)
  46. 0046specialize hequal (b)
  47. 0047specialize hequal (c)
  48. 0048specialize hequal (d)
  49. 0049apply hequal
  50. 0050specialize matrix_recursive_flattened_index_bound (S q)
  51. 0051specialize matrix_recursive_flattened_index_bound (x)
  52. 0052specialize matrix_recursive_flattened_index_bound (x1)
  53. 0053apply matrix_recursive_flattened_index_bound
  54. 0054exact hrow
  55. 0055exact hcolumn
  56. 0056exact hap_witness_witness_right_right
  57. 0057specialize matrix_integer_minor_cell_at_source (bb)
  58. 0058specialize matrix_integer_minor_cell_at_source (bc)
  59. 0059specialize matrix_integer_minor_cell_at_source (q)
  60. 0060specialize matrix_integer_minor_cell_at_source (j)
  61. 0061specialize matrix_integer_minor_cell_at_source (r)
  62. 0062specialize matrix_integer_minor_cell_at_source (s)
  63. 0063specialize matrix_integer_minor_cell_at_source (x)
  64. 0064specialize matrix_integer_minor_cell_at_source (x1)
  65. 0065specialize matrix_integer_minor_cell_at_source (b)
  66. 0066apply matrix_integer_minor_cell_at_source
  67. 0067exact hap_witness_witness_left
  68. 0068exact hap_witness_witness_right_left
  69. 0069exact han
  70. 0070specialize matrix_integer_minor_cell_at_source (eb)
  71. 0071specialize matrix_integer_minor_cell_at_source (ec)
  72. 0072specialize matrix_integer_minor_cell_at_source (q)
  73. 0073specialize matrix_integer_minor_cell_at_source (j)
  74. 0074specialize matrix_integer_minor_cell_at_source (r)
  75. 0075specialize matrix_integer_minor_cell_at_source (s)
  76. 0076specialize matrix_integer_minor_cell_at_source (x)
  77. 0077specialize matrix_integer_minor_cell_at_source (x1)
  78. 0078specialize matrix_integer_minor_cell_at_source (c)
  79. 0079apply matrix_integer_minor_cell_at_source
  80. 0080exact hap_witness_witness_left
  81. 0081exact hap_witness_witness_right_left
  82. 0082exact hbp
  83. 0083specialize matrix_integer_minor_cell_at_source (fb)
  84. 0084specialize matrix_integer_minor_cell_at_source (fc)
  85. 0085specialize matrix_integer_minor_cell_at_source (q)
  86. 0086specialize matrix_integer_minor_cell_at_source (j)
  87. 0087specialize matrix_integer_minor_cell_at_source (r)
  88. 0088specialize matrix_integer_minor_cell_at_source (s)
  89. 0089specialize matrix_integer_minor_cell_at_source (x)
  90. 0090specialize matrix_integer_minor_cell_at_source (x1)
  91. 0091specialize matrix_integer_minor_cell_at_source (d)
  92. 0092apply matrix_integer_minor_cell_at_source
  93. 0093exact hap_witness_witness_left
  94. 0094exact hap_witness_witness_right_left
  95. 0095exact hbn