BA0018

cf_approximation_signed_basis_normalization

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

Normalizing two actual signed cofactor coefficients gives all four signed coordinate cases constructively.

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 u U v V rp rn t p n q m. ((rp) + ((n) * (u) + (m) * (U)) = (rn) + ((p) * (u) + (q) * (U))) -> ((t) + ((n) * (v) + (m) * (V)) = (0) + ((p) * (v) + (q) * (V))) -> exists c d. (((((rp) = (rn) + ((c) * (u) + (d) * (U))) /\ ((t) = (0) + ((c) * (v) + (d) * (V))))) \/ (((((rp) + (d) * (U) = (rn) + (c) * (u)) /\ ((t) + (d) * (V) = (0) + (c) * (v)))) \/ (((((rp) + (c) * (u) = (rn) + (d) * (U)) /\ ((t) + (c) * (v) = (0) + (d) * (V)))) \/ ((((rp) + ((c) * (u) + (d) * (U)) = (rn)) /\ ((t) + ((c) * (v) + (d) * (V)) = (0)))))))

Constructive proof overview

Generated structural guide

Normalizing two actual signed cofactor coefficients gives all four signed coordinate cases constructively.

The unchanged tactic script uses 5 declared prerequisites and contains 153 exact native proof lines.

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

Proof neighborhood

Direct dependencies

matrix_lattice_absolute_difference_exists Alpha theorem; checked-use authorized BA0012 cf_approximation_signed_coordinates_pp BA0013 cf_approximation_signed_coordinates_pn BA0014 cf_approximation_signed_coordinates_np BA0015 cf_approximation_signed_coordinates_nn

Direct dependents

BA0019 cf_approximation_determinant_one_signed_basis BA001B cf_approximation_determinant_minus_one_signed_basis

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

153 script commands · 23 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.

Named ingredients (4)
cf approximation signed coordinates ppcf approximation signed coordinates pncf approximation signed coordinates npcf approximation signed coordinates nn
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro U
  3. L3
    intro v
  4. L4
    intro V
  5. L5
    intro rp
  6. L6
    intro rn
  7. L7
    intro t
  8. L8
    intro p
  9. L9
    intro n
  10. L10
    intro q
02Fix variables and assumptionsL11–13

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

  1. L11
    intro m
  2. L12
    intro hnumerator
  3. L13
    intro hdenominator
03Establish hpL14–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix lattice absolute difference exists.

  1. L14
    have hp : exists c. (((p) = (n) + (c)) \/ ((n) = (p) + (c)))
  2. L15
    specialize matrix_lattice_absolute_difference_exists (p)
  3. L16
    specialize matrix_lattice_absolute_difference_exists (n)
  4. L17
    apply matrix_lattice_absolute_difference_exists
04Separate the logical casesL18–18

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

  1. L18
    cases hp
05Establish hqL19–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix lattice absolute difference exists.

  1. L19
    have hq : exists d. (((q) = (m) + (d)) \/ ((m) = (q) + (d)))
  2. L20
    specialize matrix_lattice_absolute_difference_exists (q)
  3. L21
    specialize matrix_lattice_absolute_difference_exists (m)
  4. L22
    apply matrix_lattice_absolute_difference_exists
06Separate the logical casesL23–23

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

  1. L23
    cases hq
07Construct an explicit witnessL24–25

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

  1. L24
    exists x
  2. L25
    exists x1
08Separate the logical casesL26–29

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

  1. L26
    cases hp_witness
  2. L27
    cases hq_witness
  3. L28
    left
  4. L29
    split
09Use earlier factsL30–39

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

  1. L30
    specialize cf_approximation_signed_coordinates_pp (rp)
  2. L31
    specialize cf_approximation_signed_coordinates_pp (rn)
  3. L32
    specialize cf_approximation_signed_coordinates_pp (u)
  4. L33
    specialize cf_approximation_signed_coordinates_pp (U)
  5. L34
    specialize cf_approximation_signed_coordinates_pp (p)
  6. L35
    specialize cf_approximation_signed_coordinates_pp (n)
  7. L36
    specialize cf_approximation_signed_coordinates_pp (q)
  8. L37
    specialize cf_approximation_signed_coordinates_pp (m)
  9. L38
    specialize cf_approximation_signed_coordinates_pp (x)
  10. L39
    specialize cf_approximation_signed_coordinates_pp (x1)
