MC0013

signed_table_swapped_components_negation_at

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

Swapping the real positive and negative beta components constructs the exact negated signed lookup, with no canonical-component equality assumption.

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 i a b. ((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) = (((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))) * S ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))) + ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))))) -> (exists dst_positive_code_swapped_source dst_positive_scale_swapped_source dst_negative_code_swapped_source dst_negative_scale_swapped_source dst_positive_swapped_source dst_negative_swapped_source. (((F) = (((((dst_positive_code_swapped_source) + (dst_positive_scale_swapped_source)) * S ((dst_positive_code_swapped_source) + (dst_positive_scale_swapped_source)) + ((dst_positive_scale_swapped_source) + (dst_positive_scale_swapped_source))) + (((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) * S ((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) + ((dst_negative_scale_swapped_source) + (dst_negative_scale_swapped_source)))) * S ((((dst_positive_code_swapped_source) + (dst_positive_scale_swapped_source)) * S ((dst_positive_code_swapped_source) + (dst_positive_scale_swapped_source)) + ((dst_positive_scale_swapped_source) + (dst_positive_scale_swapped_source))) + (((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) * S ((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) + ((dst_negative_scale_swapped_source) + (dst_negative_scale_swapped_source)))) + ((((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) * S ((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) + ((dst_negative_scale_swapped_source) + (dst_negative_scale_swapped_source))) + (((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) * S ((dst_negative_code_swapped_source) + (dst_negative_scale_swapped_source)) + ((dst_negative_scale_swapped_source) + (dst_negative_scale_swapped_source)))))) /\ (((((exists ff_h_pvs_swapped_sourcepositive. ff_h_pvs_swapped_sourcepositive + S (dst_positive_swapped_source) = S ((S (i)) * dst_positive_scale_swapped_source)) /\ exists ff_q_pvs_swapped_sourcepositive. dst_positive_code_swapped_source = ff_q_pvs_swapped_sourcepositive * S ((S (i)) * dst_positive_scale_swapped_source) + (dst_positive_swapped_source))) /\ (((((exists ff_h_pvs_swapped_sourcenegative. ff_h_pvs_swapped_sourcenegative + S (dst_negative_swapped_source) = S ((S (i)) * dst_negative_scale_swapped_source)) /\ exists ff_q_pvs_swapped_sourcenegative. dst_negative_code_swapped_source = ff_q_pvs_swapped_sourcenegative * S ((S (i)) * dst_negative_scale_swapped_source) + (dst_negative_swapped_source))) /\ (exists ge_balance_positive_swapped_sourcevalue ge_balance_negative_swapped_sourcevalue. (((((a) = 2 * (ge_balance_positive_swapped_sourcevalue) /\ (ge_balance_negative_swapped_sourcevalue) = 0) \/ exists ge_signed_half_swapped_sourcevaluedecode. (((a) = 2 * ge_signed_half_swapped_sourcevaluedecode + 1 /\ (ge_balance_positive_swapped_sourcevalue) = 0) /\ (ge_balance_negative_swapped_sourcevalue) = S ge_signed_half_swapped_sourcevaluedecode))) /\ ((dst_positive_swapped_source) + ge_balance_negative_swapped_sourcevalue = (dst_negative_swapped_source) + ge_balance_positive_swapped_sourcevalue))))))))) -> (exists mps_positive_swapped_inverse mps_negative_swapped_inverse. (((((a) = 2 * (mps_positive_swapped_inverse) /\ (mps_negative_swapped_inverse) = 0) \/ exists ge_signed_half_swapped_inversesource. (((a) = 2 * ge_signed_half_swapped_inversesource + 1 /\ (mps_positive_swapped_inverse) = 0) /\ (mps_negative_swapped_inverse) = S ge_signed_half_swapped_inversesource))) /\ ((((b) = 2 * (mps_negative_swapped_inverse) /\ (mps_positive_swapped_inverse) = 0) \/ exists ge_signed_half_swapped_inversetarget. (((b) = 2 * ge_signed_half_swapped_inversetarget + 1 /\ (mps_negative_swapped_inverse) = 0) /\ (mps_positive_swapped_inverse) = S ge_signed_half_swapped_inversetarget))))) -> (exists dst_positive_code_swapped_result dst_positive_scale_swapped_result dst_negative_code_swapped_result dst_negative_scale_swapped_result dst_positive_swapped_result dst_negative_swapped_result. (((G) = (((((dst_positive_code_swapped_result) + (dst_positive_scale_swapped_result)) * S ((dst_positive_code_swapped_result) + (dst_positive_scale_swapped_result)) + ((dst_positive_scale_swapped_result) + (dst_positive_scale_swapped_result))) + (((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) * S ((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) + ((dst_negative_scale_swapped_result) + (dst_negative_scale_swapped_result)))) * S ((((dst_positive_code_swapped_result) + (dst_positive_scale_swapped_result)) * S ((dst_positive_code_swapped_result) + (dst_positive_scale_swapped_result)) + ((dst_positive_scale_swapped_result) + (dst_positive_scale_swapped_result))) + (((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) * S ((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) + ((dst_negative_scale_swapped_result) + (dst_negative_scale_swapped_result)))) + ((((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) * S ((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) + ((dst_negative_scale_swapped_result) + (dst_negative_scale_swapped_result))) + (((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) * S ((dst_negative_code_swapped_result) + (dst_negative_scale_swapped_result)) + ((dst_negative_scale_swapped_result) + (dst_negative_scale_swapped_result)))))) /\ (((((exists ff_h_pvs_swapped_resultpositive. ff_h_pvs_swapped_resultpositive + S (dst_positive_swapped_result) = S ((S (i)) * dst_positive_scale_swapped_result)) /\ exists ff_q_pvs_swapped_resultpositive. dst_positive_code_swapped_result = ff_q_pvs_swapped_resultpositive * S ((S (i)) * dst_positive_scale_swapped_result) + (dst_positive_swapped_result))) /\ (((((exists ff_h_pvs_swapped_resultnegative. ff_h_pvs_swapped_resultnegative + S (dst_negative_swapped_result) = S ((S (i)) * dst_negative_scale_swapped_result)) /\ exists ff_q_pvs_swapped_resultnegative. dst_negative_code_swapped_result = ff_q_pvs_swapped_resultnegative * S ((S (i)) * dst_negative_scale_swapped_result) + (dst_negative_swapped_result))) /\ (exists ge_balance_positive_swapped_resultvalue ge_balance_negative_swapped_resultvalue. (((((b) = 2 * (ge_balance_positive_swapped_resultvalue) /\ (ge_balance_negative_swapped_resultvalue) = 0) \/ exists ge_signed_half_swapped_resultvaluedecode. (((b) = 2 * ge_signed_half_swapped_resultvaluedecode + 1 /\ (ge_balance_positive_swapped_resultvalue) = 0) /\ (ge_balance_negative_swapped_resultvalue) = S ge_signed_half_swapped_resultvaluedecode))) /\ ((dst_positive_swapped_result) + ge_balance_negative_swapped_resultvalue = (dst_negative_swapped_result) + ge_balance_positive_swapped_resultvalue)))))))))

Constructive proof overview

Generated structural guide

Swapping the real positive and negative beta components constructs the exact negated signed lookup, with no canonical-component equality assumption.

The unchanged tactic script uses 3 declared prerequisites and contains 48 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_balance_negate Alpha theorem; checked-use authorized

Direct dependents

MC0014 signed_prefix_sum_pointwise_negate

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

48 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.

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 i
  8. L8
    intro a
  9. L9
    intro b
  10. L10
    intro hF
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hG
  2. L12
    intro ha
  3. L13
    intro hn
03Establish hcL14–23

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. L14
    have hc : ∃ p. ∃ n. BetaAt(pb,pc,i,p) ∧ (BetaAt(nb,nc,i,n) ∧ SignedBalance(a,p,n))Definitions: SignedBalanceBetaAt
  2. L15
    specialize divisor_signed_table_at_to_components (F)
  3. L16
    specialize divisor_signed_table_at_to_components (pb)
  4. L17
    specialize divisor_signed_table_at_to_components (pc)
  5. L18
    specialize divisor_signed_table_at_to_components (nb)
  6. L19
    specialize divisor_signed_table_at_to_components (nc)
  7. L20
    specialize divisor_signed_table_at_to_components (i)
  8. L21
    specialize divisor_signed_table_at_to_components (a)
  9. L22
    apply divisor_signed_table_at_to_components
  10. L23
    exact hF
04Use earlier factsL24–24

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

  1. L24
    exact ha
05Separate the logical casesL25–28

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

  1. L25
    cases hc
  2. L26
    cases hc_witness
  3. L27
    cases hc_witness_witness
  4. L28
    cases hc_witness_witness_right
06Use earlier factsL29–38

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

  1. L29
    specialize divisor_signed_table_at_from_components (G)
  2. L30
    specialize divisor_signed_table_at_from_components (nb)
  3. L31
    specialize divisor_signed_table_at_from_components (nc)
  4. L32
    specialize divisor_signed_table_at_from_components (pb)
  5. L33
    specialize divisor_signed_table_at_from_components (pc)
  6. L34
    specialize divisor_signed_table_at_from_components (i)
  7. L35
    specialize divisor_signed_table_at_from_components (x1)
  8. L36
    specialize divisor_signed_table_at_from_components (x)
  9. L37
    specialize divisor_signed_table_at_from_components (b)
  10. L38
    apply divisor_signed_table_at_from_components
07Use earlier factsL39–48

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

  1. L39
    exact hG
  2. L40
    exact hc_witness_witness_right_left
  3. L41
    exact hc_witness_witness_left
  4. L42
    specialize divisor_signed_balance_negate (a)
  5. L43
    specialize divisor_signed_balance_negate (b)
  6. L44
    specialize divisor_signed_balance_negate (x)
  7. L45
    specialize divisor_signed_balance_negate (x1)
  8. L46
    apply divisor_signed_balance_negate
  9. L47
    exact hc_witness_witness_right_right
  10. L48
    exact hn

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro pb
  4. 0004intro pc
  5. 0005intro nb
  6. 0006intro nc
  7. 0007intro i
  8. 0008intro a
  9. 0009intro b
  10. 0010intro hF
  11. 0011intro hG
  12. 0012intro ha
  13. 0013intro hn
  14. 0014have hc : exists p n. (((((exists ff_h_pvs_swapped_entry_componentspositive. ff_h_pvs_swapped_entry_componentspositive + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_swapped_entry_componentspositive. pb = ff_q_pvs_swapped_entry_componentspositive * S ((S (i)) * pc) + (p))) /\ (((((exists ff_h_pvs_swapped_entry_componentsnegative. ff_h_pvs_swapped_entry_componentsnegative + S (n) = S ((S (i)) * nc)) /\ exists ff_q_pvs_swapped_entry_componentsnegative. nb = ff_q_pvs_swapped_entry_componentsnegative * S ((S (i)) * nc) + (n))) /\ (exists ge_balance_positive_swapped_entry_componentsvalue ge_balance_negative_swapped_entry_componentsvalue. (((((a) = 2 * (ge_balance_positive_swapped_entry_componentsvalue) /\ (ge_balance_negative_swapped_entry_componentsvalue) = 0) \/ exists ge_signed_half_swapped_entry_componentsvaluedecode. (((a) = 2 * ge_signed_half_swapped_entry_componentsvaluedecode + 1 /\ (ge_balance_positive_swapped_entry_componentsvalue) = 0) /\ (ge_balance_negative_swapped_entry_componentsvalue) = S ge_signed_half_swapped_entry_componentsvaluedecode))) /\ ((p) + ge_balance_negative_swapped_entry_componentsvalue = (n) + ge_balance_positive_swapped_entry_componentsvalue)))))))
  15. 0015specialize divisor_signed_table_at_to_components (F)
  16. 0016specialize divisor_signed_table_at_to_components (pb)
  17. 0017specialize divisor_signed_table_at_to_components (pc)
  18. 0018specialize divisor_signed_table_at_to_components (nb)
  19. 0019specialize divisor_signed_table_at_to_components (nc)
  20. 0020specialize divisor_signed_table_at_to_components (i)
  21. 0021specialize divisor_signed_table_at_to_components (a)
  22. 0022apply divisor_signed_table_at_to_components
  23. 0023exact hF
  24. 0024exact ha
  25. 0025cases hc
  26. 0026cases hc_witness
  27. 0027cases hc_witness_witness
  28. 0028cases hc_witness_witness_right
  29. 0029specialize divisor_signed_table_at_from_components (G)
  30. 0030specialize divisor_signed_table_at_from_components (nb)
  31. 0031specialize divisor_signed_table_at_from_components (nc)
  32. 0032specialize divisor_signed_table_at_from_components (pb)
  33. 0033specialize divisor_signed_table_at_from_components (pc)
  34. 0034specialize divisor_signed_table_at_from_components (i)
  35. 0035specialize divisor_signed_table_at_from_components (x1)
  36. 0036specialize divisor_signed_table_at_from_components (x)
  37. 0037specialize divisor_signed_table_at_from_components (b)
  38. 0038apply divisor_signed_table_at_from_components
  39. 0039exact hG
  40. 0040exact hc_witness_witness_right_left
  41. 0041exact hc_witness_witness_left
  42. 0042specialize divisor_signed_balance_negate (a)
  43. 0043specialize divisor_signed_balance_negate (b)
  44. 0044specialize divisor_signed_balance_negate (x)
  45. 0045specialize divisor_signed_balance_negate (x1)
  46. 0046apply divisor_signed_balance_negate
  47. 0047exact hc_witness_witness_right_right
  48. 0048exact hn