DV0001

arithmetic_signed_table_component_prefix_preserved

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

Preservation of both actual natural beta prefixes preserves canonical signed values without identifying distinct component representations.

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 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 pfp_i_pvs_preserve_positive pfp_a_pvs_preserve_positive. (exists pfp_gap_pvs_preserve_positivebound. pfp_gap_pvs_preserve_positivebound + S (pfp_i_pvs_preserve_positive) = (l)) -> (((exists ff_h_pfp_pvs_preserve_positiveold. ff_h_pfp_pvs_preserve_positiveold + S (pfp_a_pvs_preserve_positive) = S ((S (pfp_i_pvs_preserve_positive)) * pc)) /\ exists ff_q_pfp_pvs_preserve_positiveold. pb = ff_q_pfp_pvs_preserve_positiveold * S ((S (pfp_i_pvs_preserve_positive)) * pc) + (pfp_a_pvs_preserve_positive))) -> (((exists ff_h_pfp_pvs_preserve_positivenew. ff_h_pfp_pvs_preserve_positivenew + S (pfp_a_pvs_preserve_positive) = S ((S (pfp_i_pvs_preserve_positive)) * qc)) /\ exists ff_q_pfp_pvs_preserve_positivenew. qb = ff_q_pfp_pvs_preserve_positivenew * S ((S (pfp_i_pvs_preserve_positive)) * qc) + (pfp_a_pvs_preserve_positive)))) -> (forall pfp_i_pvs_preserve_negative pfp_a_pvs_preserve_negative. (exists pfp_gap_pvs_preserve_negativebound. pfp_gap_pvs_preserve_negativebound + S (pfp_i_pvs_preserve_negative) = (l)) -> (((exists ff_h_pfp_pvs_preserve_negativeold. ff_h_pfp_pvs_preserve_negativeold + S (pfp_a_pvs_preserve_negative) = S ((S (pfp_i_pvs_preserve_negative)) * nc)) /\ exists ff_q_pfp_pvs_preserve_negativeold. nb = ff_q_pfp_pvs_preserve_negativeold * S ((S (pfp_i_pvs_preserve_negative)) * nc) + (pfp_a_pvs_preserve_negative))) -> (((exists ff_h_pfp_pvs_preserve_negativenew. ff_h_pfp_pvs_preserve_negativenew + S (pfp_a_pvs_preserve_negative) = S ((S (pfp_i_pvs_preserve_negative)) * mc)) /\ exists ff_q_pfp_pvs_preserve_negativenew. mb = ff_q_pfp_pvs_preserve_negativenew * S ((S (pfp_i_pvs_preserve_negative)) * mc) + (pfp_a_pvs_preserve_negative)))) -> (forall dst_index_preserve_result dst_first_preserve_result dst_second_preserve_result. (exists pvs_gap_preserve_resultbound. pvs_gap_preserve_resultbound + S (dst_index_preserve_result) = (l)) -> (exists dst_positive_code_preserve_resultfirst dst_positive_scale_preserve_resultfirst dst_negative_code_preserve_resultfirst dst_negative_scale_preserve_resultfirst dst_positive_preserve_resultfirst dst_negative_preserve_resultfirst. (((F) = (((((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) * S ((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) + ((dst_positive_scale_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst))) + (((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)))) * S ((((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) * S ((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) + ((dst_positive_scale_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst))) + (((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)))) + ((((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst))) + (((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)))))) /\ (((((exists ff_h_pvs_preserve_resultfirstpositive. ff_h_pvs_preserve_resultfirstpositive + S (dst_positive_preserve_resultfirst) = S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultfirst)) /\ exists ff_q_pvs_preserve_resultfirstpositive. dst_positive_code_preserve_resultfirst = ff_q_pvs_preserve_resultfirstpositive * S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultfirst) + (dst_positive_preserve_resultfirst))) /\ (((((exists ff_h_pvs_preserve_resultfirstnegative. ff_h_pvs_preserve_resultfirstnegative + S (dst_negative_preserve_resultfirst) = S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultfirst)) /\ exists ff_q_pvs_preserve_resultfirstnegative. dst_negative_code_preserve_resultfirst = ff_q_pvs_preserve_resultfirstnegative * S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultfirst) + (dst_negative_preserve_resultfirst))) /\ (exists ge_balance_positive_preserve_resultfirstvalue ge_balance_negative_preserve_resultfirstvalue. (((((dst_first_preserve_result) = 2 * (ge_balance_positive_preserve_resultfirstvalue) /\ (ge_balance_negative_preserve_resultfirstvalue) = 0) \/ exists ge_signed_half_preserve_resultfirstvaluedecode. (((dst_first_preserve_result) = 2 * ge_signed_half_preserve_resultfirstvaluedecode + 1 /\ (ge_balance_positive_preserve_resultfirstvalue) = 0) /\ (ge_balance_negative_preserve_resultfirstvalue) = S ge_signed_half_preserve_resultfirstvaluedecode))) /\ ((dst_positive_preserve_resultfirst) + ge_balance_negative_preserve_resultfirstvalue = (dst_negative_preserve_resultfirst) + ge_balance_positive_preserve_resultfirstvalue))))))))) -> (exists dst_positive_code_preserve_resultsecond dst_positive_scale_preserve_resultsecond dst_negative_code_preserve_resultsecond dst_negative_scale_preserve_resultsecond dst_positive_preserve_resultsecond dst_negative_preserve_resultsecond. (((G) = (((((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) * S ((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) + ((dst_positive_scale_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond))) + (((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)))) * S ((((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) * S ((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) + ((dst_positive_scale_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond))) + (((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)))) + ((((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond))) + (((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)))))) /\ (((((exists ff_h_pvs_preserve_resultsecondpositive. ff_h_pvs_preserve_resultsecondpositive + S (dst_positive_preserve_resultsecond) = S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultsecond)) /\ exists ff_q_pvs_preserve_resultsecondpositive. dst_positive_code_preserve_resultsecond = ff_q_pvs_preserve_resultsecondpositive * S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultsecond) + (dst_positive_preserve_resultsecond))) /\ (((((exists ff_h_pvs_preserve_resultsecondnegative. ff_h_pvs_preserve_resultsecondnegative + S (dst_negative_preserve_resultsecond) = S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultsecond)) /\ exists ff_q_pvs_preserve_resultsecondnegative. dst_negative_code_preserve_resultsecond = ff_q_pvs_preserve_resultsecondnegative * S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultsecond) + (dst_negative_preserve_resultsecond))) /\ (exists ge_balance_positive_preserve_resultsecondvalue ge_balance_negative_preserve_resultsecondvalue. (((((dst_second_preserve_result) = 2 * (ge_balance_positive_preserve_resultsecondvalue) /\ (ge_balance_negative_preserve_resultsecondvalue) = 0) \/ exists ge_signed_half_preserve_resultsecondvaluedecode. (((dst_second_preserve_result) = 2 * ge_signed_half_preserve_resultsecondvaluedecode + 1 /\ (ge_balance_positive_preserve_resultsecondvalue) = 0) /\ (ge_balance_negative_preserve_resultsecondvalue) = S ge_signed_half_preserve_resultsecondvaluedecode))) /\ ((dst_positive_preserve_resultsecond) + ge_balance_negative_preserve_resultsecondvalue = (dst_negative_preserve_resultsecond) + ge_balance_positive_preserve_resultsecondvalue))))))))) -> dst_first_preserve_result = dst_second_preserve_result)

