DL0014

matrix_recursive_node_code_injective

The conservatively shared record determines all seven actual matrix/dimension/value fields uniquely, by six independently checked pairing injections.

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

∀ z. ∀ d. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ p. ∀ n. ∀ e. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ r. ∀ s. SignedDeterminantNodeCode(z,d,pb,pc,nb,nc,p,n) → SignedDeterminantNodeCode(z,e,ab,ac,bb,bc,r,s) → d = e ∧ (pb = ab ∧ (pc = ac ∧ (nb = bb ∧ (nc = bc ∧ (p = r ∧ n = s)))))

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

Definition DAG

SignedDeterminantNodeCode(z,d,pb,pc,nb,nc,p,n) · 2

Actual proof prerequisites

pair_code_injective · checked external prerequisite
Original expanded first-order statement 
forall z d pb pc nb nc p n e ab ac bb bc r s. (exists mdr_a_code_first mdr_b_code_first mdr_c_code_first mdr_e_code_first mdr_f_code_first. ((mdr_a_code_first = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_code_first = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_code_first = ((mdr_a_code_first) + (mdr_b_code_first)) * S ((mdr_a_code_first) + (mdr_b_code_first)) + ((mdr_b_code_first) + (mdr_b_code_first))) /\ ((mdr_e_code_first = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_code_first = ((nc) + (mdr_e_code_first)) * S ((nc) + (mdr_e_code_first)) + ((mdr_e_code_first) + (mdr_e_code_first))) /\ ((z) = ((mdr_c_code_first) + (mdr_f_code_first)) * S ((mdr_c_code_first) + (mdr_f_code_first)) + ((mdr_f_code_first) + (mdr_f_code_first))))))))) -> (exists mdr_a_code_second mdr_b_code_second mdr_c_code_second mdr_e_code_second mdr_f_code_second. ((mdr_a_code_second = ((e) + (ab)) * S ((e) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_code_second = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_code_second = ((mdr_a_code_second) + (mdr_b_code_second)) * S ((mdr_a_code_second) + (mdr_b_code_second)) + ((mdr_b_code_second) + (mdr_b_code_second))) /\ ((mdr_e_code_second = ((r) + (s)) * S ((r) + (s)) + ((s) + (s))) /\ ((mdr_f_code_second = ((bc) + (mdr_e_code_second)) * S ((bc) + (mdr_e_code_second)) + ((mdr_e_code_second) + (mdr_e_code_second))) /\ ((z) = ((mdr_c_code_second) + (mdr_f_code_second)) * S ((mdr_c_code_second) + (mdr_f_code_second)) + ((mdr_f_code_second) + (mdr_f_code_second))))))))) -> ((d = e) /\ ((pb = ab) /\ ((pc = ac) /\ ((nb = bb) /\ ((nc = bc) /\ ((p = r) /\ (n = s)))))))

Complete tactic proof in conservative notation

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

120 script commands · 32 reading checkpoints · 6 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 z
  2. L2
    intro d
  3. L3
    intro pb
  4. L4
    intro pc
  5. L5
    intro nb
  6. L6
    intro nc
  7. L7
    intro p
  8. L8
    intro n
  9. L9
    intro e
  10. L10
    intro ab
02Fix variables and assumptionsL11–17

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

  1. L11
    intro ac
  2. L12
    intro bb
  3. L13
    intro bc
  4. L14
    intro r
  5. L15
    intro s
  6. L16
    intro hfirst
  7. L17
    intro hsecond
03Separate the logical casesL18–27

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

  1. L18
    cases hfirst
  2. L19
    cases hfirst_witness
  3. L20
    cases hfirst_witness_witness
  4. L21
    cases hfirst_witness_witness_witness
  5. L22
    cases hfirst_witness_witness_witness_witness
  6. L23
    cases hfirst_witness_witness_witness_witness_witness
  7. L24
    cases hfirst_witness_witness_witness_witness_witness_right
  8. L25
    cases hfirst_witness_witness_witness_witness_witness_right_right
  9. L26
    cases hfirst_witness_witness_witness_witness_witness_right_right_right
  10. L27
    cases hfirst_witness_witness_witness_witness_witness_right_right_right_right
