DL0087

matrix_integer_pair_product_balance

Actual signed-pair multiplication preserves integer equality in both inputs, by two checked multiplication transports and cancellative cross-sum composition.

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

∀ ap. ∀ an. ∀ bp. ∀ bn. ∀ cp. ∀ cn. ∀ dp. ∀ dn. ap + bn = bp + an → cp + dn = dp + cn → ap · cp + an · cn + (bp · dn + bn · dp) = bp · dp + bn · dn + (ap · cn + an · cp)

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

Definition DAG

none

Actual proof prerequisites

signed_pair_mul_cross_transport · checked external prerequisiteadd_comm · checked external prerequisiteadd_cross_sum_chain · checked external prerequisite
Original expanded first-order statement 
forall ap an bp bn cp cn dp dn. ap + bn = bp + an -> cp + dn = dp + cn -> ((ap) * (cp) + (an) * (cn)) + ((bp) * (dn) + (bn) * (dp)) = ((bp) * (dp) + (bn) * (dn)) + ((ap) * (cn) + (an) * (cp))

Complete tactic proof in conservative notation

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

49 script commands · 9 reading checkpoints · 4 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 ap
  2. L2
    intro an
  3. L3
    intro bp
  4. L4
    intro bn
  5. L5
    intro cp
  6. L6
    intro cn
  7. L7
    intro dp
  8. L8
    intro dn
  9. L9
    intro hrow
  10. L10
    intro hcofactor
02Establish hroworientedL11–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add comm.

  1. L11
    have hroworiented : ap + bn = an + bp
  2. L12
    trans bp + an
  3. L13
    exact hrow
  4. L14
    apply add_comm
03Establish hcoforientedL15–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add comm.

  1. L15
    have hcoforiented : cp + dn = cn + dp
  2. L16
    trans dp + cn
  3. L17
    exact hcofactor
  4. L18
    apply add_comm
04Establish hfirstL19–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed pair mul cross transport.

  1. L19
    have hfirst : ((((ap) * (cp) + (an) * (cn)) + ((bp) * (cn) + (bn) * (cp)) = ((ap) * (cn) + (an) * (cp)) + ((bp) * (cp) + (bn) * (cn))) /\ (((cp) * (ap) + (cn) * (an)) + ((cp) * (bn) + (cn) * (bp)) = ((cp) * (an) + (cn) * (ap)) + ((cp) * (bp) + (cn) * (bn))))
  2. L20
    specialize signed_pair_mul_cross_transport (ap)
  3. L21
    specialize signed_pair_mul_cross_transport (an)
  4. L22
    specialize signed_pair_mul_cross_transport (bp)
  5. L23
    specialize signed_pair_mul_cross_transport (bn)
  6. L24
    specialize signed_pair_mul_cross_transport (cp)
  7. L25
    specialize signed_pair_mul_cross_transport (cn)
  8. L26
    apply signed_pair_mul_cross_transport
  9. L27
    exact hroworiented
05Separate the logical casesL28–28

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

  1. L28
    cases hfirst
06Establish hsecondL29–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed pair mul cross transport.

  1. L29
    have hsecond : ((((cp) * (bp) + (cn) * (bn)) + ((dp) * (bn) + (dn) * (bp)) = ((cp) * (bn) + (cn) * (bp)) + ((dp) * (bp) + (dn) * (bn))) /\ (((bp) * (cp) + (bn) * (cn)) + ((bp) * (dn) + (bn) * (dp)) = ((bp) * (cn) + (bn) * (cp)) + ((bp) * (dp) + (bn) * (dn))))
  2. L30
    specialize signed_pair_mul_cross_transport (cp)
  3. L31
    specialize signed_pair_mul_cross_transport (cn)
  4. L32
    specialize signed_pair_mul_cross_transport (dp)
  5. L33
    specialize signed_pair_mul_cross_transport (dn)
  6. L34
    specialize signed_pair_mul_cross_transport (bp)
  7. L35
    specialize signed_pair_mul_cross_transport (bn)
  8. L36
    apply signed_pair_mul_cross_transport
  9. L37
    exact hcoforiented
07Separate the logical casesL38–38

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

  1. L38
    cases hsecond
08Calculate and transport equalitiesL39–39

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

  1. L39
    trans ((ap) * (cn) + (an) * (cp)) + ((bp) * (dp) + (bn) * (dn))
