DL0089

matrix_integer_cofactor_term_balance

Each genuine parity-correct signed cofactor term respects integer equality of its row entry and its evaluated cofactor, in both parity branches.

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. ∀ cp. ∀ cn. ∀ bp. ∀ bn. ∀ dp. ∀ dn. ∀ i. ∀ p. ∀ n. ∀ P. ∀ N. ap + bn = bp + an → cp + dn = dp + cn → SignedAlternatingCofactorTerm(ap,an,cp,cn,i,p,n) → SignedAlternatingCofactorTerm(bp,bn,dp,dn,i,P,N) → p + N = P + n

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

Definition DAG

SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n) · 2

Actual proof prerequisites

signed_alternating_cofactor_term_even · checked external prerequisitesigned_alternating_cofactor_term_odd · checked external prerequisitematrix_integer_pair_product_balancematrix_integer_pair_negation_balance
Original expanded first-order statement 
forall ap an cp cn bp bn dp dn i p n P N. ap + bn = bp + an -> cp + dn = dp + cn -> (((exists ff_even_mce_term_integer_first_term. i = 2 * ff_even_mce_term_integer_first_term) /\ (p = (ap) * (cp) + (an) * (cn) /\ n = (ap) * (cn) + (an) * (cp))) \/ ((exists ff_odd_mce_term_integer_first_term. i = 2 * ff_odd_mce_term_integer_first_term + 1) /\ (p = (ap) * (cn) + (an) * (cp) /\ n = (ap) * (cp) + (an) * (cn)))) -> (((exists ff_even_mce_term_integer_second_term. i = 2 * ff_even_mce_term_integer_second_term) /\ (P = (bp) * (dp) + (bn) * (dn) /\ N = (bp) * (dn) + (bn) * (dp))) \/ ((exists ff_odd_mce_term_integer_second_term. i = 2 * ff_odd_mce_term_integer_second_term + 1) /\ (P = (bp) * (dn) + (bn) * (dp) /\ N = (bp) * (dp) + (bn) * (dn)))) -> p + N = P + n

Complete tactic proof in conservative notation

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

81 script commands · 16 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 (2)
matrix integer pair product balancematrix integer pair negation balance
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 cp
  4. L4
    intro cn
  5. L5
    intro bp
  6. L6
    intro bn
  7. L7
    intro dp
  8. L8
    intro dn
  9. L9
    intro i
  10. L10
    intro p
02Fix variables and assumptionsL11–17

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

  1. L11
    intro n
  2. L12
    intro P
  3. L13
    intro N
  4. L14
    intro hrow
  5. L15
    intro hcofactor
  6. L16
    intro hfirst
  7. L17
    intro hsecond
03Separate the logical casesL18–20

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

  1. L18
    cases hfirst
  2. L19
    cases hfirst_left
  3. L20
    cases hfirst_left_right
04Establish hotherL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed alternating cofactor term even.

  1. L21
    have hother : P = ((bp) * (dp) + (bn) * (dn)) /\ N = ((bp) * (dn) + (bn) * (dp))
  2. L22
    specialize signed_alternating_cofactor_term_even (bp)
  3. L23
    specialize signed_alternating_cofactor_term_even (bn)
  4. L24
    specialize signed_alternating_cofactor_term_even (dp)
  5. L25
    specialize signed_alternating_cofactor_term_even (dn)
  6. L26
    specialize signed_alternating_cofactor_term_even (i)
  7. L27
    specialize signed_alternating_cofactor_term_even (P)
  8. L28
    specialize signed_alternating_cofactor_term_even (N)
  9. L29
    apply signed_alternating_cofactor_term_even
  10. L30
    exact hsecond
05Use earlier factsL31–31

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

  1. L31
    exact hfirst_left_left
06Separate the logical casesL32–32

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

  1. L32
    cases hother
07Calculate and transport equalitiesL33–36

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

  1. L33
    rewrite hfirst_left_right_left
  2. L34
    rewrite hfirst_left_right_right
  3. L35
    rewrite hother_left
  4. L36
    rewrite hother_right