04Separate the logical casesL28–37

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

  1. L28
    cases hsecond
  2. L29
    cases hsecond_witness
  3. L30
    cases hsecond_witness_witness
  4. L31
    cases hsecond_witness_witness_witness
  5. L32
    cases hsecond_witness_witness_witness_witness
  6. L33
    cases hsecond_witness_witness_witness_witness_witness
  7. L34
    cases hsecond_witness_witness_witness_witness_witness_right
  8. L35
    cases hsecond_witness_witness_witness_witness_witness_right_right
  9. L36
    cases hsecond_witness_witness_witness_witness_witness_right_right_right
  10. L37
    cases hsecond_witness_witness_witness_witness_witness_right_right_right_right
05Establish hrootL38–46

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

  1. L38
    have hroot : x2 = x7 /\ x4 = x9
  2. L39
    specialize pair_code_injective (z)
  3. L40
    specialize pair_code_injective (x2)
  4. L41
    specialize pair_code_injective (x4)
  5. L42
    specialize pair_code_injective (x7)
  6. L43
    specialize pair_code_injective (x9)
  7. L44
    apply pair_code_injective
  8. L45
    exact hfirst_witness_witness_witness_witness_witness_right_right_right_right_right
  9. L46
    exact hsecond_witness_witness_witness_witness_witness_right_right_right_right_right
06Separate the logical casesL47–47

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

  1. L47
    cases hroot
07Establish hleftL48–57

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

  1. L48
    have hleft : x = x5 /\ x1 = x6
  2. L49
    specialize pair_code_injective (x2)
  3. L50
    specialize pair_code_injective (x)
  4. L51
    specialize pair_code_injective (x1)
  5. L52
    specialize pair_code_injective (x5)
  6. L53
    specialize pair_code_injective (x6)
  7. L54
    apply pair_code_injective
  8. L55
    exact hfirst_witness_witness_witness_witness_witness_right_right_left
  9. L56
    trans x7
  10. L57
    exact hroot_left
08Use earlier factsL58–58

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

  1. L58
    exact hsecond_witness_witness_witness_witness_witness_right_right_left
09Separate the logical casesL59–59

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

  1. L59
    cases hleft
10Establish hfirsttwoL60–69

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

  1. L60
    have hfirsttwo : d = e /\ pb = ab
  2. L61
    specialize pair_code_injective (x)
  3. L62
    specialize pair_code_injective (d)
  4. L63
    specialize pair_code_injective (pb)
  5. L64
    specialize pair_code_injective (e)
  6. L65
    specialize pair_code_injective (ab)
  7. L66
    apply pair_code_injective
  8. L67
    exact hfirst_witness_witness_witness_witness_witness_left
  9. L68
    trans x5
  10. L69
    exact hleft_left
11Use earlier factsL70–70

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

  1. L70
    exact hsecond_witness_witness_witness_witness_witness_left
12Separate the logical casesL71–71

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

  1. L71
    cases hfirsttwo
13Establish hnexttwoL72–81

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

  1. L72
    have hnexttwo : pc = ac /\ nb = bb
  2. L73
    specialize pair_code_injective (x1)
  3. L74
    specialize pair_code_injective (pc)
  4. L75
    specialize pair_code_injective (nb)
  5. L76
    specialize pair_code_injective (ac)
  6. L77
    specialize pair_code_injective (bb)
  7. L78
    apply pair_code_injective
  8. L79
    exact hfirst_witness_witness_witness_witness_witness_right_left
  9. L80
    trans x6
  10. L81
    exact hleft_right
14Use earlier factsL82–82

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

  1. L82
    exact hsecond_witness_witness_witness_witness_witness_right_left
15Separate the logical casesL83–83

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

  1. L83
    cases hnexttwo
