DL00A2

matrix_lattice_absolute_difference_functional

The actual natural absolute value of a signed pair is unique, including the zero and opposite-orientation boundaries.

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

∀ p. ∀ n. ∀ D. ∀ E. p = n + D ∨ n = p + D → p = n + E ∨ n = p + E → D = E

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

Definition DAG

none

Actual proof prerequisites

add_left_cancel · checked external prerequisitematrix_lattice_opposite_gaps_zero
Original expanded first-order statement 
forall p n D E. (((p) = (n) + (D)) \/ ((n) = (p) + (D))) -> (((p) = (n) + (E)) \/ ((n) = (p) + (E))) -> D = E

Complete tactic proof in conservative notation

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

51 script commands · 20 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 (1)
matrix lattice opposite gaps zero
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro D
  4. L4
    intro E
  5. L5
    intro hfirst
  6. L6
    intro hsecond
02Separate the logical casesL7–8

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

  1. L7
    cases hfirst
  2. L8
    cases hsecond
03Use earlier factsL9–12

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

  1. L9
    specialize add_left_cancel (n)
  2. L10
    specialize add_left_cancel (D)
  3. L11
    specialize add_left_cancel (E)
  4. L12
    apply add_left_cancel
04Calculate and transport equalitiesL13–14

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

  1. L13
    trans p
  2. L14
    symm
05Use earlier factsL15–16

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

  1. L15
    exact hfirst_left
  2. L16
    exact hsecond_left
06Establish hzerosL17–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix lattice opposite gaps zero.

  1. L17
    have hzeros : D = 0 /\ E = 0
  2. L18
    specialize matrix_lattice_opposite_gaps_zero (p)
  3. L19
    specialize matrix_lattice_opposite_gaps_zero (n)
  4. L20
    specialize matrix_lattice_opposite_gaps_zero (D)
  5. L21
    specialize matrix_lattice_opposite_gaps_zero (E)
  6. L22
    apply matrix_lattice_opposite_gaps_zero
  7. L23
    exact hfirst_left
  8. L24
    exact hsecond_right
07Separate the logical casesL25–25

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

  1. L25
    cases hzeros
08Calculate and transport equalitiesL26–26

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

  1. L26
    trans 0
09Use earlier factsL27–27

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

  1. L27
    exact hzeros_left
10Calculate and transport equalitiesL28–28

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

  1. L28
    symm
11Use earlier factsL29–29

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

  1. L29
    exact hzeros_right
12Separate the logical casesL30–30

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

  1. L30
    cases hsecond
13Establish hzerosL31–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix lattice opposite gaps zero.

  1. L31
    have hzeros : D = 0 /\ E = 0
  2. L32
    specialize matrix_lattice_opposite_gaps_zero (n)
  3. L33
    specialize matrix_lattice_opposite_gaps_zero (p)
  4. L34
    specialize matrix_lattice_opposite_gaps_zero (D)
  5. L35
    specialize matrix_lattice_opposite_gaps_zero (E)
  6. L36
    apply matrix_lattice_opposite_gaps_zero
  7. L37
    exact hfirst_right
  8. L38
    exact hsecond_left
14Separate the logical casesL39–39

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

  1. L39
    cases hzeros
15Calculate and transport equalitiesL40–40

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

  1. L40
    trans 0
16Use earlier factsL41–41

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

  1. L41
    exact hzeros_left
17Calculate and transport equalitiesL42–42

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

  1. L42
    symm
18Use earlier factsL43–47

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

  1. L43
    exact hzeros_right
  2. L44
    specialize add_left_cancel (p)
  3. L45
    specialize add_left_cancel (D)
  4. L46
    specialize add_left_cancel (E)
  5. L47
    apply add_left_cancel
19Calculate and transport equalitiesL48–49

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

  1. L48
    trans n
  2. L49
    symm
20Use earlier factsL50–51

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

  1. L50
    exact hfirst_right
  2. L51
    exact hsecond_right

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro D
  4. 0004intro E
  5. 0005intro hfirst
  6. 0006intro hsecond
  7. 0007cases hfirst
  8. 0008cases hsecond
  9. 0009specialize add_left_cancel (n)
  10. 0010specialize add_left_cancel (D)
  11. 0011specialize add_left_cancel (E)
  12. 0012apply add_left_cancel
  13. 0013trans p
  14. 0014symm
  15. 0015exact hfirst_left
  16. 0016exact hsecond_left
  17. 0017have hzeros : D = 0 /\ E = 0
  18. 0018specialize matrix_lattice_opposite_gaps_zero (p)
  19. 0019specialize matrix_lattice_opposite_gaps_zero (n)
  20. 0020specialize matrix_lattice_opposite_gaps_zero (D)
  21. 0021specialize matrix_lattice_opposite_gaps_zero (E)
  22. 0022apply matrix_lattice_opposite_gaps_zero
  23. 0023exact hfirst_left
  24. 0024exact hsecond_right
  25. 0025cases hzeros
  26. 0026trans 0
  27. 0027exact hzeros_left
  28. 0028symm
  29. 0029exact hzeros_right
  30. 0030cases hsecond
  31. 0031have hzeros : D = 0 /\ E = 0
  32. 0032specialize matrix_lattice_opposite_gaps_zero (n)
  33. 0033specialize matrix_lattice_opposite_gaps_zero (p)
  34. 0034specialize matrix_lattice_opposite_gaps_zero (D)
  35. 0035specialize matrix_lattice_opposite_gaps_zero (E)
  36. 0036apply matrix_lattice_opposite_gaps_zero
  37. 0037exact hfirst_right
  38. 0038exact hsecond_left
  39. 0039cases hzeros
  40. 0040trans 0
  41. 0041exact hzeros_left
  42. 0042symm
  43. 0043exact hzeros_right
  44. 0044specialize add_left_cancel (p)
  45. 0045specialize add_left_cancel (D)
  46. 0046specialize add_left_cancel (E)
  47. 0047apply add_left_cancel
  48. 0048trans n
  49. 0049symm
  50. 0050exact hfirst_right
  51. 0051exact hsecond_right