DL001E

matrix_recursive_minor_prefix_functional

Two complete codes of the same actual cofactor minor agree at every in-range child entry; division uniqueness aligns the genuine row/column witnesses.

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

∀ b. ∀ c. ∀ q. ∀ j. ∀ u. ∀ v. ∀ U. ∀ V. MatrixMinorPrefix(b,c,S q,0,j,u,v,q,q · q) → MatrixMinorPrefix(b,c,S q,0,j,U,V,q,q · q) → ∀ x. ∀ y. Lt(x,q · q) → BetaAt(u,v,x,y) → BetaAt(U,V,x,y)

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

Definition DAG

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

Actual proof prerequisites

division_remainder_unique · checked external prerequisitebeta_at_unique · checked external prerequisitebeta_matrix_minor_cell_functional · checked external prerequisite
Original expanded first-order statement 
forall b c q j u v U V. (forall ff_index_mdm_prefix_mdre_first_minor. (exists ff_gap_mdm_lt_mdre_first_minor_index_bound. ff_gap_mdm_lt_mdre_first_minor_index_bound + S (ff_index_mdm_prefix_mdre_first_minor) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdre_first_minor ff_column_mdm_prefix_mdre_first_minor ff_value_mdm_prefix_mdre_first_minor. (ff_index_mdm_prefix_mdre_first_minor = (q) * ff_row_mdm_prefix_mdre_first_minor + ff_column_mdm_prefix_mdre_first_minor /\ ((exists ff_gap_mdm_lt_mdre_first_minor_column_bound. ff_gap_mdm_lt_mdre_first_minor_column_bound + S (ff_column_mdm_prefix_mdre_first_minor) = (q)) /\ ((exists ff_row_mdm_cell_mdre_first_minor_cell ff_column_mdm_cell_mdre_first_minor_cell. (((((exists ff_gap_mdm_lt_mdre_first_minor_cell_row_before. ff_gap_mdm_lt_mdre_first_minor_cell_row_before + S (ff_row_mdm_prefix_mdre_first_minor) = (0)) /\ ff_row_mdm_cell_mdre_first_minor_cell = ff_row_mdm_prefix_mdre_first_minor) \/ ((exists ff_gap_mdm_le_mdre_first_minor_cell_row_after. ff_gap_mdm_le_mdre_first_minor_cell_row_after + (0) = (ff_row_mdm_prefix_mdre_first_minor)) /\ ff_row_mdm_cell_mdre_first_minor_cell = S ff_row_mdm_prefix_mdre_first_minor))) /\ (((((exists ff_gap_mdm_lt_mdre_first_minor_cell_column_before. ff_gap_mdm_lt_mdre_first_minor_cell_column_before + S (ff_column_mdm_prefix_mdre_first_minor) = (j)) /\ ff_column_mdm_cell_mdre_first_minor_cell = ff_column_mdm_prefix_mdre_first_minor) \/ ((exists ff_gap_mdm_le_mdre_first_minor_cell_column_after. ff_gap_mdm_le_mdre_first_minor_cell_column_after + (j) = (ff_column_mdm_prefix_mdre_first_minor)) /\ ff_column_mdm_cell_mdre_first_minor_cell = S ff_column_mdm_prefix_mdre_first_minor))) /\ (((exists ff_h_mdm_mdre_first_minor_cell_source. ff_h_mdm_mdre_first_minor_cell_source + S (ff_value_mdm_prefix_mdre_first_minor) = S ((S ((ff_row_mdm_cell_mdre_first_minor_cell) * (S (q)) + (ff_column_mdm_cell_mdre_first_minor_cell))) * c)) /\ exists ff_q_mdm_mdre_first_minor_cell_source. b = ff_q_mdm_mdre_first_minor_cell_source * S ((S ((ff_row_mdm_cell_mdre_first_minor_cell) * (S (q)) + (ff_column_mdm_cell_mdre_first_minor_cell))) * c) + (ff_value_mdm_prefix_mdre_first_minor)))))) /\ (((exists ff_h_mdm_mdre_first_minor_target. ff_h_mdm_mdre_first_minor_target + S (ff_value_mdm_prefix_mdre_first_minor) = S ((S (ff_index_mdm_prefix_mdre_first_minor)) * v)) /\ exists ff_q_mdm_mdre_first_minor_target. u = ff_q_mdm_mdre_first_minor_target * S ((S (ff_index_mdm_prefix_mdre_first_minor)) * v) + (ff_value_mdm_prefix_mdre_first_minor))))))) -> (forall ff_index_mdm_prefix_mdre_second_minor. (exists ff_gap_mdm_lt_mdre_second_minor_index_bound. ff_gap_mdm_lt_mdre_second_minor_index_bound + S (ff_index_mdm_prefix_mdre_second_minor) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdre_second_minor ff_column_mdm_prefix_mdre_second_minor ff_value_mdm_prefix_mdre_second_minor. (ff_index_mdm_prefix_mdre_second_minor = (q) * ff_row_mdm_prefix_mdre_second_minor + ff_column_mdm_prefix_mdre_second_minor /\ ((exists ff_gap_mdm_lt_mdre_second_minor_column_bound. ff_gap_mdm_lt_mdre_second_minor_column_bound + S (ff_column_mdm_prefix_mdre_second_minor) = (q)) /\ ((exists ff_row_mdm_cell_mdre_second_minor_cell ff_column_mdm_cell_mdre_second_minor_cell. (((((exists ff_gap_mdm_lt_mdre_second_minor_cell_row_before. ff_gap_mdm_lt_mdre_second_minor_cell_row_before + S (ff_row_mdm_prefix_mdre_second_minor) = (0)) /\ ff_row_mdm_cell_mdre_second_minor_cell = ff_row_mdm_prefix_mdre_second_minor) \/ ((exists ff_gap_mdm_le_mdre_second_minor_cell_row_after. ff_gap_mdm_le_mdre_second_minor_cell_row_after + (0) = (ff_row_mdm_prefix_mdre_second_minor)) /\ ff_row_mdm_cell_mdre_second_minor_cell = S ff_row_mdm_prefix_mdre_second_minor))) /\ (((((exists ff_gap_mdm_lt_mdre_second_minor_cell_column_before. ff_gap_mdm_lt_mdre_second_minor_cell_column_before + S (ff_column_mdm_prefix_mdre_second_minor) = (j)) /\ ff_column_mdm_cell_mdre_second_minor_cell = ff_column_mdm_prefix_mdre_second_minor) \/ ((exists ff_gap_mdm_le_mdre_second_minor_cell_column_after. ff_gap_mdm_le_mdre_second_minor_cell_column_after + (j) = (ff_column_mdm_prefix_mdre_second_minor)) /\ ff_column_mdm_cell_mdre_second_minor_cell = S ff_column_mdm_prefix_mdre_second_minor))) /\ (((exists ff_h_mdm_mdre_second_minor_cell_source. ff_h_mdm_mdre_second_minor_cell_source + S (ff_value_mdm_prefix_mdre_second_minor) = S ((S ((ff_row_mdm_cell_mdre_second_minor_cell) * (S (q)) + (ff_column_mdm_cell_mdre_second_minor_cell))) * c)) /\ exists ff_q_mdm_mdre_second_minor_cell_source. b = ff_q_mdm_mdre_second_minor_cell_source * S ((S ((ff_row_mdm_cell_mdre_second_minor_cell) * (S (q)) + (ff_column_mdm_cell_mdre_second_minor_cell))) * c) + (ff_value_mdm_prefix_mdre_second_minor)))))) /\ (((exists ff_h_mdm_mdre_second_minor_target. ff_h_mdm_mdre_second_minor_target + S (ff_value_mdm_prefix_mdre_second_minor) = S ((S (ff_index_mdm_prefix_mdre_second_minor)) * V)) /\ exists ff_q_mdm_mdre_second_minor_target. U = ff_q_mdm_mdre_second_minor_target * S ((S (ff_index_mdm_prefix_mdre_second_minor)) * V) + (ff_value_mdm_prefix_mdre_second_minor))))))) -> (forall mdr_i_minor_unique mdr_a_minor_unique. (exists mdr_gap_minor_uniqueb. mdr_gap_minor_uniqueb + S (mdr_i_minor_unique) = (q * q)) -> (((exists ff_h_mdr_minor_uniqueo. ff_h_mdr_minor_uniqueo + S (mdr_a_minor_unique) = S ((S (mdr_i_minor_unique)) * v)) /\ exists ff_q_mdr_minor_uniqueo. u = ff_q_mdr_minor_uniqueo * S ((S (mdr_i_minor_unique)) * v) + (mdr_a_minor_unique))) -> (((exists ff_h_mdr_minor_uniquen. ff_h_mdr_minor_uniquen + S (mdr_a_minor_unique) = S ((S (mdr_i_minor_unique)) * V)) /\ exists ff_q_mdr_minor_uniquen. U = ff_q_mdr_minor_uniquen * S ((S (mdr_i_minor_unique)) * V) + (mdr_a_minor_unique))))

Complete tactic proof in conservative notation

All 82 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

82 script commands · 17 reading checkpoints · 5 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.

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 q
  4. L4
    intro j
  5. L5
    intro u
  6. L6
    intro v
  7. L7
    intro U
  8. L8
    intro V
  9. L9
    intro hleft
  10. L10
    intro hright
02Fix variables and assumptionsL11–14

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

  1. L11
    intro k
  2. L12
    intro a
  3. L13
    intro hk
  4. L14
    intro ha
03Establish hfirstL15–18

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

  1. L15
    have hfirst : ∃ r. ∃ s. ∃ z. k = q · r + s ∧ (Lt(s,q) ∧ (MatrixMinorCell(b,c,S q,0,j,r,s,z) ∧ BetaAt(u,v,k,z)))Definitions: Lt(s,q)MatrixMinorCell(b,c,S q,0,j,r,s,z)BetaAt(u,v,k,z)Original native command in the exact edition
  2. L16
    specialize hleft (k)
  3. L17
    apply hleft
  4. L18
    exact hk
04Separate the logical casesL19–24

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

  1. L19
    cases hfirst
  2. L20
    cases hfirst_witness
  3. L21
    cases hfirst_witness_witness
  4. L22
    cases hfirst_witness_witness_witness
  5. L23
    cases hfirst_witness_witness_witness_right
  6. L24
    cases hfirst_witness_witness_witness_right_right
05Establish hsecondL25–28

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

  1. L25
    have hsecond : ∃ r. ∃ s. ∃ z. k = q · r + s ∧ (Lt(s,q) ∧ (MatrixMinorCell(b,c,S q,0,j,r,s,z) ∧ BetaAt(U,V,k,z)))Definitions: Lt(s,q)MatrixMinorCell(b,c,S q,0,j,r,s,z)BetaAt(U,V,k,z)Original native command in the exact edition
  2. L26
    specialize hright (k)
  3. L27
    apply hright
  4. L28
    exact hk
06Separate the logical casesL29–34

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

  1. L29
    cases hsecond
  2. L30
    cases hsecond_witness
  3. L31
    cases hsecond_witness_witness
  4. L32
    cases hsecond_witness_witness_witness
  5. L33
    cases hsecond_witness_witness_witness_right
  6. L34
    cases hsecond_witness_witness_witness_right_right
07Establish hcoordinatesL35–44

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

  1. L35
    have hcoordinates : x = x3 /\ x1 = x4
  2. L36
    specialize division_remainder_unique (q)
  3. L37
    specialize division_remainder_unique (k)
  4. L38
    specialize division_remainder_unique (x)
  5. L39
    specialize division_remainder_unique (x1)
  6. L40
    specialize division_remainder_unique (x3)
  7. L41
    specialize division_remainder_unique (x4)
  8. L42
    apply division_remainder_unique
  9. L43
    exact hfirst_witness_witness_witness_left
  10. L44
    exact hfirst_witness_witness_witness_right_left
08Use earlier factsL45–46

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

  1. L45
    exact hsecond_witness_witness_witness_left
  2. L46
    exact hsecond_witness_witness_witness_right_left
09Separate the logical casesL47–47

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

  1. L47
    cases hcoordinates
10Establish hvaluesL48–57

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

  1. L48
    have hvalues : x2 = x5
  2. L49
    specialize beta_matrix_minor_cell_functional (b)
  3. L50
    specialize beta_matrix_minor_cell_functional (c)
  4. L51
    specialize beta_matrix_minor_cell_functional (S q)
  5. L52
    specialize beta_matrix_minor_cell_functional (0)
  6. L53
    specialize beta_matrix_minor_cell_functional (j)
  7. L54
    specialize beta_matrix_minor_cell_functional (x)
  8. L55
    specialize beta_matrix_minor_cell_functional (x1)
  9. L56
    specialize beta_matrix_minor_cell_functional (x2)
  10. L57
    specialize beta_matrix_minor_cell_functional (x5)
11Use earlier factsL58–59

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

  1. L58
    apply beta_matrix_minor_cell_functional
  2. L59
    exact hfirst_witness_witness_witness_right_right_left
12Calculate and transport equalitiesL60–67

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

  1. L60
    rewrite hcoordinates_left
  2. L61
    rewrite hcoordinates_left
  3. L62
    rewrite hcoordinates_left
  4. L63
    rewrite hcoordinates_left
  5. L64
    rewrite hcoordinates_right
  6. L65
    rewrite hcoordinates_right
  7. L66
    rewrite hcoordinates_right
  8. L67
    rewrite hcoordinates_right
13Use earlier factsL68–68

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

  1. L68
    exact hsecond_witness_witness_witness_right_right_left
14Establish houtputL69–78

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

  1. L69
    have houtput : a = x5
  2. L70
    trans x2
  3. L71
    specialize beta_at_unique (u)
  4. L72
    specialize beta_at_unique (v)
  5. L73
    specialize beta_at_unique (k)
  6. L74
    specialize beta_at_unique (a)
  7. L75
    specialize beta_at_unique (x2)
  8. L76
    apply beta_at_unique
  9. L77
    exact ha
  10. L78
    exact hfirst_witness_witness_witness_right_right_right
15Use earlier factsL79–79

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

  1. L79
    exact hvalues
16Calculate and transport equalitiesL80–81

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

  1. L80
    rewrite houtput
  2. L81
    rewrite houtput
17Use earlier factsL82–82

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

  1. L82
    exact hsecond_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro q
  4. 0004intro j
  5. 0005intro u
  6. 0006intro v
  7. 0007intro U
  8. 0008intro V
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011intro k
  12. 0012intro a
  13. 0013intro hk
  14. 0014intro ha
  15. 0015have hfirst : ∃ r. ∃ s. ∃ z. k = q · r + s ∧ (Lt(s,q) ∧ (MatrixMinorCell(b,c,S q,0,j,r,s,z) ∧ BetaAt(u,v,k,z)))
  16. 0016specialize hleft (k)
  17. 0017apply hleft
  18. 0018exact hk
  19. 0019cases hfirst
  20. 0020cases hfirst_witness
  21. 0021cases hfirst_witness_witness
  22. 0022cases hfirst_witness_witness_witness
  23. 0023cases hfirst_witness_witness_witness_right
  24. 0024cases hfirst_witness_witness_witness_right_right
  25. 0025have hsecond : ∃ r. ∃ s. ∃ z. k = q · r + s ∧ (Lt(s,q) ∧ (MatrixMinorCell(b,c,S q,0,j,r,s,z) ∧ BetaAt(U,V,k,z)))
  26. 0026specialize hright (k)
  27. 0027apply hright
  28. 0028exact hk
  29. 0029cases hsecond
  30. 0030cases hsecond_witness
  31. 0031cases hsecond_witness_witness
  32. 0032cases hsecond_witness_witness_witness
  33. 0033cases hsecond_witness_witness_witness_right
  34. 0034cases hsecond_witness_witness_witness_right_right
  35. 0035have hcoordinates : x = x3 /\ x1 = x4
  36. 0036specialize division_remainder_unique (q)
  37. 0037specialize division_remainder_unique (k)
  38. 0038specialize division_remainder_unique (x)
  39. 0039specialize division_remainder_unique (x1)
  40. 0040specialize division_remainder_unique (x3)
  41. 0041specialize division_remainder_unique (x4)
  42. 0042apply division_remainder_unique
  43. 0043exact hfirst_witness_witness_witness_left
  44. 0044exact hfirst_witness_witness_witness_right_left
  45. 0045exact hsecond_witness_witness_witness_left
  46. 0046exact hsecond_witness_witness_witness_right_left
  47. 0047cases hcoordinates
  48. 0048have hvalues : x2 = x5
  49. 0049specialize beta_matrix_minor_cell_functional (b)
  50. 0050specialize beta_matrix_minor_cell_functional (c)
  51. 0051specialize beta_matrix_minor_cell_functional (S q)
  52. 0052specialize beta_matrix_minor_cell_functional (0)
  53. 0053specialize beta_matrix_minor_cell_functional (j)
  54. 0054specialize beta_matrix_minor_cell_functional (x)
  55. 0055specialize beta_matrix_minor_cell_functional (x1)
  56. 0056specialize beta_matrix_minor_cell_functional (x2)
  57. 0057specialize beta_matrix_minor_cell_functional (x5)
  58. 0058apply beta_matrix_minor_cell_functional
  59. 0059exact hfirst_witness_witness_witness_right_right_left
  60. 0060rewrite hcoordinates_left
  61. 0061rewrite hcoordinates_left
  62. 0062rewrite hcoordinates_left
  63. 0063rewrite hcoordinates_left
  64. 0064rewrite hcoordinates_right
  65. 0065rewrite hcoordinates_right
  66. 0066rewrite hcoordinates_right
  67. 0067rewrite hcoordinates_right
  68. 0068exact hsecond_witness_witness_witness_right_right_left
  69. 0069have houtput : a = x5
  70. 0070trans x2
  71. 0071specialize beta_at_unique (u)
  72. 0072specialize beta_at_unique (v)
  73. 0073specialize beta_at_unique (k)
  74. 0074specialize beta_at_unique (a)
  75. 0075specialize beta_at_unique (x2)
  76. 0076apply beta_at_unique
  77. 0077exact ha
  78. 0078exact hfirst_witness_witness_witness_right_right_right
  79. 0079exact hvalues
  80. 0080rewrite houtput
  81. 0081rewrite houtput
  82. 0082exact hsecond_witness_witness_witness_right_right_right