16Establish hrightL84–93

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

  1. L84
    have hright : nc = bc /\ x3 = x8
  2. L85
    specialize pair_code_injective (x4)
  3. L86
    specialize pair_code_injective (nc)
  4. L87
    specialize pair_code_injective (x3)
  5. L88
    specialize pair_code_injective (bc)
  6. L89
    specialize pair_code_injective (x8)
  7. L90
    apply pair_code_injective
  8. L91
    exact hfirst_witness_witness_witness_witness_witness_right_right_right_right_left
  9. L92
    trans x9
  10. L93
    exact hroot_right
17Use earlier factsL94–94

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

  1. L94
    exact hsecond_witness_witness_witness_witness_witness_right_right_right_right_left
18Separate the logical casesL95–95

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

  1. L95
    cases hright
19Establish hvaluesL96–105

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

  1. L96
    have hvalues : p = r /\ n = s
  2. L97
    specialize pair_code_injective (x3)
  3. L98
    specialize pair_code_injective (p)
  4. L99
    specialize pair_code_injective (n)
  5. L100
    specialize pair_code_injective (r)
  6. L101
    specialize pair_code_injective (s)
  7. L102
    apply pair_code_injective
  8. L103
    exact hfirst_witness_witness_witness_witness_witness_right_right_right_left
  9. L104
    trans x8
  10. L105
    exact hright_right
20Use earlier factsL106–106

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

  1. L106
    exact hsecond_witness_witness_witness_witness_witness_right_right_right_left
21Separate the logical casesL107–108

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

  1. L107
    cases hvalues
  2. L108
    split
22Use earlier factsL109–109

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

  1. L109
    exact hfirsttwo_left
23Separate the logical casesL110–110

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

  1. L110
    split
24Use earlier factsL111–111

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

  1. L111
    exact hfirsttwo_right
25Separate the logical casesL112–112

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

  1. L112
    split
26Use earlier factsL113–113

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

  1. L113
    exact hnexttwo_left
27Separate the logical casesL114–114

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

  1. L114
    split
28Use earlier factsL115–115

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

  1. L115
    exact hnexttwo_right
29Separate the logical casesL116–116

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

  1. L116
    split
30Use earlier factsL117–117

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

  1. L117
    exact hright_left
31Separate the logical casesL118–118

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

  1. L118
    split
32Use earlier factsL119–120

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

  1. L119
    exact hvalues_left
  2. L120
    exact hvalues_right

Library-wide reading audit

