SS0003

divisor_signed_table_from_components

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

Every actual pair of beta component streams gives canonical signed entries on every requested finite domain, including the zero endpoint.

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 pb pc nb nc. ((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)))))) -> (exists dst_positive_code_constructor_table dst_positive_scale_constructor_table dst_negative_code_constructor_table dst_negative_scale_constructor_table. (((F) = (((((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) * S ((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) + ((dst_positive_scale_constructor_table) + (dst_positive_scale_constructor_table))) + (((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table)))) * S ((((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) * S ((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) + ((dst_positive_scale_constructor_table) + (dst_positive_scale_constructor_table))) + (((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table)))) + ((((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table))) + (((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table)))))) /\ (forall dst_index_constructor_table. (exists pvs_le_gap_constructor_tabledomain. pvs_le_gap_constructor_tabledomain + (dst_index_constructor_table) = (N)) -> exists dst_positive_constructor_table dst_negative_constructor_table dst_value_constructor_table. ((((exists ff_h_pvs_constructor_tableentrypositive. ff_h_pvs_constructor_tableentrypositive + S (dst_positive_constructor_table) = S ((S (dst_index_constructor_table)) * dst_positive_scale_constructor_table)) /\ exists ff_q_pvs_constructor_tableentrypositive. dst_positive_code_constructor_table = ff_q_pvs_constructor_tableentrypositive * S ((S (dst_index_constructor_table)) * dst_positive_scale_constructor_table) + (dst_positive_constructor_table))) /\ (((((exists ff_h_pvs_constructor_tableentrynegative. ff_h_pvs_constructor_tableentrynegative + S (dst_negative_constructor_table) = S ((S (dst_index_constructor_table)) * dst_negative_scale_constructor_table)) /\ exists ff_q_pvs_constructor_tableentrynegative. dst_negative_code_constructor_table = ff_q_pvs_constructor_tableentrynegative * S ((S (dst_index_constructor_table)) * dst_negative_scale_constructor_table) + (dst_negative_constructor_table))) /\ (exists ge_balance_positive_constructor_tableentryvalue ge_balance_negative_constructor_tableentryvalue. (((((dst_value_constructor_table) = 2 * (ge_balance_positive_constructor_tableentryvalue) /\ (ge_balance_negative_constructor_tableentryvalue) = 0) \/ exists ge_signed_half_constructor_tableentryvaluedecode. (((dst_value_constructor_table) = 2 * ge_signed_half_constructor_tableentryvaluedecode + 1 /\ (ge_balance_positive_constructor_tableentryvalue) = 0) /\ (ge_balance_negative_constructor_tableentryvalue) = S ge_signed_half_constructor_tableentryvaluedecode))) /\ ((dst_positive_constructor_table) + ge_balance_negative_constructor_tableentryvalue = (dst_negative_constructor_table) + ge_balance_positive_constructor_tableentryvalue)))))))))

Constructive proof overview

Generated structural guide

Every actual pair of beta component streams gives canonical signed entries on every requested finite domain, including the zero endpoint.

The unchanged tactic script uses 2 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized signed_balance_total Alpha theorem; checked-use authorized

Direct dependents

SS0004 divisor_signed_table_construct SS0008 divisor_signed_table_restrict SS0018 divisor_signed_table_lookup_from_components SS001B divisor_signed_table_reindex_exists

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

40 script commands · 16 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.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro pb
  4. L4
    intro pc
  5. L5
    intro nb
  6. L6
    intro nc
  7. L7
    intro hrep
02Construct an explicit witnessL8–11

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

  1. L8
    exists pb
  2. L9
    exists pc
  3. L10
    exists nb
  4. L11
    exists nc
03Separate the logical casesL12–12

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

  1. L12
    split
04Use earlier factsL13–13

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

  1. L13
    exact hrep
05Fix variables and assumptionsL14–15

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

  1. L14
    intro i
  2. L15
    intro hbound
06Establish hpL16–20

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

  1. L16
    have hp : exists p. (((exists ff_h_pvs_constructor_positive. ff_h_pvs_constructor_positive + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_constructor_positive. pb = ff_q_pvs_constructor_positive * S ((S (i)) * pc) + (p)))
  2. L17
    specialize beta_at_exists (pb)
  3. L18
    specialize beta_at_exists (pc)
  4. L19
    specialize beta_at_exists (i)
  5. L20
    apply beta_at_exists
07Separate the logical casesL21–21

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

  1. L21
    cases hp
08Establish hnL22–26

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

  1. L22
    have hn : exists n. (((exists ff_h_pvs_constructor_negative. ff_h_pvs_constructor_negative + S (n) = S ((S (i)) * nc)) /\ exists ff_q_pvs_constructor_negative. nb = ff_q_pvs_constructor_negative * S ((S (i)) * nc) + (n)))
  2. L23
    specialize beta_at_exists (nb)
  3. L24
    specialize beta_at_exists (nc)
  4. L25
    specialize beta_at_exists (i)
  5. L26
    apply beta_at_exists
09Separate the logical casesL27–27

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

  1. L27
    cases hn
10Establish hzL28–31

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

  1. L28
    have hz : exists z. (exists ge_balance_positive_constructor_balance ge_balance_negative_constructor_balance. (((((z) = 2 * (ge_balance_positive_constructor_balance) /\ (ge_balance_negative_constructor_balance) = 0) \/ exists ge_signed_half_constructor_balancedecode. (((z) = 2 * ge_signed_half_constructor_balancedecode + 1 /\ (ge_balance_positive_constructor_balance) = 0) /\ (ge_balance_negative_constructor_balance) = S ge_signed_half_constructor_balancedecode))) /\ ((x) + ge_balance_negative_constructor_balance = (x1) + ge_balance_positive_constructor_balance)))
  2. L29
    specialize signed_balance_total (x)
  3. L30
    specialize signed_balance_total (x1)
  4. L31
    apply signed_balance_total
11Separate the logical casesL32–32

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

  1. L32
    cases hz
12Construct an explicit witnessL33–35

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

  1. L33
    exists x
  2. L34
    exists x1
  3. L35
    exists x2
13Separate the logical casesL36–36

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

  1. L36
    split
14Use earlier factsL37–37

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

  1. L37
    exact hp_witness
15Separate the logical casesL38–38

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

  1. L38
    split
16Use earlier factsL39–40

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

  1. L39
    exact hn_witness
  2. L40
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro pb
  4. 0004intro pc
  5. 0005intro nb
  6. 0006intro nc
  7. 0007intro hrep
  8. 0008exists pb
  9. 0009exists pc
  10. 0010exists nb
  11. 0011exists nc
  12. 0012split
  13. 0013exact hrep
  14. 0014intro i
  15. 0015intro hbound
  16. 0016have hp : exists p. (((exists ff_h_pvs_constructor_positive. ff_h_pvs_constructor_positive + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_constructor_positive. pb = ff_q_pvs_constructor_positive * S ((S (i)) * pc) + (p)))
  17. 0017specialize beta_at_exists (pb)
  18. 0018specialize beta_at_exists (pc)
  19. 0019specialize beta_at_exists (i)
  20. 0020apply beta_at_exists
  21. 0021cases hp
  22. 0022have hn : exists n. (((exists ff_h_pvs_constructor_negative. ff_h_pvs_constructor_negative + S (n) = S ((S (i)) * nc)) /\ exists ff_q_pvs_constructor_negative. nb = ff_q_pvs_constructor_negative * S ((S (i)) * nc) + (n)))
  23. 0023specialize beta_at_exists (nb)
  24. 0024specialize beta_at_exists (nc)
  25. 0025specialize beta_at_exists (i)
  26. 0026apply beta_at_exists
  27. 0027cases hn
  28. 0028have hz : exists z. (exists ge_balance_positive_constructor_balance ge_balance_negative_constructor_balance. (((((z) = 2 * (ge_balance_positive_constructor_balance) /\ (ge_balance_negative_constructor_balance) = 0) \/ exists ge_signed_half_constructor_balancedecode. (((z) = 2 * ge_signed_half_constructor_balancedecode + 1 /\ (ge_balance_positive_constructor_balance) = 0) /\ (ge_balance_negative_constructor_balance) = S ge_signed_half_constructor_balancedecode))) /\ ((x) + ge_balance_negative_constructor_balance = (x1) + ge_balance_positive_constructor_balance)))
  29. 0029specialize signed_balance_total (x)
  30. 0030specialize signed_balance_total (x1)
  31. 0031apply signed_balance_total
  32. 0032cases hz
  33. 0033exists x
  34. 0034exists x1
  35. 0035exists x2
  36. 0036split
  37. 0037exact hp_witness
  38. 0038split
  39. 0039exact hn_witness
  40. 0040exact hz_witness