10Use earlier factsL40–49

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

  1. L40
    apply cf_approximation_signed_coordinates_pp
  2. L41
    exact hnumerator
  3. L42
    exact hp_witness_left
  4. L43
    exact hq_witness_left
  5. L44
    specialize cf_approximation_signed_coordinates_pp (t)
  6. L45
    specialize cf_approximation_signed_coordinates_pp (0)
  7. L46
    specialize cf_approximation_signed_coordinates_pp (v)
  8. L47
    specialize cf_approximation_signed_coordinates_pp (V)
  9. L48
    specialize cf_approximation_signed_coordinates_pp (p)
  10. L49
    specialize cf_approximation_signed_coordinates_pp (n)
11Use earlier factsL50–57

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

  1. L50
    specialize cf_approximation_signed_coordinates_pp (q)
  2. L51
    specialize cf_approximation_signed_coordinates_pp (m)
  3. L52
    specialize cf_approximation_signed_coordinates_pp (x)
  4. L53
    specialize cf_approximation_signed_coordinates_pp (x1)
  5. L54
    apply cf_approximation_signed_coordinates_pp
  6. L55
    exact hdenominator
  7. L56
    exact hp_witness_left
  8. L57
    exact hq_witness_left
12Separate the logical casesL58–60

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

  1. L58
    right
  2. L59
    left
  3. L60
    split
13Use earlier factsL61–70

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

  1. L61
    specialize cf_approximation_signed_coordinates_pn (rp)
  2. L62
    specialize cf_approximation_signed_coordinates_pn (rn)
  3. L63
    specialize cf_approximation_signed_coordinates_pn (u)
  4. L64
    specialize cf_approximation_signed_coordinates_pn (U)
  5. L65
    specialize cf_approximation_signed_coordinates_pn (p)
  6. L66
    specialize cf_approximation_signed_coordinates_pn (n)
  7. L67
    specialize cf_approximation_signed_coordinates_pn (q)
  8. L68
    specialize cf_approximation_signed_coordinates_pn (m)
  9. L69
    specialize cf_approximation_signed_coordinates_pn (x)
  10. L70
    specialize cf_approximation_signed_coordinates_pn (x1)
14Use earlier factsL71–80

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

  1. L71
    apply cf_approximation_signed_coordinates_pn
  2. L72
    exact hnumerator
  3. L73
    exact hp_witness_left
  4. L74
    exact hq_witness_right
  5. L75
    specialize cf_approximation_signed_coordinates_pn (t)
  6. L76
    specialize cf_approximation_signed_coordinates_pn (0)
  7. L77
    specialize cf_approximation_signed_coordinates_pn (v)
  8. L78
    specialize cf_approximation_signed_coordinates_pn (V)
  9. L79
    specialize cf_approximation_signed_coordinates_pn (p)
  10. L80
    specialize cf_approximation_signed_coordinates_pn (n)
15Use earlier factsL81–88

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

  1. L81
    specialize cf_approximation_signed_coordinates_pn (q)
  2. L82
    specialize cf_approximation_signed_coordinates_pn (m)
  3. L83
    specialize cf_approximation_signed_coordinates_pn (x)
  4. L84
    specialize cf_approximation_signed_coordinates_pn (x1)
  5. L85
    apply cf_approximation_signed_coordinates_pn
  6. L86
    exact hdenominator
  7. L87
    exact hp_witness_left
  8. L88
    exact hq_witness_right
16Separate the logical casesL89–93

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

  1. L89
    cases hq_witness
  2. L90
    right
  3. L91
    right
  4. L92
    left
  5. L93
    split
17Use earlier factsL94–103

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

  1. L94
    specialize cf_approximation_signed_coordinates_np (rp)
  2. L95
    specialize cf_approximation_signed_coordinates_np (rn)
  3. L96
    specialize cf_approximation_signed_coordinates_np (u)
  4. L97
    specialize cf_approximation_signed_coordinates_np (U)
  5. L98
    specialize cf_approximation_signed_coordinates_np (p)
  6. L99
    specialize cf_approximation_signed_coordinates_np (n)
  7. L100
    specialize cf_approximation_signed_coordinates_np (q)
  8. L101
    specialize cf_approximation_signed_coordinates_np (m)
  9. L102
    specialize cf_approximation_signed_coordinates_np (x)
  10. L103
    specialize cf_approximation_signed_coordinates_np (x1)