08Use earlier factsL37–46

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

  1. L37
    specialize matrix_integer_pair_product_balance (ap)
  2. L38
    specialize matrix_integer_pair_product_balance (an)
  3. L39
    specialize matrix_integer_pair_product_balance (bp)
  4. L40
    specialize matrix_integer_pair_product_balance (bn)
  5. L41
    specialize matrix_integer_pair_product_balance (cp)
  6. L42
    specialize matrix_integer_pair_product_balance (cn)
  7. L43
    specialize matrix_integer_pair_product_balance (dp)
  8. L44
    specialize matrix_integer_pair_product_balance (dn)
  9. L45
    apply matrix_integer_pair_product_balance
  10. L46
    exact hrow
09Use earlier factsL47–47

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

  1. L47
    exact hcofactor
10Separate the logical casesL48–49

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

  1. L48
    cases hfirst_right
  2. L49
    cases hfirst_right_right
11Establish hotherL50–59

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed alternating cofactor term odd.

  1. L50
    have hother : P = ((bp) * (dn) + (bn) * (dp)) /\ N = ((bp) * (dp) + (bn) * (dn))
  2. L51
    specialize signed_alternating_cofactor_term_odd (bp)
  3. L52
    specialize signed_alternating_cofactor_term_odd (bn)
  4. L53
    specialize signed_alternating_cofactor_term_odd (dp)
  5. L54
    specialize signed_alternating_cofactor_term_odd (dn)
  6. L55
    specialize signed_alternating_cofactor_term_odd (i)
  7. L56
    specialize signed_alternating_cofactor_term_odd (P)
  8. L57
    specialize signed_alternating_cofactor_term_odd (N)
  9. L58
    apply signed_alternating_cofactor_term_odd
  10. L59
    exact hsecond
12Use earlier factsL60–60

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

  1. L60
    exact hfirst_right_left
13Separate the logical casesL61–61

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

  1. L61
    cases hother
14Calculate and transport equalitiesL62–65

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

  1. L62
    rewrite hfirst_right_right_left
  2. L63
    rewrite hfirst_right_right_right
  3. L64
    rewrite hother_left
  4. L65
    rewrite hother_right
15Use earlier factsL66–75

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

  1. L66
    specialize matrix_integer_pair_negation_balance ((ap) * (cp) + (an) * (cn))
  2. L67
    specialize matrix_integer_pair_negation_balance ((ap) * (cn) + (an) * (cp))
  3. L68
    specialize matrix_integer_pair_negation_balance ((bp) * (dp) + (bn) * (dn))
  4. L69
    specialize matrix_integer_pair_negation_balance ((bp) * (dn) + (bn) * (dp))
  5. L70
    apply matrix_integer_pair_negation_balance
  6. L71
    specialize matrix_integer_pair_product_balance (ap)
  7. L72
    specialize matrix_integer_pair_product_balance (an)
  8. L73
    specialize matrix_integer_pair_product_balance (bp)
  9. L74
    specialize matrix_integer_pair_product_balance (bn)
  10. L75
    specialize matrix_integer_pair_product_balance (cp)
