DL00A6

matrix_lattice_absolute_difference_integer_transport

Natural absolute value is an invariant of the represented integer, not of the chosen positive and negative components.

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. ∀ P. ∀ N. ∀ D. p + N = P + n → p = n + D ∨ n = p + D → P = N + D ∨ N = P + D

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

Definition DAG

none

Actual proof prerequisites

matrix_lattice_positive_gap_integer_transportmatrix_integer_pair_negation_balanceeq_symm · checked external prerequisite
Original expanded first-order statement 
forall p n P N D. p + N = P + n -> (((p) = (n) + (D)) \/ ((n) = (p) + (D))) -> (((P) = (N) + (D)) \/ ((N) = (P) + (D)))

Complete tactic proof in conservative notation

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

37 script commands · 7 reading checkpoints · 0 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 lattice positive gap integer transportmatrix integer pair negation balance
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro P
  4. L4
    intro N
  5. L5
    intro D
  6. L6
    intro hbalance
  7. L7
    intro habsolute
02Separate the logical casesL8–9

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

  1. L8
    cases habsolute
  2. L9
    left
03Use earlier factsL10–19

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

  1. L10
    specialize matrix_lattice_positive_gap_integer_transport (P)
  2. L11
    specialize matrix_lattice_positive_gap_integer_transport (N)
  3. L12
    specialize matrix_lattice_positive_gap_integer_transport (p)
  4. L13
    specialize matrix_lattice_positive_gap_integer_transport (n)
  5. L14
    specialize matrix_lattice_positive_gap_integer_transport (D)
  6. L15
    apply matrix_lattice_positive_gap_integer_transport
  7. L16
    specialize eq_symm (p + N)
  8. L17
    specialize eq_symm (P + n)
  9. L18
    apply eq_symm
  10. L19
    exact hbalance
04Use earlier factsL20–20

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

  1. L20
    exact habsolute_left
05Separate the logical casesL21–21

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

  1. L21
    right
06Use earlier factsL22–31

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

  1. L22
    specialize matrix_lattice_positive_gap_integer_transport (N)
  2. L23
    specialize matrix_lattice_positive_gap_integer_transport (P)
  3. L24
    specialize matrix_lattice_positive_gap_integer_transport (n)
  4. L25
    specialize matrix_lattice_positive_gap_integer_transport (p)
  5. L26
    specialize matrix_lattice_positive_gap_integer_transport (D)
  6. L27
    apply matrix_lattice_positive_gap_integer_transport
  7. L28
    specialize eq_symm (n + P)
  8. L29
    specialize eq_symm (N + p)
  9. L30
    apply eq_symm
  10. L31
    specialize matrix_integer_pair_negation_balance (p)
07Use earlier factsL32–37

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

  1. L32
    specialize matrix_integer_pair_negation_balance (n)
  2. L33
    specialize matrix_integer_pair_negation_balance (P)
  3. L34
    specialize matrix_integer_pair_negation_balance (N)
  4. L35
    apply matrix_integer_pair_negation_balance
  5. L36
    exact hbalance
  6. L37
    exact habsolute_right

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro P
  4. 0004intro N
  5. 0005intro D
  6. 0006intro hbalance
  7. 0007intro habsolute
  8. 0008cases habsolute
  9. 0009left
  10. 0010specialize matrix_lattice_positive_gap_integer_transport (P)
  11. 0011specialize matrix_lattice_positive_gap_integer_transport (N)
  12. 0012specialize matrix_lattice_positive_gap_integer_transport (p)
  13. 0013specialize matrix_lattice_positive_gap_integer_transport (n)
  14. 0014specialize matrix_lattice_positive_gap_integer_transport (D)
  15. 0015apply matrix_lattice_positive_gap_integer_transport
  16. 0016specialize eq_symm (p + N)
  17. 0017specialize eq_symm (P + n)
  18. 0018apply eq_symm
  19. 0019exact hbalance
  20. 0020exact habsolute_left
  21. 0021right
  22. 0022specialize matrix_lattice_positive_gap_integer_transport (N)
  23. 0023specialize matrix_lattice_positive_gap_integer_transport (P)
  24. 0024specialize matrix_lattice_positive_gap_integer_transport (n)
  25. 0025specialize matrix_lattice_positive_gap_integer_transport (p)
  26. 0026specialize matrix_lattice_positive_gap_integer_transport (D)
  27. 0027apply matrix_lattice_positive_gap_integer_transport
  28. 0028specialize eq_symm (n + P)
  29. 0029specialize eq_symm (N + p)
  30. 0030apply eq_symm
  31. 0031specialize matrix_integer_pair_negation_balance (p)
  32. 0032specialize matrix_integer_pair_negation_balance (n)
  33. 0033specialize matrix_integer_pair_negation_balance (P)
  34. 0034specialize matrix_integer_pair_negation_balance (N)
  35. 0035apply matrix_integer_pair_negation_balance
  36. 0036exact hbalance
  37. 0037exact habsolute_right