18Use earlier factsL104–113

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

  1. L104
    apply cf_approximation_signed_coordinates_np
  2. L105
    exact hnumerator
  3. L106
    exact hp_witness_right
  4. L107
    exact hq_witness_left
  5. L108
    specialize cf_approximation_signed_coordinates_np (t)
  6. L109
    specialize cf_approximation_signed_coordinates_np (0)
  7. L110
    specialize cf_approximation_signed_coordinates_np (v)
  8. L111
    specialize cf_approximation_signed_coordinates_np (V)
  9. L112
    specialize cf_approximation_signed_coordinates_np (p)
  10. L113
    specialize cf_approximation_signed_coordinates_np (n)
19Use earlier factsL114–121

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

  1. L114
    specialize cf_approximation_signed_coordinates_np (q)
  2. L115
    specialize cf_approximation_signed_coordinates_np (m)
  3. L116
    specialize cf_approximation_signed_coordinates_np (x)
  4. L117
    specialize cf_approximation_signed_coordinates_np (x1)
  5. L118
    apply cf_approximation_signed_coordinates_np
  6. L119
    exact hdenominator
  7. L120
    exact hp_witness_right
  8. L121
    exact hq_witness_left
20Separate the logical casesL122–125

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

  1. L122
    right
  2. L123
    right
  3. L124
    right
  4. L125
    split
21Use earlier factsL126–135

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

  1. L126
    specialize cf_approximation_signed_coordinates_nn (rp)
  2. L127
    specialize cf_approximation_signed_coordinates_nn (rn)
  3. L128
    specialize cf_approximation_signed_coordinates_nn (u)
  4. L129
    specialize cf_approximation_signed_coordinates_nn (U)
  5. L130
    specialize cf_approximation_signed_coordinates_nn (p)
  6. L131
    specialize cf_approximation_signed_coordinates_nn (n)
  7. L132
    specialize cf_approximation_signed_coordinates_nn (q)
  8. L133
    specialize cf_approximation_signed_coordinates_nn (m)
  9. L134
    specialize cf_approximation_signed_coordinates_nn (x)
  10. L135
    specialize cf_approximation_signed_coordinates_nn (x1)
22Use earlier factsL136–145

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

  1. L136
    apply cf_approximation_signed_coordinates_nn
  2. L137
    exact hnumerator
  3. L138
    exact hp_witness_right
  4. L139
    exact hq_witness_right
  5. L140
    specialize cf_approximation_signed_coordinates_nn (t)
  6. L141
    specialize cf_approximation_signed_coordinates_nn (0)
  7. L142
    specialize cf_approximation_signed_coordinates_nn (v)
  8. L143
    specialize cf_approximation_signed_coordinates_nn (V)
  9. L144
    specialize cf_approximation_signed_coordinates_nn (p)
  10. L145
    specialize cf_approximation_signed_coordinates_nn (n)
23Use earlier factsL146–153

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

  1. L146
    specialize cf_approximation_signed_coordinates_nn (q)
  2. L147
    specialize cf_approximation_signed_coordinates_nn (m)
  3. L148
    specialize cf_approximation_signed_coordinates_nn (x)
  4. L149
    specialize cf_approximation_signed_coordinates_nn (x1)
  5. L150
    apply cf_approximation_signed_coordinates_nn
  6. L151
    exact hdenominator
  7. L152
    exact hp_witness_right
  8. L153
    exact hq_witness_right

Library-wide reading audit