16Use earlier factsL76–81

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

  1. L76
    specialize matrix_integer_pair_product_balance (cn)
  2. L77
    specialize matrix_integer_pair_product_balance (dp)
  3. L78
    specialize matrix_integer_pair_product_balance (dn)
  4. L79
    apply matrix_integer_pair_product_balance
  5. L80
    exact hrow
  6. L81
    exact hcofactor

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro cp
  4. 0004intro cn
  5. 0005intro bp
  6. 0006intro bn
  7. 0007intro dp
  8. 0008intro dn
  9. 0009intro i
  10. 0010intro p
  11. 0011intro n
  12. 0012intro P
  13. 0013intro N
  14. 0014intro hrow
  15. 0015intro hcofactor
  16. 0016intro hfirst
  17. 0017intro hsecond
  18. 0018cases hfirst
  19. 0019cases hfirst_left
  20. 0020cases hfirst_left_right
  21. 0021have hother : P = ((bp) * (dp) + (bn) * (dn)) /\ N = ((bp) * (dn) + (bn) * (dp))
  22. 0022specialize signed_alternating_cofactor_term_even (bp)
  23. 0023specialize signed_alternating_cofactor_term_even (bn)
  24. 0024specialize signed_alternating_cofactor_term_even (dp)
  25. 0025specialize signed_alternating_cofactor_term_even (dn)
  26. 0026specialize signed_alternating_cofactor_term_even (i)
  27. 0027specialize signed_alternating_cofactor_term_even (P)
  28. 0028specialize signed_alternating_cofactor_term_even (N)
  29. 0029apply signed_alternating_cofactor_term_even
  30. 0030exact hsecond
  31. 0031exact hfirst_left_left
  32. 0032cases hother
  33. 0033rewrite hfirst_left_right_left
  34. 0034rewrite hfirst_left_right_right
  35. 0035rewrite hother_left
  36. 0036rewrite hother_right
  37. 0037specialize matrix_integer_pair_product_balance (ap)
  38. 0038specialize matrix_integer_pair_product_balance (an)
  39. 0039specialize matrix_integer_pair_product_balance (bp)
  40. 0040specialize matrix_integer_pair_product_balance (bn)
  41. 0041specialize matrix_integer_pair_product_balance (cp)
  42. 0042specialize matrix_integer_pair_product_balance (cn)
  43. 0043specialize matrix_integer_pair_product_balance (dp)
  44. 0044specialize matrix_integer_pair_product_balance (dn)
  45. 0045apply matrix_integer_pair_product_balance
  46. 0046exact hrow
  47. 0047exact hcofactor
  48. 0048cases hfirst_right
  49. 0049cases hfirst_right_right
  50. 0050have hother : P = ((bp) * (dn) + (bn) * (dp)) /\ N = ((bp) * (dp) + (bn) * (dn))
  51. 0051specialize signed_alternating_cofactor_term_odd (bp)
  52. 0052specialize signed_alternating_cofactor_term_odd (bn)
  53. 0053specialize signed_alternating_cofactor_term_odd (dp)
  54. 0054specialize signed_alternating_cofactor_term_odd (dn)
  55. 0055specialize signed_alternating_cofactor_term_odd (i)
  56. 0056specialize signed_alternating_cofactor_term_odd (P)
  57. 0057specialize signed_alternating_cofactor_term_odd (N)
  58. 0058apply signed_alternating_cofactor_term_odd
  59. 0059exact hsecond
  60. 0060exact hfirst_right_left
  61. 0061cases hother
  62. 0062rewrite hfirst_right_right_left
  63. 0063rewrite hfirst_right_right_right
  64. 0064rewrite hother_left
  65. 0065rewrite hother_right
  66. 0066specialize matrix_integer_pair_negation_balance ((ap) * (cp) + (an) * (cn))
  67. 0067specialize matrix_integer_pair_negation_balance ((ap) * (cn) + (an) * (cp))
  68. 0068specialize matrix_integer_pair_negation_balance ((bp) * (dp) + (bn) * (dn))
  69. 0069specialize matrix_integer_pair_negation_balance ((bp) * (dn) + (bn) * (dp))
  70. 0070apply matrix_integer_pair_negation_balance
  71. 0071specialize matrix_integer_pair_product_balance (ap)
  72. 0072specialize matrix_integer_pair_product_balance (an)
  73. 0073specialize matrix_integer_pair_product_balance (bp)
  74. 0074specialize matrix_integer_pair_product_balance (bn)
  75. 0075specialize matrix_integer_pair_product_balance (cp)
  76. 0076specialize matrix_integer_pair_product_balance (cn)
  77. 0077specialize matrix_integer_pair_product_balance (dp)
  78. 0078specialize matrix_integer_pair_product_balance (dn)
  79. 0079apply matrix_integer_pair_product_balance
  80. 0080exact hrow
  81. 0081exact hcofactor