SS0013

divisor_signed_table_equality_component_balance

Pointwise equality of canonical lookup values implies balanced integer equality of arbitrary component streams, without equating the components themselves.

Alpha v34 checked-use · first admitted v31 · 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.

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ qb. ∀ qc. ∀ mb. ∀ mc. ∀ l. MatrixMinorFourCode(F,pb,pc,nb,nc) → MatrixMinorFourCode(G,qb,qc,mb,mc) → ArithTableEqual(F,G,l) → ∀ x. ∀ y. ∀ z. ∀ n. ∀ m. Lt(x,l) → BetaAt(pb,pc,x,y) → BetaAt(nb,nc,x,z) → BetaAt(qb,qc,x,n) → BetaAt(mb,mc,x,m) → y + m = n + z

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

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 2SignedBalance(z,p,n) · 2ArithTableEqual(F,G,l) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 4

Actual proof prerequisites

signed_balance_total · checked external prerequisitedivisor_signed_table_at_from_componentsgaussian_signed_balance_same_code · checked external prerequisite
Original expanded first-order statement 
forall F G pb pc nb nc qb qc mb mc l. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> ((G) = (((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) * S ((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) + ((((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))))) -> (forall dst_index_equal_codes dst_first_equal_codes dst_second_equal_codes. (exists pvs_gap_equal_codesbound. pvs_gap_equal_codesbound + S (dst_index_equal_codes) = (l)) -> (exists dst_positive_code_equal_codesfirst dst_positive_scale_equal_codesfirst dst_negative_code_equal_codesfirst dst_negative_scale_equal_codesfirst dst_positive_equal_codesfirst dst_negative_equal_codesfirst. (((F) = (((((dst_positive_code_equal_codesfirst) + (dst_positive_scale_equal_codesfirst)) * S ((dst_positive_code_equal_codesfirst) + (dst_positive_scale_equal_codesfirst)) + ((dst_positive_scale_equal_codesfirst) + (dst_positive_scale_equal_codesfirst))) + (((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) * S ((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) + ((dst_negative_scale_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)))) * S ((((dst_positive_code_equal_codesfirst) + (dst_positive_scale_equal_codesfirst)) * S ((dst_positive_code_equal_codesfirst) + (dst_positive_scale_equal_codesfirst)) + ((dst_positive_scale_equal_codesfirst) + (dst_positive_scale_equal_codesfirst))) + (((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) * S ((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) + ((dst_negative_scale_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)))) + ((((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) * S ((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) + ((dst_negative_scale_equal_codesfirst) + (dst_negative_scale_equal_codesfirst))) + (((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) * S ((dst_negative_code_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)) + ((dst_negative_scale_equal_codesfirst) + (dst_negative_scale_equal_codesfirst)))))) /\ (((((exists ff_h_pvs_equal_codesfirstpositive. ff_h_pvs_equal_codesfirstpositive + S (dst_positive_equal_codesfirst) = S ((S (dst_index_equal_codes)) * dst_positive_scale_equal_codesfirst)) /\ exists ff_q_pvs_equal_codesfirstpositive. dst_positive_code_equal_codesfirst = ff_q_pvs_equal_codesfirstpositive * S ((S (dst_index_equal_codes)) * dst_positive_scale_equal_codesfirst) + (dst_positive_equal_codesfirst))) /\ (((((exists ff_h_pvs_equal_codesfirstnegative. ff_h_pvs_equal_codesfirstnegative + S (dst_negative_equal_codesfirst) = S ((S (dst_index_equal_codes)) * dst_negative_scale_equal_codesfirst)) /\ exists ff_q_pvs_equal_codesfirstnegative. dst_negative_code_equal_codesfirst = ff_q_pvs_equal_codesfirstnegative * S ((S (dst_index_equal_codes)) * dst_negative_scale_equal_codesfirst) + (dst_negative_equal_codesfirst))) /\ (exists ge_balance_positive_equal_codesfirstvalue ge_balance_negative_equal_codesfirstvalue. (((((dst_first_equal_codes) = 2 * (ge_balance_positive_equal_codesfirstvalue) /\ (ge_balance_negative_equal_codesfirstvalue) = 0) \/ exists ge_signed_half_equal_codesfirstvaluedecode. (((dst_first_equal_codes) = 2 * ge_signed_half_equal_codesfirstvaluedecode + 1 /\ (ge_balance_positive_equal_codesfirstvalue) = 0) /\ (ge_balance_negative_equal_codesfirstvalue) = S ge_signed_half_equal_codesfirstvaluedecode))) /\ ((dst_positive_equal_codesfirst) + ge_balance_negative_equal_codesfirstvalue = (dst_negative_equal_codesfirst) + ge_balance_positive_equal_codesfirstvalue))))))))) -> (exists dst_positive_code_equal_codessecond dst_positive_scale_equal_codessecond dst_negative_code_equal_codessecond dst_negative_scale_equal_codessecond dst_positive_equal_codessecond dst_negative_equal_codessecond. (((G) = (((((dst_positive_code_equal_codessecond) + (dst_positive_scale_equal_codessecond)) * S ((dst_positive_code_equal_codessecond) + (dst_positive_scale_equal_codessecond)) + ((dst_positive_scale_equal_codessecond) + (dst_positive_scale_equal_codessecond))) + (((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) * S ((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) + ((dst_negative_scale_equal_codessecond) + (dst_negative_scale_equal_codessecond)))) * S ((((dst_positive_code_equal_codessecond) + (dst_positive_scale_equal_codessecond)) * S ((dst_positive_code_equal_codessecond) + (dst_positive_scale_equal_codessecond)) + ((dst_positive_scale_equal_codessecond) + (dst_positive_scale_equal_codessecond))) + (((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) * S ((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) + ((dst_negative_scale_equal_codessecond) + (dst_negative_scale_equal_codessecond)))) + ((((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) * S ((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) + ((dst_negative_scale_equal_codessecond) + (dst_negative_scale_equal_codessecond))) + (((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) * S ((dst_negative_code_equal_codessecond) + (dst_negative_scale_equal_codessecond)) + ((dst_negative_scale_equal_codessecond) + (dst_negative_scale_equal_codessecond)))))) /\ (((((exists ff_h_pvs_equal_codessecondpositive. ff_h_pvs_equal_codessecondpositive + S (dst_positive_equal_codessecond) = S ((S (dst_index_equal_codes)) * dst_positive_scale_equal_codessecond)) /\ exists ff_q_pvs_equal_codessecondpositive. dst_positive_code_equal_codessecond = ff_q_pvs_equal_codessecondpositive * S ((S (dst_index_equal_codes)) * dst_positive_scale_equal_codessecond) + (dst_positive_equal_codessecond))) /\ (((((exists ff_h_pvs_equal_codessecondnegative. ff_h_pvs_equal_codessecondnegative + S (dst_negative_equal_codessecond) = S ((S (dst_index_equal_codes)) * dst_negative_scale_equal_codessecond)) /\ exists ff_q_pvs_equal_codessecondnegative. dst_negative_code_equal_codessecond = ff_q_pvs_equal_codessecondnegative * S ((S (dst_index_equal_codes)) * dst_negative_scale_equal_codessecond) + (dst_negative_equal_codessecond))) /\ (exists ge_balance_positive_equal_codessecondvalue ge_balance_negative_equal_codessecondvalue. (((((dst_second_equal_codes) = 2 * (ge_balance_positive_equal_codessecondvalue) /\ (ge_balance_negative_equal_codessecondvalue) = 0) \/ exists ge_signed_half_equal_codessecondvaluedecode. (((dst_second_equal_codes) = 2 * ge_signed_half_equal_codessecondvaluedecode + 1 /\ (ge_balance_positive_equal_codessecondvalue) = 0) /\ (ge_balance_negative_equal_codessecondvalue) = S ge_signed_half_equal_codessecondvaluedecode))) /\ ((dst_positive_equal_codessecond) + ge_balance_negative_equal_codessecondvalue = (dst_negative_equal_codessecond) + ge_balance_positive_equal_codessecondvalue))))))))) -> dst_first_equal_codes = dst_second_equal_codes) -> (forall ics_index_equal_components ics_value0_equal_components ics_value1_equal_components ics_value2_equal_components ics_value3_equal_components. (exists ics_gap_equal_components_bound. ics_gap_equal_components_bound + S (ics_index_equal_components) = (l)) -> (((exists fs_h_ics_equal_components_at0. fs_h_ics_equal_components_at0 + S (ics_value0_equal_components) = S ((S (ics_index_equal_components)) * pc)) /\ exists fs_q_ics_equal_components_at0. pb = fs_q_ics_equal_components_at0 * S ((S (ics_index_equal_components)) * pc) + (ics_value0_equal_components))) -> (((exists fs_h_ics_equal_components_at1. fs_h_ics_equal_components_at1 + S (ics_value1_equal_components) = S ((S (ics_index_equal_components)) * nc)) /\ exists fs_q_ics_equal_components_at1. nb = fs_q_ics_equal_components_at1 * S ((S (ics_index_equal_components)) * nc) + (ics_value1_equal_components))) -> (((exists fs_h_ics_equal_components_at2. fs_h_ics_equal_components_at2 + S (ics_value2_equal_components) = S ((S (ics_index_equal_components)) * qc)) /\ exists fs_q_ics_equal_components_at2. qb = fs_q_ics_equal_components_at2 * S ((S (ics_index_equal_components)) * qc) + (ics_value2_equal_components))) -> (((exists fs_h_ics_equal_components_at3. fs_h_ics_equal_components_at3 + S (ics_value3_equal_components) = S ((S (ics_index_equal_components)) * mc)) /\ exists fs_q_ics_equal_components_at3. mb = fs_q_ics_equal_components_at3 * S ((S (ics_index_equal_components)) * mc) + (ics_value3_equal_components))) -> ics_value0_equal_components + ics_value3_equal_components = ics_value2_equal_components + ics_value1_equal_components)

Complete tactic proof in conservative notation

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

78 script commands · 13 reading checkpoints · 3 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 (1)
divisor signed table at from components
01Fix variables and assumptionsL1–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro pb
  4. L4
    intro pc
  5. L5
    intro nb
  6. L6
    intro nc
  7. L7
    intro qb
  8. L8
    intro qc
  9. L9
    intro mb
  10. L10
    intro mc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro l
  2. L12
    intro hF
  3. L13
    intro hG
  4. L14
    intro hequal
  5. L15
    intro i
  6. L16
    intro p
  7. L17
    intro n
  8. L18
    intro q
  9. L19
    intro m
  10. L20
    intro hi
03Fix variables and assumptionsL21–24

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

  1. L21
    intro hp
  2. L22
    intro hn
  3. L23
    intro hq
  4. L24
    intro hm
04Establish hxL25–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance total.

  1. L25
    have hx : ∃ x. SignedBalance(x,p,n)Definitions: SignedBalance(x,p,n)Original native command in the exact edition
  2. L26
    specialize signed_balance_total (p)
  3. L27
    specialize signed_balance_total (n)
  4. L28
    apply signed_balance_total
05Separate the logical casesL29–29

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

  1. L29
    cases hx
06Establish hyL30–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance total.

  1. L30
    have hy : ∃ y. SignedBalance(y,q,m)Definitions: SignedBalance(y,q,m)Original native command in the exact edition
  2. L31
    specialize signed_balance_total (q)
  3. L32
    specialize signed_balance_total (m)
  4. L33
    apply signed_balance_total
07Separate the logical casesL34–34

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

  1. L34
    cases hy
08Establish heqL35–44

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

  1. L35
    have heq : x = x1
  2. L36
    specialize hequal (i)
  3. L37
    specialize hequal (x)
  4. L38
    specialize hequal (x1)
  5. L39
    apply hequal
  6. L40
    exact hi
  7. L41
    specialize divisor_signed_table_at_from_components (F)
  8. L42
    specialize divisor_signed_table_at_from_components (pb)
  9. L43
    specialize divisor_signed_table_at_from_components (pc)
  10. L44
    specialize divisor_signed_table_at_from_components (nb)
09Use earlier factsL45–54

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

  1. L45
    specialize divisor_signed_table_at_from_components (nc)
  2. L46
    specialize divisor_signed_table_at_from_components (i)
  3. L47
    specialize divisor_signed_table_at_from_components (p)
  4. L48
    specialize divisor_signed_table_at_from_components (n)
  5. L49
    specialize divisor_signed_table_at_from_components (x)
  6. L50
    apply divisor_signed_table_at_from_components
  7. L51
    exact hF
  8. L52
    exact hp
  9. L53
    exact hn
  10. L54
    exact hx_witness
10Use earlier factsL55–64

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

  1. L55
    specialize divisor_signed_table_at_from_components (G)
  2. L56
    specialize divisor_signed_table_at_from_components (qb)
  3. L57
    specialize divisor_signed_table_at_from_components (qc)
  4. L58
    specialize divisor_signed_table_at_from_components (mb)
  5. L59
    specialize divisor_signed_table_at_from_components (mc)
  6. L60
    specialize divisor_signed_table_at_from_components (i)
  7. L61
    specialize divisor_signed_table_at_from_components (q)
  8. L62
    specialize divisor_signed_table_at_from_components (m)
  9. L63
    specialize divisor_signed_table_at_from_components (x1)
  10. L64
    apply divisor_signed_table_at_from_components
11Use earlier factsL65–68

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

  1. L65
    exact hG
  2. L66
    exact hq
  3. L67
    exact hm
  4. L68
    exact hy_witness
12Calculate and transport equalitiesL69–70

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

  1. L69
    rewrite heq at hx_witness
  2. L70
    rewrite heq at hx_witness
13Use earlier factsL71–78

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

  1. L71
    specialize gaussian_signed_balance_same_code (x1)
  2. L72
    specialize gaussian_signed_balance_same_code (p)
  3. L73
    specialize gaussian_signed_balance_same_code (n)
  4. L74
    specialize gaussian_signed_balance_same_code (q)
  5. L75
    specialize gaussian_signed_balance_same_code (m)
  6. L76
    apply gaussian_signed_balance_same_code
  7. L77
    exact hx_witness
  8. L78
    exact hy_witness

Library-wide reading audit

Original defined command ledger · 78 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro pb
  4. 0004intro pc
  5. 0005intro nb
  6. 0006intro nc
  7. 0007intro qb
  8. 0008intro qc
  9. 0009intro mb
  10. 0010intro mc
  11. 0011intro l
  12. 0012intro hF
  13. 0013intro hG
  14. 0014intro hequal
  15. 0015intro i
  16. 0016intro p
  17. 0017intro n
  18. 0018intro q
  19. 0019intro m
  20. 0020intro hi
  21. 0021intro hp
  22. 0022intro hn
  23. 0023intro hq
  24. 0024intro hm
  25. 0025have hx : ∃ x. SignedBalance(x,p,n)
  26. 0026specialize signed_balance_total (p)
  27. 0027specialize signed_balance_total (n)
  28. 0028apply signed_balance_total
  29. 0029cases hx
  30. 0030have hy : ∃ y. SignedBalance(y,q,m)
  31. 0031specialize signed_balance_total (q)
  32. 0032specialize signed_balance_total (m)
  33. 0033apply signed_balance_total
  34. 0034cases hy
  35. 0035have heq : x = x1
  36. 0036specialize hequal (i)
  37. 0037specialize hequal (x)
  38. 0038specialize hequal (x1)
  39. 0039apply hequal
  40. 0040exact hi
  41. 0041specialize divisor_signed_table_at_from_components (F)
  42. 0042specialize divisor_signed_table_at_from_components (pb)
  43. 0043specialize divisor_signed_table_at_from_components (pc)
  44. 0044specialize divisor_signed_table_at_from_components (nb)
  45. 0045specialize divisor_signed_table_at_from_components (nc)
  46. 0046specialize divisor_signed_table_at_from_components (i)
  47. 0047specialize divisor_signed_table_at_from_components (p)
  48. 0048specialize divisor_signed_table_at_from_components (n)
  49. 0049specialize divisor_signed_table_at_from_components (x)
  50. 0050apply divisor_signed_table_at_from_components
  51. 0051exact hF
  52. 0052exact hp
  53. 0053exact hn
  54. 0054exact hx_witness
  55. 0055specialize divisor_signed_table_at_from_components (G)
  56. 0056specialize divisor_signed_table_at_from_components (qb)
  57. 0057specialize divisor_signed_table_at_from_components (qc)
  58. 0058specialize divisor_signed_table_at_from_components (mb)
  59. 0059specialize divisor_signed_table_at_from_components (mc)
  60. 0060specialize divisor_signed_table_at_from_components (i)
  61. 0061specialize divisor_signed_table_at_from_components (q)
  62. 0062specialize divisor_signed_table_at_from_components (m)
  63. 0063specialize divisor_signed_table_at_from_components (x1)
  64. 0064apply divisor_signed_table_at_from_components
  65. 0065exact hG
  66. 0066exact hq
  67. 0067exact hm
  68. 0068exact hy_witness
  69. 0069rewrite heq at hx_witness
  70. 0070rewrite heq at hx_witness
  71. 0071specialize gaussian_signed_balance_same_code (x1)
  72. 0072specialize gaussian_signed_balance_same_code (p)
  73. 0073specialize gaussian_signed_balance_same_code (n)
  74. 0074specialize gaussian_signed_balance_same_code (q)
  75. 0075specialize gaussian_signed_balance_same_code (m)
  76. 0076apply gaussian_signed_balance_same_code
  77. 0077exact hx_witness
  78. 0078exact hy_witness