Constructive proof overview

Generated structural guide

Preservation of both actual natural beta prefixes preserves canonical signed values without identifying distinct component representations.

The unchanged tactic script uses 3 declared prerequisites and contains 64 exact native proof lines.

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

Proof neighborhood

Direct dependencies

divisor_signed_table_at_to_components Alpha theorem; checked-use authorized divisor_signed_table_at_from_components Alpha theorem; checked-use authorized divisor_signed_table_at_functional Alpha theorem; checked-use authorized

Direct dependents

DV0003 arithmetic_signed_table_extend_at

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

64 script commands · 9 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.

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–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 hp
  5. L15
    intro hn
  6. L16
    intro i
  7. L17
    intro a
  8. L18
    intro b
  9. L19
    intro hi
  10. L20
    intro ha
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hb
04Establish hpartsL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at to components.

  1. L22
    have hparts : ∃ p. ∃ n. BetaAt(pb,pc,i,p) ∧ (BetaAt(nb,nc,i,n) ∧ SignedBalance(a,p,n))Definitions: SignedBalanceBetaAt
  2. L23
    specialize divisor_signed_table_at_to_components (F)
  3. L24
    specialize divisor_signed_table_at_to_components (pb)
  4. L25
    specialize divisor_signed_table_at_to_components (pc)
  5. L26
    specialize divisor_signed_table_at_to_components (nb)
  6. L27
    specialize divisor_signed_table_at_to_components (nc)
  7. L28
    specialize divisor_signed_table_at_to_components (i)
  8. L29
    specialize divisor_signed_table_at_to_components (a)
  9. L30
    apply divisor_signed_table_at_to_components
  10. L31
    exact hF
05Use earlier factsL32–32

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

  1. L32
    exact ha
06Separate the logical casesL33–36

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

  1. L33
    cases hparts
  2. L34
    cases hparts_witness
  3. L35
    cases hparts_witness_witness
  4. L36
    cases hparts_witness_witness_right
07Use earlier factsL37–46

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

  1. L37
    specialize divisor_signed_table_at_functional (G)
  2. L38
    specialize divisor_signed_table_at_functional (i)
  3. L39
    specialize divisor_signed_table_at_functional (a)
  4. L40
    specialize divisor_signed_table_at_functional (b)
  5. L41
    apply divisor_signed_table_at_functional
  6. L42
    specialize divisor_signed_table_at_from_components (G)
  7. L43
    specialize divisor_signed_table_at_from_components (qb)
  8. L44
    specialize divisor_signed_table_at_from_components (qc)
  9. L45
    specialize divisor_signed_table_at_from_components (mb)
  10. L46
    specialize divisor_signed_table_at_from_components (mc)
