DL0087

matrix_integer_pair_product_balance

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

signed_pair_mul_cross_transport Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized add_cross_sum_chain Alpha theorem; checked-use authorized

Direct dependents

DL0089 matrix_integer_cofactor_term_balance

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

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.

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