09Use earlier factsL40–49

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

  1. L40
    specialize add_cross_sum_chain ((ap) * (cp) + (an) * (cn))
  2. L41
    specialize add_cross_sum_chain ((ap) * (cn) + (an) * (cp))
  3. L42
    specialize add_cross_sum_chain ((bp) * (cn) + (bn) * (cp))
  4. L43
    specialize add_cross_sum_chain ((bp) * (cp) + (bn) * (cn))
  5. L44
    specialize add_cross_sum_chain ((bp) * (dn) + (bn) * (dp))
  6. L45
    specialize add_cross_sum_chain ((bp) * (dp) + (bn) * (dn))
  7. L46
    apply add_cross_sum_chain
  8. L47
    exact hfirst_left
  9. L48
    exact hsecond_right
  10. L49
    apply add_comm

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro bp
  4. 0004intro bn
  5. 0005intro cp
  6. 0006intro cn
  7. 0007intro dp
  8. 0008intro dn
  9. 0009intro hrow
  10. 0010intro hcofactor
  11. 0011have hroworiented : ap + bn = an + bp
  12. 0012trans bp + an
  13. 0013exact hrow
  14. 0014apply add_comm
  15. 0015have hcoforiented : cp + dn = cn + dp
  16. 0016trans dp + cn
  17. 0017exact hcofactor
  18. 0018apply add_comm
  19. 0019have hfirst : ((((ap) * (cp) + (an) * (cn)) + ((bp) * (cn) + (bn) * (cp)) = ((ap) * (cn) + (an) * (cp)) + ((bp) * (cp) + (bn) * (cn))) /\ (((cp) * (ap) + (cn) * (an)) + ((cp) * (bn) + (cn) * (bp)) = ((cp) * (an) + (cn) * (ap)) + ((cp) * (bp) + (cn) * (bn))))
  20. 0020specialize signed_pair_mul_cross_transport (ap)
  21. 0021specialize signed_pair_mul_cross_transport (an)
  22. 0022specialize signed_pair_mul_cross_transport (bp)
  23. 0023specialize signed_pair_mul_cross_transport (bn)
  24. 0024specialize signed_pair_mul_cross_transport (cp)
  25. 0025specialize signed_pair_mul_cross_transport (cn)
  26. 0026apply signed_pair_mul_cross_transport
  27. 0027exact hroworiented
  28. 0028cases hfirst
  29. 0029have hsecond : ((((cp) * (bp) + (cn) * (bn)) + ((dp) * (bn) + (dn) * (bp)) = ((cp) * (bn) + (cn) * (bp)) + ((dp) * (bp) + (dn) * (bn))) /\ (((bp) * (cp) + (bn) * (cn)) + ((bp) * (dn) + (bn) * (dp)) = ((bp) * (cn) + (bn) * (cp)) + ((bp) * (dp) + (bn) * (dn))))
  30. 0030specialize signed_pair_mul_cross_transport (cp)
  31. 0031specialize signed_pair_mul_cross_transport (cn)
  32. 0032specialize signed_pair_mul_cross_transport (dp)
  33. 0033specialize signed_pair_mul_cross_transport (dn)
  34. 0034specialize signed_pair_mul_cross_transport (bp)
  35. 0035specialize signed_pair_mul_cross_transport (bn)
  36. 0036apply signed_pair_mul_cross_transport
  37. 0037exact hcoforiented
  38. 0038cases hsecond
  39. 0039trans ((ap) * (cn) + (an) * (cp)) + ((bp) * (dp) + (bn) * (dn))
  40. 0040specialize add_cross_sum_chain ((ap) * (cp) + (an) * (cn))
  41. 0041specialize add_cross_sum_chain ((ap) * (cn) + (an) * (cp))
  42. 0042specialize add_cross_sum_chain ((bp) * (cn) + (bn) * (cp))
  43. 0043specialize add_cross_sum_chain ((bp) * (cp) + (bn) * (cn))
  44. 0044specialize add_cross_sum_chain ((bp) * (dn) + (bn) * (dp))
  45. 0045specialize add_cross_sum_chain ((bp) * (dp) + (bn) * (dn))
  46. 0046apply add_cross_sum_chain
  47. 0047exact hfirst_left
  48. 0048exact hsecond_right
  49. 0049apply add_comm