Original exact command ledger · 153 lines
  1. 0001intro u
  2. 0002intro U
  3. 0003intro v
  4. 0004intro V
  5. 0005intro rp
  6. 0006intro rn
  7. 0007intro t
  8. 0008intro p
  9. 0009intro n
  10. 0010intro q
  11. 0011intro m
  12. 0012intro hnumerator
  13. 0013intro hdenominator
  14. 0014have hp : exists c. (((p) = (n) + (c)) \/ ((n) = (p) + (c)))
  15. 0015specialize matrix_lattice_absolute_difference_exists (p)
  16. 0016specialize matrix_lattice_absolute_difference_exists (n)
  17. 0017apply matrix_lattice_absolute_difference_exists
  18. 0018cases hp
  19. 0019have hq : exists d. (((q) = (m) + (d)) \/ ((m) = (q) + (d)))
  20. 0020specialize matrix_lattice_absolute_difference_exists (q)
  21. 0021specialize matrix_lattice_absolute_difference_exists (m)
  22. 0022apply matrix_lattice_absolute_difference_exists
  23. 0023cases hq
  24. 0024exists x
  25. 0025exists x1
  26. 0026cases hp_witness
  27. 0027cases hq_witness
  28. 0028left
  29. 0029split
  30. 0030specialize cf_approximation_signed_coordinates_pp (rp)
  31. 0031specialize cf_approximation_signed_coordinates_pp (rn)
  32. 0032specialize cf_approximation_signed_coordinates_pp (u)
  33. 0033specialize cf_approximation_signed_coordinates_pp (U)
  34. 0034specialize cf_approximation_signed_coordinates_pp (p)
  35. 0035specialize cf_approximation_signed_coordinates_pp (n)
  36. 0036specialize cf_approximation_signed_coordinates_pp (q)
  37. 0037specialize cf_approximation_signed_coordinates_pp (m)
  38. 0038specialize cf_approximation_signed_coordinates_pp (x)
  39. 0039specialize cf_approximation_signed_coordinates_pp (x1)
  40. 0040apply cf_approximation_signed_coordinates_pp
  41. 0041exact hnumerator
  42. 0042exact hp_witness_left
  43. 0043exact hq_witness_left
  44. 0044specialize cf_approximation_signed_coordinates_pp (t)
  45. 0045specialize cf_approximation_signed_coordinates_pp (0)
  46. 0046specialize cf_approximation_signed_coordinates_pp (v)
  47. 0047specialize cf_approximation_signed_coordinates_pp (V)
  48. 0048specialize cf_approximation_signed_coordinates_pp (p)
  49. 0049specialize cf_approximation_signed_coordinates_pp (n)
  50. 0050specialize cf_approximation_signed_coordinates_pp (q)
  51. 0051specialize cf_approximation_signed_coordinates_pp (m)
  52. 0052specialize cf_approximation_signed_coordinates_pp (x)
  53. 0053specialize cf_approximation_signed_coordinates_pp (x1)
  54. 0054apply cf_approximation_signed_coordinates_pp
  55. 0055exact hdenominator
  56. 0056exact hp_witness_left
  57. 0057exact hq_witness_left
  58. 0058right
  59. 0059left
  60. 0060split
  61. 0061specialize cf_approximation_signed_coordinates_pn (rp)
  62. 0062specialize cf_approximation_signed_coordinates_pn (rn)
  63. 0063specialize cf_approximation_signed_coordinates_pn (u)
  64. 0064specialize cf_approximation_signed_coordinates_pn (U)
  65. 0065specialize cf_approximation_signed_coordinates_pn (p)
  66. 0066specialize cf_approximation_signed_coordinates_pn (n)
  67. 0067specialize cf_approximation_signed_coordinates_pn (q)
  68. 0068specialize cf_approximation_signed_coordinates_pn (m)
  69. 0069specialize cf_approximation_signed_coordinates_pn (x)
  70. 0070specialize cf_approximation_signed_coordinates_pn (x1)
  71. 0071apply cf_approximation_signed_coordinates_pn
  72. 0072exact hnumerator
  73. 0073exact hp_witness_left
  74. 0074exact hq_witness_right
  75. 0075specialize cf_approximation_signed_coordinates_pn (t)
  76. 0076specialize cf_approximation_signed_coordinates_pn (0)
  77. 0077specialize cf_approximation_signed_coordinates_pn (v)
  78. 0078specialize cf_approximation_signed_coordinates_pn (V)
  79. 0079specialize cf_approximation_signed_coordinates_pn (p)
  80. 0080specialize cf_approximation_signed_coordinates_pn (n)
  81. 0081specialize cf_approximation_signed_coordinates_pn (q)
  82. 0082specialize cf_approximation_signed_coordinates_pn (m)
  83. 0083specialize cf_approximation_signed_coordinates_pn (x)
  84. 0084specialize cf_approximation_signed_coordinates_pn (x1)
  85. 0085apply cf_approximation_signed_coordinates_pn
  86. 0086exact hdenominator
  87. 0087exact hp_witness_left
  88. 0088exact hq_witness_right
  89. 0089cases hq_witness
  90. 0090right
  91. 0091right
  92. 0092left
  93. 0093split
  94. 0094specialize cf_approximation_signed_coordinates_np (rp)
  95. 0095specialize cf_approximation_signed_coordinates_np (rn)
  96. 0096specialize cf_approximation_signed_coordinates_np (u)
  97. 0097specialize cf_approximation_signed_coordinates_np (U)
  98. 0098specialize cf_approximation_signed_coordinates_np (p)
  99. 0099specialize cf_approximation_signed_coordinates_np (n)
  100. 0100specialize cf_approximation_signed_coordinates_np (q)
  101. 0101specialize cf_approximation_signed_coordinates_np (m)
  102. 0102specialize cf_approximation_signed_coordinates_np (x)
  103. 0103specialize cf_approximation_signed_coordinates_np (x1)
  104. 0104apply cf_approximation_signed_coordinates_np
  105. 0105exact hnumerator
  106. 0106exact hp_witness_right
  107. 0107exact hq_witness_left
  108. 0108specialize cf_approximation_signed_coordinates_np (t)
  109. 0109specialize cf_approximation_signed_coordinates_np (0)
  110. 0110specialize cf_approximation_signed_coordinates_np (v)
  111. 0111specialize cf_approximation_signed_coordinates_np (V)
  112. 0112specialize cf_approximation_signed_coordinates_np (p)
  113. 0113specialize cf_approximation_signed_coordinates_np (n)
  114. 0114specialize cf_approximation_signed_coordinates_np (q)
  115. 0115specialize cf_approximation_signed_coordinates_np (m)
  116. 0116specialize cf_approximation_signed_coordinates_np (x)
  117. 0117specialize cf_approximation_signed_coordinates_np (x1)
  118. 0118apply cf_approximation_signed_coordinates_np
  119. 0119exact hdenominator
  120. 0120exact hp_witness_right
  121. 0121exact hq_witness_left
  122. 0122right
  123. 0123right
  124. 0124right
  125. 0125split
  126. 0126specialize cf_approximation_signed_coordinates_nn (rp)
  127. 0127specialize cf_approximation_signed_coordinates_nn (rn)
  128. 0128specialize cf_approximation_signed_coordinates_nn (u)
  129. 0129specialize cf_approximation_signed_coordinates_nn (U)
  130. 0130specialize cf_approximation_signed_coordinates_nn (p)
  131. 0131specialize cf_approximation_signed_coordinates_nn (n)
  132. 0132specialize cf_approximation_signed_coordinates_nn (q)
  133. 0133specialize cf_approximation_signed_coordinates_nn (m)
  134. 0134specialize cf_approximation_signed_coordinates_nn (x)
  135. 0135specialize cf_approximation_signed_coordinates_nn (x1)
  136. 0136apply cf_approximation_signed_coordinates_nn
  137. 0137exact hnumerator
  138. 0138exact hp_witness_right
  139. 0139exact hq_witness_right
  140. 0140specialize cf_approximation_signed_coordinates_nn (t)
  141. 0141specialize cf_approximation_signed_coordinates_nn (0)
  142. 0142specialize cf_approximation_signed_coordinates_nn (v)
  143. 0143specialize cf_approximation_signed_coordinates_nn (V)
  144. 0144specialize cf_approximation_signed_coordinates_nn (p)
  145. 0145specialize cf_approximation_signed_coordinates_nn (n)
  146. 0146specialize cf_approximation_signed_coordinates_nn (q)
  147. 0147specialize cf_approximation_signed_coordinates_nn (m)
  148. 0148specialize cf_approximation_signed_coordinates_nn (x)
  149. 0149specialize cf_approximation_signed_coordinates_nn (x1)
  150. 0150apply cf_approximation_signed_coordinates_nn
  151. 0151exact hdenominator
  152. 0152exact hp_witness_right
  153. 0153exact hq_witness_right