SS0006

divisor_signed_table_lookup

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

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

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 expanded first-order arithmetic 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)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 34 exact native proof lines.

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

Proof neighborhood

Direct dependencies

SS0001 divisor_signed_table_at_from_components

Direct dependents

SS0018 divisor_signed_table_lookup_from_components

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

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.

Named ingredients (1)
divisor signed table at from components

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: SignedBalanceBetaAt
  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 exact 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 : exists p n z. (((((exists ff_h_pvs_lookup_valuepositive. ff_h_pvs_lookup_valuepositive + S (p) = S ((S (i)) * x1)) /\ exists ff_q_pvs_lookup_valuepositive. x = ff_q_pvs_lookup_valuepositive * S ((S (i)) * x1) + (p))) /\ (((((exists ff_h_pvs_lookup_valuenegative. ff_h_pvs_lookup_valuenegative + S (n) = S ((S (i)) * x3)) /\ exists ff_q_pvs_lookup_valuenegative. x2 = ff_q_pvs_lookup_valuenegative * S ((S (i)) * x3) + (n))) /\ (exists ge_balance_positive_lookup_valuevalue ge_balance_negative_lookup_valuevalue. (((((z) = 2 * (ge_balance_positive_lookup_valuevalue) /\ (ge_balance_negative_lookup_valuevalue) = 0) \/ exists ge_signed_half_lookup_valuevaluedecode. (((z) = 2 * ge_signed_half_lookup_valuevaluedecode + 1 /\ (ge_balance_positive_lookup_valuevalue) = 0) /\ (ge_balance_negative_lookup_valuevalue) = S ge_signed_half_lookup_valuevaluedecode))) /\ ((p) + ge_balance_negative_lookup_valuevalue = (n) + ge_balance_positive_lookup_valuevalue)))))))
  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