SS0006

divisor_signed_table_lookup

Every index in the explicitly stated finite domain has an actual canonical signed lookup code.

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

∀ N. ∀ F. ∀ i. ArithTable(N,F) → Le(i,N) → ∃ x. ArithAt(F,i,x)

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

Definition DAG

SignedBalance(z,p,n) · 1ArithTable(N,F) · 1ArithAt(F,i,z) · 1Le(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

divisor_signed_table_at_from_components
Original expanded first-order statement 
forall N F i. (exists dst_positive_code_lookup_table dst_positive_scale_lookup_table dst_negative_code_lookup_table dst_negative_scale_lookup_table. (((F) = (((((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) * S ((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) + ((dst_positive_scale_lookup_table) + (dst_positive_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))) * S ((((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) * S ((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) + ((dst_positive_scale_lookup_table) + (dst_positive_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))) + ((((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))))) /\ (forall dst_index_lookup_table. (exists pvs_le_gap_lookup_tabledomain. pvs_le_gap_lookup_tabledomain + (dst_index_lookup_table) = (N)) -> exists dst_positive_lookup_table dst_negative_lookup_table dst_value_lookup_table. ((((exists ff_h_pvs_lookup_tableentrypositive. ff_h_pvs_lookup_tableentrypositive + S (dst_positive_lookup_table) = S ((S (dst_index_lookup_table)) * dst_positive_scale_lookup_table)) /\ exists ff_q_pvs_lookup_tableentrypositive. dst_positive_code_lookup_table = ff_q_pvs_lookup_tableentrypositive * S ((S (dst_index_lookup_table)) * dst_positive_scale_lookup_table) + (dst_positive_lookup_table))) /\ (((((exists ff_h_pvs_lookup_tableentrynegative. ff_h_pvs_lookup_tableentrynegative + S (dst_negative_lookup_table) = S ((S (dst_index_lookup_table)) * dst_negative_scale_lookup_table)) /\ exists ff_q_pvs_lookup_tableentrynegative. dst_negative_code_lookup_table = ff_q_pvs_lookup_tableentrynegative * S ((S (dst_index_lookup_table)) * dst_negative_scale_lookup_table) + (dst_negative_lookup_table))) /\ (exists ge_balance_positive_lookup_tableentryvalue ge_balance_negative_lookup_tableentryvalue. (((((dst_value_lookup_table) = 2 * (ge_balance_positive_lookup_tableentryvalue) /\ (ge_balance_negative_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_tableentryvaluedecode. (((dst_value_lookup_table) = 2 * ge_signed_half_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_tableentryvalue) = S ge_signed_half_lookup_tableentryvaluedecode))) /\ ((dst_positive_lookup_table) + ge_balance_negative_lookup_tableentryvalue = (dst_negative_lookup_table) + ge_balance_positive_lookup_tableentryvalue))))))))) -> (exists pvs_le_gap_lookup_domain. pvs_le_gap_lookup_domain + (i) = (N)) -> exists z. (exists dst_positive_code_lookup_result dst_positive_scale_lookup_result dst_negative_code_lookup_result dst_negative_scale_lookup_result dst_positive_lookup_result dst_negative_lookup_result. (((F) = (((((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) * S ((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) + ((dst_positive_scale_lookup_result) + (dst_positive_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))) * S ((((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) * S ((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) + ((dst_positive_scale_lookup_result) + (dst_positive_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))) + ((((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))))) /\ (((((exists ff_h_pvs_lookup_resultpositive. ff_h_pvs_lookup_resultpositive + S (dst_positive_lookup_result) = S ((S (i)) * dst_positive_scale_lookup_result)) /\ exists ff_q_pvs_lookup_resultpositive. dst_positive_code_lookup_result = ff_q_pvs_lookup_resultpositive * S ((S (i)) * dst_positive_scale_lookup_result) + (dst_positive_lookup_result))) /\ (((((exists ff_h_pvs_lookup_resultnegative. ff_h_pvs_lookup_resultnegative + S (dst_negative_lookup_result) = S ((S (i)) * dst_negative_scale_lookup_result)) /\ exists ff_q_pvs_lookup_resultnegative. dst_negative_code_lookup_result = ff_q_pvs_lookup_resultnegative * S ((S (i)) * dst_negative_scale_lookup_result) + (dst_negative_lookup_result))) /\ (exists ge_balance_positive_lookup_resultvalue ge_balance_negative_lookup_resultvalue. (((((z) = 2 * (ge_balance_positive_lookup_resultvalue) /\ (ge_balance_negative_lookup_resultvalue) = 0) \/ exists ge_signed_half_lookup_resultvaluedecode. (((z) = 2 * ge_signed_half_lookup_resultvaluedecode + 1 /\ (ge_balance_positive_lookup_resultvalue) = 0) /\ (ge_balance_negative_lookup_resultvalue) = S ge_signed_half_lookup_resultvaluedecode))) /\ ((dst_positive_lookup_result) + ge_balance_negative_lookup_resultvalue = (dst_negative_lookup_result) + ge_balance_positive_lookup_resultvalue)))))))))

Complete tactic proof in conservative notation

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

34 script commands · 7 reading checkpoints · 1 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–5

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro i
  4. L4
    intro ht
  5. L5
    intro hi
02Separate the logical casesL6–10

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

  1. L6
    cases ht
  2. L7
    cases ht_witness
  3. L8
    cases ht_witness_witness
  4. L9
    cases ht_witness_witness_witness
  5. L10
    cases ht_witness_witness_witness_witness
03Establish hvalueL11–14

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

  1. L11
    have hvalue : ∃ p. ∃ n. ∃ z. BetaAt(x,x1,i,p) ∧ (BetaAt(x2,x3,i,n) ∧ SignedBalance(z,p,n))Definitions: BetaAt(x,x1,i,p)BetaAt(x2,x3,i,n)SignedBalance(z,p,n)Original native command in the exact edition
  2. L12
    specialize ht_witness_witness_witness_witness_right (i)
  3. L13
    apply ht_witness_witness_witness_witness_right
  4. L14
    exact hi
04Separate the logical casesL15–19

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

  1. L15
    cases hvalue
  2. L16
    cases hvalue_witness
  3. L17
    cases hvalue_witness_witness
  4. L18
    cases hvalue_witness_witness_witness
  5. L19
    cases hvalue_witness_witness_witness_right
05Construct an explicit witnessL20–20

Supply the displayed value, then prove that it has the required property.

  1. L20
    exists x6
06Use earlier factsL21–30

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

  1. L21
    specialize divisor_signed_table_at_from_components (F)
  2. L22
    specialize divisor_signed_table_at_from_components (x)
  3. L23
    specialize divisor_signed_table_at_from_components (x1)
  4. L24
    specialize divisor_signed_table_at_from_components (x2)
  5. L25
    specialize divisor_signed_table_at_from_components (x3)
  6. L26
    specialize divisor_signed_table_at_from_components (i)
  7. L27
    specialize divisor_signed_table_at_from_components (x4)
  8. L28
    specialize divisor_signed_table_at_from_components (x5)
  9. L29
    specialize divisor_signed_table_at_from_components (x6)
  10. L30
    apply divisor_signed_table_at_from_components
07Use earlier factsL31–34

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

  1. L31
    exact ht_witness_witness_witness_witness_left
  2. L32
    exact hvalue_witness_witness_witness_left
  3. L33
    exact hvalue_witness_witness_witness_right_left
  4. L34
    exact hvalue_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro i
  4. 0004intro ht
  5. 0005intro hi
  6. 0006cases ht
  7. 0007cases ht_witness
  8. 0008cases ht_witness_witness
  9. 0009cases ht_witness_witness_witness
  10. 0010cases ht_witness_witness_witness_witness
  11. 0011have hvalue : ∃ p. ∃ n. ∃ z. BetaAt(x,x1,i,p) ∧ (BetaAt(x2,x3,i,n) ∧ SignedBalance(z,p,n))
  12. 0012specialize ht_witness_witness_witness_witness_right (i)
  13. 0013apply ht_witness_witness_witness_witness_right
  14. 0014exact hi
  15. 0015cases hvalue
  16. 0016cases hvalue_witness
  17. 0017cases hvalue_witness_witness
  18. 0018cases hvalue_witness_witness_witness
  19. 0019cases hvalue_witness_witness_witness_right
  20. 0020exists x6
  21. 0021specialize divisor_signed_table_at_from_components (F)
  22. 0022specialize divisor_signed_table_at_from_components (x)
  23. 0023specialize divisor_signed_table_at_from_components (x1)
  24. 0024specialize divisor_signed_table_at_from_components (x2)
  25. 0025specialize divisor_signed_table_at_from_components (x3)
  26. 0026specialize divisor_signed_table_at_from_components (i)
  27. 0027specialize divisor_signed_table_at_from_components (x4)
  28. 0028specialize divisor_signed_table_at_from_components (x5)
  29. 0029specialize divisor_signed_table_at_from_components (x6)
  30. 0030apply divisor_signed_table_at_from_components
  31. 0031exact ht_witness_witness_witness_witness_left
  32. 0032exact hvalue_witness_witness_witness_left
  33. 0033exact hvalue_witness_witness_witness_right_left
  34. 0034exact hvalue_witness_witness_witness_right_right