SS0003

divisor_signed_table_from_components

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

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. ∀ pb. ∀ pc. ∀ nb. ∀ nc. MatrixMinorFourCode(F,pb,pc,nb,nc) → ArithTable(N,F)

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

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 1SignedBalance(z,p,n) · 1ArithTable(N,F) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

beta_at_exists · checked external prerequisitesigned_balance_total · checked external prerequisite
Original expanded first-order 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)))))))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ p. BetaAt(pb,pc,i,p)Definitions: BetaAt(pb,pc,i,p)Original native command in the exact edition
  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 : ∃ n. BetaAt(nb,nc,i,n)Definitions: BetaAt(nb,nc,i,n)Original native command in the exact edition
  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 : ∃ z. SignedBalance(z,x,x1)Definitions: SignedBalance(z,x,x1)Original native command in the exact edition
  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 defined 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 : ∃ p. BetaAt(pb,pc,i,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 : ∃ n. BetaAt(nb,nc,i,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 : ∃ z. SignedBalance(z,x,x1)
  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