08Use earlier factsL47–56

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

  1. L47
    specialize divisor_signed_table_at_from_components (i)
  2. L48
    specialize divisor_signed_table_at_from_components (x)
  3. L49
    specialize divisor_signed_table_at_from_components (x1)
  4. L50
    specialize divisor_signed_table_at_from_components (a)
  5. L51
    apply divisor_signed_table_at_from_components
  6. L52
    exact hG
  7. L53
    specialize hp (i)
  8. L54
    specialize hp (x)
  9. L55
    apply hp
  10. L56
    exact hi
09Use earlier factsL57–64

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

  1. L57
    exact hparts_witness_witness_left
  2. L58
    specialize hn (i)
  3. L59
    specialize hn (x1)
  4. L60
    apply hn
  5. L61
    exact hi
  6. L62
    exact hparts_witness_witness_right_left
  7. L63
    exact hparts_witness_witness_right_right
  8. L64
    exact hb

Library-wide reading audit

Original exact command ledger · 64 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 hp
  15. 0015intro hn
  16. 0016intro i
  17. 0017intro a
  18. 0018intro b
  19. 0019intro hi
  20. 0020intro ha
  21. 0021intro hb
  22. 0022have hparts : exists p n. (((((exists ff_h_pvs_preserve_componentspositive. ff_h_pvs_preserve_componentspositive + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_preserve_componentspositive. pb = ff_q_pvs_preserve_componentspositive * S ((S (i)) * pc) + (p))) /\ (((((exists ff_h_pvs_preserve_componentsnegative. ff_h_pvs_preserve_componentsnegative + S (n) = S ((S (i)) * nc)) /\ exists ff_q_pvs_preserve_componentsnegative. nb = ff_q_pvs_preserve_componentsnegative * S ((S (i)) * nc) + (n))) /\ (exists ge_balance_positive_preserve_componentsvalue ge_balance_negative_preserve_componentsvalue. (((((a) = 2 * (ge_balance_positive_preserve_componentsvalue) /\ (ge_balance_negative_preserve_componentsvalue) = 0) \/ exists ge_signed_half_preserve_componentsvaluedecode. (((a) = 2 * ge_signed_half_preserve_componentsvaluedecode + 1 /\ (ge_balance_positive_preserve_componentsvalue) = 0) /\ (ge_balance_negative_preserve_componentsvalue) = S ge_signed_half_preserve_componentsvaluedecode))) /\ ((p) + ge_balance_negative_preserve_componentsvalue = (n) + ge_balance_positive_preserve_componentsvalue)))))))
  23. 0023specialize divisor_signed_table_at_to_components (F)
  24. 0024specialize divisor_signed_table_at_to_components (pb)
  25. 0025specialize divisor_signed_table_at_to_components (pc)
  26. 0026specialize divisor_signed_table_at_to_components (nb)
  27. 0027specialize divisor_signed_table_at_to_components (nc)
  28. 0028specialize divisor_signed_table_at_to_components (i)
  29. 0029specialize divisor_signed_table_at_to_components (a)
  30. 0030apply divisor_signed_table_at_to_components
  31. 0031exact hF
  32. 0032exact ha
  33. 0033cases hparts
  34. 0034cases hparts_witness
  35. 0035cases hparts_witness_witness
  36. 0036cases hparts_witness_witness_right
  37. 0037specialize divisor_signed_table_at_functional (G)
  38. 0038specialize divisor_signed_table_at_functional (i)
  39. 0039specialize divisor_signed_table_at_functional (a)
  40. 0040specialize divisor_signed_table_at_functional (b)
  41. 0041apply divisor_signed_table_at_functional
  42. 0042specialize divisor_signed_table_at_from_components (G)
  43. 0043specialize divisor_signed_table_at_from_components (qb)
  44. 0044specialize divisor_signed_table_at_from_components (qc)
  45. 0045specialize divisor_signed_table_at_from_components (mb)
  46. 0046specialize divisor_signed_table_at_from_components (mc)
  47. 0047specialize divisor_signed_table_at_from_components (i)
  48. 0048specialize divisor_signed_table_at_from_components (x)
  49. 0049specialize divisor_signed_table_at_from_components (x1)
  50. 0050specialize divisor_signed_table_at_from_components (a)
  51. 0051apply divisor_signed_table_at_from_components
  52. 0052exact hG
  53. 0053specialize hp (i)
  54. 0054specialize hp (x)
  55. 0055apply hp
  56. 0056exact hi
  57. 0057exact hparts_witness_witness_left
  58. 0058specialize hn (i)
  59. 0059specialize hn (x1)
  60. 0060apply hn
  61. 0061exact hi
  62. 0062exact hparts_witness_witness_right_left
  63. 0063exact hparts_witness_witness_right_right
  64. 0064exact hb