MC0013

signed_table_swapped_components_negation_at

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

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.

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ i. ∀ a. ∀ b. MatrixMinorFourCode(F,pb,pc,nb,nc) → MatrixMinorFourCode(G,nb,nc,pb,pc) → ArithAt(F,i,a) → SignedNegate(a,b) → ArithAt(G,i,b)

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

Definition DAG

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

Actual proof prerequisites

divisor_signed_table_at_to_components · checked external prerequisitedivisor_signed_table_at_from_components · checked external prerequisitedivisor_signed_balance_negate · checked external prerequisite
Original expanded first-order 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)))))))))

Complete tactic proof in conservative notation

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

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.

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