Original defined command ledger · 120 lines
  1. 0001intro z
  2. 0002intro d
  3. 0003intro pb
  4. 0004intro pc
  5. 0005intro nb
  6. 0006intro nc
  7. 0007intro p
  8. 0008intro n
  9. 0009intro e
  10. 0010intro ab
  11. 0011intro ac
  12. 0012intro bb
  13. 0013intro bc
  14. 0014intro r
  15. 0015intro s
  16. 0016intro hfirst
  17. 0017intro hsecond
  18. 0018cases hfirst
  19. 0019cases hfirst_witness
  20. 0020cases hfirst_witness_witness
  21. 0021cases hfirst_witness_witness_witness
  22. 0022cases hfirst_witness_witness_witness_witness
  23. 0023cases hfirst_witness_witness_witness_witness_witness
  24. 0024cases hfirst_witness_witness_witness_witness_witness_right
  25. 0025cases hfirst_witness_witness_witness_witness_witness_right_right
  26. 0026cases hfirst_witness_witness_witness_witness_witness_right_right_right
  27. 0027cases hfirst_witness_witness_witness_witness_witness_right_right_right_right
  28. 0028cases hsecond
  29. 0029cases hsecond_witness
  30. 0030cases hsecond_witness_witness
  31. 0031cases hsecond_witness_witness_witness
  32. 0032cases hsecond_witness_witness_witness_witness
  33. 0033cases hsecond_witness_witness_witness_witness_witness
  34. 0034cases hsecond_witness_witness_witness_witness_witness_right
  35. 0035cases hsecond_witness_witness_witness_witness_witness_right_right
  36. 0036cases hsecond_witness_witness_witness_witness_witness_right_right_right
  37. 0037cases hsecond_witness_witness_witness_witness_witness_right_right_right_right
  38. 0038have hroot : x2 = x7 /\ x4 = x9
  39. 0039specialize pair_code_injective (z)
  40. 0040specialize pair_code_injective (x2)
  41. 0041specialize pair_code_injective (x4)
  42. 0042specialize pair_code_injective (x7)
  43. 0043specialize pair_code_injective (x9)
  44. 0044apply pair_code_injective
  45. 0045exact hfirst_witness_witness_witness_witness_witness_right_right_right_right_right
  46. 0046exact hsecond_witness_witness_witness_witness_witness_right_right_right_right_right
  47. 0047cases hroot
  48. 0048have hleft : x = x5 /\ x1 = x6
  49. 0049specialize pair_code_injective (x2)
  50. 0050specialize pair_code_injective (x)
  51. 0051specialize pair_code_injective (x1)
  52. 0052specialize pair_code_injective (x5)
  53. 0053specialize pair_code_injective (x6)
  54. 0054apply pair_code_injective
  55. 0055exact hfirst_witness_witness_witness_witness_witness_right_right_left
  56. 0056trans x7
  57. 0057exact hroot_left
  58. 0058exact hsecond_witness_witness_witness_witness_witness_right_right_left
  59. 0059cases hleft
  60. 0060have hfirsttwo : d = e /\ pb = ab
  61. 0061specialize pair_code_injective (x)
  62. 0062specialize pair_code_injective (d)
  63. 0063specialize pair_code_injective (pb)
  64. 0064specialize pair_code_injective (e)
  65. 0065specialize pair_code_injective (ab)
  66. 0066apply pair_code_injective
  67. 0067exact hfirst_witness_witness_witness_witness_witness_left
  68. 0068trans x5
  69. 0069exact hleft_left
  70. 0070exact hsecond_witness_witness_witness_witness_witness_left
  71. 0071cases hfirsttwo
  72. 0072have hnexttwo : pc = ac /\ nb = bb
  73. 0073specialize pair_code_injective (x1)
  74. 0074specialize pair_code_injective (pc)
  75. 0075specialize pair_code_injective (nb)
  76. 0076specialize pair_code_injective (ac)
  77. 0077specialize pair_code_injective (bb)
  78. 0078apply pair_code_injective
  79. 0079exact hfirst_witness_witness_witness_witness_witness_right_left
  80. 0080trans x6
  81. 0081exact hleft_right
  82. 0082exact hsecond_witness_witness_witness_witness_witness_right_left
  83. 0083cases hnexttwo
  84. 0084have hright : nc = bc /\ x3 = x8
  85. 0085specialize pair_code_injective (x4)
  86. 0086specialize pair_code_injective (nc)
  87. 0087specialize pair_code_injective (x3)
  88. 0088specialize pair_code_injective (bc)
  89. 0089specialize pair_code_injective (x8)
  90. 0090apply pair_code_injective
  91. 0091exact hfirst_witness_witness_witness_witness_witness_right_right_right_right_left
  92. 0092trans x9
  93. 0093exact hroot_right
  94. 0094exact hsecond_witness_witness_witness_witness_witness_right_right_right_right_left
  95. 0095cases hright
  96. 0096have hvalues : p = r /\ n = s
  97. 0097specialize pair_code_injective (x3)
  98. 0098specialize pair_code_injective (p)
  99. 0099specialize pair_code_injective (n)
  100. 0100specialize pair_code_injective (r)
  101. 0101specialize pair_code_injective (s)
  102. 0102apply pair_code_injective
  103. 0103exact hfirst_witness_witness_witness_witness_witness_right_right_right_left
  104. 0104trans x8
  105. 0105exact hright_right
  106. 0106exact hsecond_witness_witness_witness_witness_witness_right_right_right_left
  107. 0107cases hvalues
  108. 0108split
  109. 0109exact hfirsttwo_left
  110. 0110split
  111. 0111exact hfirsttwo_right
  112. 0112split
  113. 0113exact hnexttwo_left
  114. 0114split
  115. 0115exact hnexttwo_right
  116. 0116split
  117. 0117exact hright_left
  118. 0118split
  119. 0119exact hvalues_left
  120. 0120exact hvalues_right