DL00A6

matrix_lattice_absolute_difference_integer_transport

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

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

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 p n P N D. p + N = P + n -> (((p) = (n) + (D)) \/ ((n) = (p) + (D))) -> (((P) = (N) + (D)) \/ ((N) = (P) + (D)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 37 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL00A5 matrix_lattice_positive_gap_integer_transport DL0088 matrix_integer_pair_negation_balance eq_symm Stable theorem; checked-use authorized

Direct dependents

DL00A9 absolute_recursive_determinant_integer_transport

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

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.

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 exact 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