text:
Let's suppose a creditor (open account) obtains a judgement before the SOL runs. Is there any limit to how many years the creditor may attempt to collect on the judgement?

Also, with the judgement in hand, can the creditor place a lien on an inheritance?

Thank you.

format: plain


text:
# (-a) × (-a) = a × a

We all know that $$\(-a) \times (-a) = a \times a\$$ (hopefully), but can you prove it?

Your task is to prove this fact using the ring axioms. What are the ring axioms? The ring axioms are a list of rules that two binary operations on a set have to follow. The two operation are addition, $$\+\$$, and multiplication, $$\\times\$$. For this challenge here are the ring axioms where $$\+\$$ and $$\\times\$$ are closed binary operations on some set $$\S\$$, $$\-\$$ is a closed unary operation on $$\S\$$, and $$\a\$$, $$\b\$$, $$\c\$$ are members of $$\S\$$:

1. $$\a + (b + c) = (a + b) + c\$$

2. $$\a + 0 = a\$$

3. $$\a + (-a) = 0\$$

4. $$\a + b = b + a\$$*

5. $$\a \times (b \times c) = (a \times b) \times c\$$

6. $$\a \times 1 = a\$$

7. $$\1 × a = a\$$

8. $$\a \times (b + c) = (a \times b) + (a × c)\$$

9. $$\(b + c) \times a = (b \times a) + (c \times a)\$$

Your proof should be a string of equalities each being the application of one axiom.

You may apply the axioms to either the entire expression or to some sub-expression. For example if we have $$\(a + c) + (b + c)\$$ we can apply Axiom 4 to just the $$\(b + c)\$$ term, the $$\(a + c)\$$ term or the entire expression as a whole. The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to $$\((a \times c) + b) + ((-a) + 1)\$$ to get $$\((-a) + 1) + ((a \times c) + b)\$$. In each step of the proof you can only apply one axiom to one expression. All axioms are bidirectional, meaning substitution can go in either direction. Things like the following are not allowed

(a + b) + (c + d) = (a + (b + c)) + d Ax. 1

This should be done in two steps:

(a + b) + (c + d) = ((a + b) + c) + d Ax. 1
= (a + (b + c)) + d Ax. 1

Facts you might normally take for granted but are not listed on the axioms list cannot be assumed, for example $$\(-a) = (-1) \times a\$$ is true but requires multiple steps to preform.

User Anthony has kindly provided a online proof validator that can be used as a replacement for TIO.

## Example proof

Here is an example proof that $$\-(-a) = a\$$ with the axioms used labeled on the right of each step.

 -(-a) = (-(-a)) + 0          Ax. 2
= 0 + (-(-a))          Ax. 4
= (a + (-a)) + (-(-a)) Ax. 3
= a + ((-a) + (-(-a))) Ax. 1
= a + 0                Ax. 3
= a                    Ax. 2

Try it online!

You will be tasked to prove $$\(-a) \times (-a) = a \times a\$$ using successive substitution like that shown above.

## Scoring

This is so your answers will be scored in number of steps taken to get from $$\(-a) \times (-a)\$$ to $$\a \times a\$$, with a lower score being better.

### Lemmas

Some answers have chosen to use Lemmas in their proofs, so I will describe how that should be scored to avoid any confusion. For the uninitiated, lemmas are proofs of facts that you use later in the proof. In real mathematics they can be helpful in organizing your thoughts or conveying information clearly to the reader. In this challenge using lemmas should not have an direct effect on your score. (Although proof organization may make it easier or harder to golf)

If you choose to use lemmas it will cost as many steps as it took to prove that lemma in the first place each time you use it. For example the here is the score breakdown of a proof using lemmas.

Lemma:
a × 0 = 0

Proof (7 steps):
a × 0 = (a × 0) + 0                        Ax. 2 (1)
= (a × 0) + ((a × b) + (-(a × b)))   Ax. 3 (1)
= ((a × 0) + (a × b)) + (-(a × b))   Ax. 1 (1)
= (a × (0 + b)) + (-(a × b))         Ax. 8 (1)
= (a × (b + 0)) + (-(a × b))         Ax. 4 (1)
= (a × b) + (-(a × b))               Ax. 2 (1)
= 0                                  Ax. 3 (1)

Theorem:
(a × 0) + (b × 0) = 0

Proof (15 steps):
(a × 0) + (b × 0) = 0 + (b × 0)  Lemma (7)
= (b × 0) + 0  Ax. 4 (1)
= b × 0        Ax. 2 (1)
= 0            Lemma (7)

*: It has been pointed out that this axiom is not strictly necessary to prove this property, however you are still allowed to use it.

†: Since $$\1\$$ does not appear in the desired equality any proof that uses these axioms is not minimal. That is these axioms cannot help with proving the desired fact. They have been included just for the sake of completeness.

• Is a program we write supposed to solve this, or just print the answer?
– Tahg
Sep 26 '17 at 22:42
• @Tahg You're supposed to prove it and submit your proof as an answer. This is different from most (if not all) problems you will see here. Sep 26 '17 at 22:44
• I got frustratingly close before I realized that a*0=0 isn't in the list of axioms. Sep 26 '17 at 22:48
• Erm... I might be wrong but isn't this way off-topic? Shouldn't answers contain code? Sep 27 '17 at 1:25
• @icrieverytim if it helps, think of the axiom list as a programming language with nine built-in parameter substitution functions, and this is a code golf for a function that turns a specific input into a specific output. Sep 27 '17 at 1:33

## 18 Steps

(-a)*(-a) = ((-a)*(-a))+0                                             Axiom 2
= ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))        Axiom 3
= (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
= (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a))))        Axiom 4
= ((a*a)+((a*(-a))+((-a)*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
= ((a*a)+((a+(-a))*(-a)))+(-((a*a)+(a*(-a))))               Axiom 9
= ((a*a)+(0*(-a)))+(-((a*a)+(a*(-a))))                      Axiom 3
= ((a*(a+0))+(0*(-a)))+(-((a*a)+(a*(-a))))                  Axiom 2
= ((a*(a+(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))           Axiom 3
= (((a*a)+(a*(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))       Axiom 8
= ((a*a)+((a*(a+(-a)))+(0*(-a))))+(-((a*a)+(a*(-a))))       Axiom 1
= (a*a)+(((a*(a+(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))       Axiom 1
= (a*a)+((((a*a)+(a*(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))   Axiom 8
= (a*a)+(((a*a)+((a*(-a))+(0*(-a))))+(-((a*a)+(a*(-a)))))   Axiom 1
= (a*a)+(((a*a)+((a+0)*(-a)))+(-((a*a)+(a*(-a)))))          Axiom 9
= (a*a)+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))              Axiom 2
= (a*a)+0                                                   Axiom 3
= a*a                                                       Axiom 2

I wrote a program to check my solution. So if you find an error in this, then my program is wrong too.

• @Etoplay Just out of curiosity, did you write your program in Prolog? Sep 27 '17 at 23:49
• It would be great if you could include your program. It could certainly help verify other solutions. Sep 28 '17 at 4:20
• How did you get from the first line to the second just by applying one axiom one time? Sep 28 '17 at 8:15
• @SztupY Axiom 3 is v + (-v) = 0 let v = ((a*a)+(a*(-a)) and you get there in 1 step.
– MT0
Sep 28 '17 at 11:42
• validated Oct 18 '17 at 10:43

## 18 steps

Different from the already posted 18-step solution.

a*a = a*a + 0                                                 A2
= a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))        A3
= (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))        A1
= (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a)))          A8
= a*(a + ((-a) + (-a))) + (-(a*(-a) + a*(-a)))            A8
= a*((a + (-a)) + (-a)) + (-(a*(-a) + a*(-a)))            A1
= a*(0 + (-a)) + (-(a*(-a) + a*(-a)))                     A3
= a*((-a) + 0) + (-(a*(-a) + a*(-a)))                     A4
= a*(-a) + (-(a*(-a) + a*(-a)))                           A2
= (a + 0)*(-a) + (-(a*(-a) + a*(-a)))                     A2
= (a + (a + (-a)))*(-a) + (-(a*(-a) + a*(-a)))            A3
= ((a + a) + (-a))*(-a) + (-(a*(-a) + a*(-a)))            A1
= ((-a) + (a + a))*(-a) + (-(a*(-a) + a*(-a)))            A4
= ((-a)*(-a) + (a + a)*(-a)) + (-(a*(-a) + a*(-a)))       A9
= ((-a)*(-a) + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))  A9
= (-a)*(-a) + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))  A1
= (-a)*(-a) + 0                                           A3
= (-a)*(-a)                                               A2

• Interesting to see someone do it backwards. All the steps are reversible so this is a fine proof. Sep 29 '17 at 13:22
• That it goes upside down is mostly accidental. The proof is actually fairly symmetric: I use two similar sequences of steps to get from either end to the middle term a*(-a) + stuff. Sep 29 '17 at 13:27
• validated Oct 18 '17 at 18:57

# 29 26 Steps

No lemmas!

Comment if you see anything wrong. (It's very easy to make a mistake)

(-a) × (-a) = ((-a) + 0) × (-a)                                                  Ax. 2
= ((-a) + (a + (-a))) × (-a)                                         Ax. 3
= ((a + (-a)) + (-a)) × (-a)                                         Ax. 4
= (a + ((-a) + (-a))) × (-a)                                         Ax. 1
= (a × (-a)) + (((-a) + (-a)) × (-a))                                Ax. 9
= (a × ((-a) + 0)) + (((-a) + (-a)) × (-a))                          Ax. 2
= (a × ((-a) + (a + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 3
= (a × ((a + (-a)) + (-a))) + (((-a) + (-a)) × (-a))                 Ax. 4
= (a × (a + ((-a) + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 1
= ((a × a) + (a × ((-a) + (-a)))) + (((-a) + (-a)) × (-a))           Ax. 8
= (a × a) + ((a × ((-a) + (-a))) + (((-a) + (-a)) × (-a)))           Ax. 1
= (a × a) + (((a × (-a)) + (a × (-a))) + (((-a) + (-a)) × (-a)))     Ax. 8
= (a × a) + (((a + a) × (-a)) + (((-a) + (-a)) × (-a)))              Ax. 9
= (a × a) + (((a + a) + ((-a) + (-a))) × (-a))                       Ax. 9
= (a × a) + ((((a + a) + (-a)) + (-a)) × (-a))                       Ax. 1
= (a × a) + (((a + (a + (-a))) + (-a)) × (-a))                       Ax. 1
= (a × a) + (((a + 0) + (-a)) × (-a))                                Ax. 3
= (a × a) + ((a + (-a)) × (-a))                                      Ax. 2
= (a × a) + (0 × (-a))                                               Ax. 3
= (a × a) + ((0 × (-a)) + 0)                                         Ax. 2
= (a × a) + ((0 × (-a)) + ((0 × (-a)) + (-(0 × (-a)))))              Ax. 3
= (a × a) + (((0 × (-a)) + (0 × (-a))) + (-(0 × (-a))))              Ax. 1
= (a × a) + (((0 + 0) × (-a)) + (-(0 × (-a))))                       Ax. 9
= (a × a) + ((0 × (-a)) + (-(0 × (-a))))                             Ax. 2
= (a × a) + 0                                                        Ax. 3
= (a × a)                                                            Ax. 2

Credit goes to Maltysen for 0 × (-a) = 0

• validated Oct 18 '17 at 10:45

# 18 steps

Not the first 18-step proof, but it’s simpler than the others.

(-a)*(-a)
= (-a)*(-a) + 0                             [Axiom 2]
= (-a)*(-a) + ((-a)*a + -((-a)*a))          [Axiom 3]
= ((-a)*(-a) + (-a)*a) + -((-a)*a)          [Axiom 1]
= ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a)    [Axiom 2]
= ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a)  [Axiom 9]
= (((-a)*(-a) + (-a)*a) + 0*a) + -((-a)*a)  [Axiom 1]
= ((-a)*((-a) + a) + 0*a) + -((-a)*a)       [Axiom 8]
= ((-a)*(a + (-a)) + 0*a) + -((-a)*a)       [Axiom 4]
= ((-a)*0 + 0*a) + -((-a)*a)                [Axiom 3]
= (0*a + (-a)*0) + -((-a)*a)                [Axiom 4]
= ((a + (-a))*a + (-a)*0) + -((-a)*a)       [Axiom 3]
= ((a*a + (-a)*a) + (-a)*0) + -((-a)*a)     [Axiom 9]
= (a*a + ((-a)*a + (-a)*0)) + -((-a)*a)     [Axiom 1]
= (a*a + (-a)*(a + 0)) + -((-a)*a)          [Axiom 8]
= (a*a + (-a)*a) + -((-a)*a)                [Axiom 2]
= a*a + ((-a)*a + -((-a)*a))                [Axiom 1]
= a*a + 0                                   [Axiom 3]
= a*a                                       [Axiom 2]

Validate

# 23 steps

(-a) * (-a) = ((-a) * (-a)) + 0                                 ✔ axiom 2
= ((-a) * (-a)) + (((-a) * a) + -((-a) * a))        ✔ axiom 3
= (((-a) * (-a)) + (-a) * a) + -((-a) * a)          ✔ axiom 1
= (-a) * (-a + a) + -((-a) * a)                     ✔ axiom 8
= (-a) * (a + (-a)) + -((-a) * a)                   ✔ axiom 4
= ((-a) * 0) + -((-a) * a)                          ✔ axiom 3
= (((-a) * 0) + 0) + -((-a) * a)                    ✔ axiom 2
= ((-a) * 0 + ((-a)*0 + -((-a)*0))) + -((-a) * a)   ✔ axiom 3
= (((-a) * 0 + (-a)*0) + -((-a)*0)) + -((-a) * a)   ✔ axiom 1
= ((-a) * (0 + 0) + -((-a)*0)) + -((-a) * a)        ✔ axiom 8
= ((-a) * 0 + -((-a)*0)) + -((-a) * a)              ✔ axiom 2
= 0 + -((-a) * a)                                   ✔ axiom 3
= (0* a) + -(0*a) + -((-a) * a)                     ✔ axiom 3
= ((0+0)* a) + -(0*a) + -((-a) * a)                 ✔ axiom 2
= ((0 * a ) + (0*a) + -(0*a)) + -((-a) * a)         ✔ axiom 9
= ((0 * a ) + ((0*a) + -(0*a))) + -((-a) * a)       ✔ axiom 1
= ((0 * a ) + 0) + -((-a) * a)                      ✔ axiom 3
= (0 * a ) + -((-a) * a)                            ✔ axiom 2
= ((a + -a) * a ) + -((-a) * a)                     ✔ axiom 3
= ((a * a) + (-a) * a) + -((-a) * a)                ✔ axiom 9
= (a * a) + (((-a) * a) + -((-a) * a))              ✔ axiom 1
= (a * a) + 0                                       ✔ axiom 3
= a * a                                             ✔ axiom 2

Try it online!

Yes you read that right, I've written a proof-checker for this puzzle (naturally there's a possibility that the checker itself is wrong)

• Here’s a modest reward for the proof checker. May 23 '20 at 12:24
• @EmilJeřábek wow, thank you! Yeah, interesting trick with parse trees that, and not too painful to implement. I have enjoyed playing a little with a fully general prover (Metamath) since. May 30 '20 at 16:35
A2: (-a) x (-a) = ((-a) + 0) x (-a)
A3:             = ((-a) + (a + (-a))) x (-a)
A9:             = ((-a) x (-a)) + ((a + (-a)) x (-a))
A4:             = ((-a) x (-a)) + (((-a) + a) x (-a))
A9:             = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a))
A2:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + 0))
A3:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + (a x (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x a) + (a x (-a))))
A4:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x (-a)) + (a x a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + ((a x ((-a) + (-a))) + (a x a))
A1:             = (((-a) x ((-a) + (-a))) + (a x ((-a) + (-a)))) + (a x a)
A9:             = (((-a) + a) x ((-a) + (-a))) + (a x a)
A4:             = ((a + (-a)) x ((-a) + (-a))) + (a x a)
Lemma:          = (0 x ((-a) + (-a))) + (a x a)
A3:             = 0 + (a x a)
A4:             = (a x a) + 0
A2:             = (a x a)

Lemma: 0 = 0 x a

A3: 0 = (0 x a) + (-(0 x a))
A2:   = ((0 + 0) x a) + (-(0 x a))
A9:   = ((0 x a) + (0 x a)) + (-(0 x a))
A1:   = (0 x a) + ((0 x a) + (-(0 x a)))
A3:   = (0 x a) + 0
A2:   = (0 x a)

27 26 steps Thank you Funky Computer Man for noticing a duplicate line.

• Welcome to the site! I'm not sure why you create a lemma only to use it once but I suppose its not against the rules. Sep 27 '17 at 4:30
• @FunkyComputerMan Thank you! You're right; I'm not sure what I was thinking when I wrote that lemma ^^. And thank you for your edit and your remark. Sep 27 '17 at 5:11
• @JalilCompaoré I think you might be able to save that last A3 by starting by applying A2 to the second (-a) rather than the first. I'm not sure though, as I don't have the time to work through it right now. Sep 27 '17 at 7:38

# 6 + 7 + 7 + 6 + 3 = 29 steps

Lemma 1. a*0=0 (6 steps)

0 = a*0 + -(a*0)  axiom 3
= a*(0+0) + -(a*0) axiom 2
= (a*0 + a*0) + -(a*0) axiom 8
= a*0 + (a*0 + -(a*0)) axiom 1
= a*0 + 0 axiom 3
= a*0 axiom 2

Lemma 2. a*(-b) = -(a*b) (7 steps)

a*(-b) = a*(-b) + 0 axiom 2
= a*(-b) + (a*b + -(a*b)) axiom 3
= (a*(-b) + a*b) + -(a*b) axiom 1
= a*(-b+b) + -(a*b) axiom 8
= a*0 + -(a*b) axiom 3
= 0 + -(a*b) lemma 1
= -(a*b) axiom 2

Lemma 3. (-a)*b = -(a*b) (7 steps)
same as above

Lemma 4. -(-(a)) = a (6 steps)

-(-a) = (-(-a)) + 0    axiom 2
= 0 + (-(-a))          axiom 4
= (a + (-a)) + (-(-a)) axiom 3
= a + ((-a) + (-(-a))) axiom 1
= a + 0                axiom 3
= a                    axiom 2

Theorem. -a*-a=0 (3 steps)

-a*-a = -(a*(-a)) lemma 3
= -(-(a*a)) lemma 2
= a*a lemma 4

Q.E.D.

• I don't think you can make lemmas though Sep 26 '17 at 23:37
• "Theorem. -a*-a=0" should be =a*a ? Sep 27 '17 at 0:39
• @H.PWiz I don't have a problem with people using lemmas, but they cost as many steps as they are long each time they are used. I would recommend against using them because they can get in the way of optimizations, but as far as I'm concerned this post is fine. Sep 27 '17 at 2:14
• going from "0 + -(a*b)" to "-(a*b)" in a single application of axiom 2 is not right. you need to use axiom 4 to swap the sides of the + first. Sep 27 '17 at 6:20
• The way I read it is lemma 2/3 are 6 steps plus an instance of lemma 1 for 12 steps, lemma 4 is 6 steps, for a total of 30 steps. Am I missing something here?
– Tahg
Sep 29 '17 at 13:27

# 304 steps

Community wiki because this proof is generated by Mathematica's FindEquationalProof function.

The proof is rather long. Mathematica doesn't know how to golf it.

This is the Mathematica code that generates the proof (requires Mathematica 11.3), where p, t, n means +, ×, - respectively:

ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
ForAll[a, p[a, 0] == a],
ForAll[a, p[a, n[a]] == 0],
ForAll[{a, b}, p[a, b] == p[b, a]],
ForAll[{a, b, c}, t[a, t[b, c]] == t[t[a, b], c]],
ForAll[a, t[a, 1] == a], ForAll[a, t[1, a] == a],
ForAll[{a, b, c}, t[a, p[b, c]] == p[t[a, b], t[a, c]]],
ForAll[{a, b, c}, t[p[b, c], a] == p[t[b, a], t[c, a]]]};

proof = FindEquationalProof[t[n[a], n[a]] == t[a, a], ringAxioms];

proof["ProofNotebook"]

It is not easy to count the steps directly, so I calculate it by the number of paths from the axioms to the conclusion in the "proof graph".

graph = proof["ProofGraph"];
score = Sum[
Length[FindPath[graph, axiom, "Conclusion 1", Infinity,
All]], {axiom,
Select[VertexList[graph], StringMatchQ["Axiom " ~~ __]]}]

Try it online!

This is the proof generated by the code:

Axiom 1

We are given that:

x1==p[x1, 0]

Axiom 2

We are given that:

x1==t[x1, 1]

Axiom 3

We are given that:

x1==t[1, x1]

Axiom 4

We are given that:

p[x1, x2]==p[x2, x1]

Axiom 5

We are given that:

p[x1, p[x2, x3]]==p[p[x1, x2], x3]

Axiom 6

We are given that:

p[x1, n[x1]]==0

Axiom 7

We are given that:

p[t[x1, x2], t[x3, x2]]==t[p[x1, x3], x2]

Axiom 8

We are given that:

p[t[x1, x2], t[x1, x3]]==t[x1, p[x2, x3]]

Axiom 9

We are given that:

t[x1, t[x2, x3]]==t[t[x1, x2], x3]

Hypothesis 1

We would like to show that:

t[n[a], n[a]]==t[a, a]

Critical Pair Lemma 1

The following expressions are equivalent:

p[0, x1]==x1

Proof

Note that the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Axiom 4 and Axiom 1 respectively.

Critical Pair Lemma 2

The following expressions are equivalent:

p[x1, p[n[x1], x2]]==p[0, x2]

Proof

Note that the input for the rule:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Axiom 5 and Axiom 6 respectively.

Critical Pair Lemma 3

The following expressions are equivalent:

t[p[1, x1], x2]==p[x2, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x3_, x2_]]->t[p[x1, x3], x2]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[1, x1_]->x1

where these rules follow from Axiom 7 and Axiom 3 respectively.

Critical Pair Lemma 4

The following expressions are equivalent:

t[x1, p[1, x2]]==p[x1, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x1_, x3_]]->t[x1, p[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 1]->x1

where these rules follow from Axiom 8 and Axiom 2 respectively.

Critical Pair Lemma 5

The following expressions are equivalent:

t[p[1, x1], 0]==t[x1, 0]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

p[x1_, t[x2_, x1_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 6

The following expressions are equivalent:

t[0, 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Critical Pair Lemma 5 and Axiom 1 respectively.

Substitution Lemma 1

It can be shown that:

t[0, 0]==0

Proof

We start by taking Critical Pair Lemma 6, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 7

The following expressions are equivalent:

t[x1, 0]==t[p[x1, 1], 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 5 and Axiom 4 respectively.

Critical Pair Lemma 8

The following expressions are equivalent:

t[0, p[1, x1]]==t[0, x1]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

p[x1_, t[x1_, x2_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 9

The following expressions are equivalent:

t[p[x1, 1], p[1, 0]]==p[p[x1, 1], t[x1, 0]]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[p[x1_, 1], 0]->t[x1, 0]

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 7 respectively.

Substitution Lemma 2

It can be shown that:

t[p[x1, 1], 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Critical Pair Lemma 9, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 3

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Substitution Lemma 2, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Substitution Lemma 4

It can be shown that:

p[x1, 1]==p[x1, p[1, t[x1, 0]]]

Proof

We start by taking Substitution Lemma 3, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Critical Pair Lemma 10

The following expressions are equivalent:

t[0, x1]==t[0, p[x1, 1]]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 8 and Axiom 4 respectively.

Critical Pair Lemma 11

The following expressions are equivalent:

t[p[1, 0], p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

t[x2_, x1_]

which can be unified with the input for the rule:

t[0, p[x1_, 1]]->t[0, x1]

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 10 respectively.

Substitution Lemma 5

It can be shown that:

t[1, p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Critical Pair Lemma 11, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 6

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Substitution Lemma 5, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Substitution Lemma 7

It can be shown that:

p[x1, 1]==p[x1, p[1, t[0, x1]]]

Proof

We start by taking Substitution Lemma 6, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Substitution Lemma 8

It can be shown that:

p[x1, p[n[x1], x2]]==x2

Proof

We start by taking Critical Pair Lemma 2, and apply the substitution:

p[0, x1_]->x1

which follows from Critical Pair Lemma 1.

Critical Pair Lemma 12

The following expressions are equivalent:

n[n[x1]]==p[x1, 0]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

p[n[x1_], x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Substitution Lemma 8 and Axiom 6 respectively.

Substitution Lemma 9

It can be shown that:

n[n[x1]]==x1

Proof

We start by taking Critical Pair Lemma 12, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 13

The following expressions are equivalent:

x1==p[n[x2], p[x2, x1]]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

n[x1_]

which can be unified with the input for the rule:

n[n[x1_]]->x1

where these rules follow from Substitution Lemma 8 and Substitution Lemma 9 respectively.

Critical Pair Lemma 14

The following expressions are equivalent:

t[x1, x2]==p[n[x2], t[p[1, x1], x2]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 3 respectively.

Critical Pair Lemma 15

The following expressions are equivalent:

t[x1, x2]==p[n[x1], t[x1, p[1, x2]]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 4 respectively.

Critical Pair Lemma 16

The following expressions are equivalent:

p[1, t[x1, 0]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[x1_, 0]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 4 respectively.

Substitution Lemma 10

It can be shown that:

p[1, t[x1, 0]]==1

Proof

We start by taking Critical Pair Lemma 16, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 17

The following expressions are equivalent:

t[t[x1, 0], 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[x1_, 0]]->1

where these rules follow from Critical Pair Lemma 5 and Substitution Lemma 10 respectively.

Substitution Lemma 11

It can be shown that:

t[x1, t[0, 0]]==t[1, 0]

Proof

We start by taking Critical Pair Lemma 17, and apply the substitution:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

which follows from Axiom 9.

Substitution Lemma 12

It can be shown that:

t[x1, 0]==t[1, 0]

Proof

We start by taking Substitution Lemma 11, and apply the substitution:

t[0, 0]->0

which follows from Substitution Lemma 1.

Substitution Lemma 13

It can be shown that:

t[x1, 0]==0

Proof

We start by taking Substitution Lemma 12, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 18

The following expressions are equivalent:

t[x1, t[0, x2]]==t[0, x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 0]->0

where these rules follow from Axiom 9 and Substitution Lemma 13 respectively.

Critical Pair Lemma 19

The following expressions are equivalent:

p[1, t[0, x1]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[0, x1_]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 7 respectively.

Substitution Lemma 14

It can be shown that:

p[1, t[0, x1]]==1

Proof

We start by taking Critical Pair Lemma 19, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 20

The following expressions are equivalent:

t[0, t[0, x1]]==t[0, 1]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[0, x1_]]->1

where these rules follow from Critical Pair Lemma 8 and Substitution Lemma 14 respectively.

Substitution Lemma 15

It can be shown that:

t[0, x1]==t[0, 1]

Proof

We start by taking Critical Pair Lemma 20, and apply the substitution:

t[x1_, t[0, x2_]]->t[0, x2]

which follows from Critical Pair Lemma 18.

Substitution Lemma 16

It can be shown that:

t[0, x1]==0

Proof

We start by taking Substitution Lemma 15, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Critical Pair Lemma 21

The following expressions are equivalent:

t[n[1], x1]==p[n[x1], t[0, x1]]

Proof

Note that the input for the rule:

p[n[x1_], t[p[1, x2_], x1_]]->t[x2, x1]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 14 and Axiom 6 respectively.

Substitution Lemma 17

It can be shown that:

t[n[1], x1]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 21, and apply the substitution:

t[0, x1_]->0

which follows from Substitution Lemma 16.

Substitution Lemma 18

It can be shown that:

t[n[1], x1]==n[x1]

Proof

We start by taking Substitution Lemma 17, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 22

The following expressions are equivalent:

t[n[1], t[x1, x2]]==t[n[x1], x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[n[1], x1_]->n[x1]

where these rules follow from Axiom 9 and Substitution Lemma 18 respectively.

Substitution Lemma 19

It can be shown that:

n[t[x1, x2]]==t[n[x1], x2]

Proof

We start by taking Critical Pair Lemma 22, and apply the substitution:

t[n[1], x1_]->n[x1]

which follows from Substitution Lemma 18.

Critical Pair Lemma 23

The following expressions are equivalent:

t[x1, n[1]]==p[n[x1], t[x1, 0]]

Proof

Note that the input for the rule:

p[n[x1_], t[x1_, p[1, x2_]]]->t[x1, x2]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 15 and Axiom 6 respectively.

Substitution Lemma 20

It can be shown that:

t[x1, n[1]]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 23, and apply the substitution:

t[x1_, 0]->0

which follows from Substitution Lemma 13.

Substitution Lemma 21

It can be shown that:

t[x1, n[1]]==n[x1]

Proof

We start by taking Substitution Lemma 20, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 24

The following expressions are equivalent:

n[t[x1, x2]]==t[x1, t[x2, n[1]]]

Proof

Note that the input for the rule:

t[x1_, n[1]]->n[x1]

contains a subpattern of the form:

t[x1_, n[1]]

which can be unified with the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

where these rules follow from Substitution Lemma 21 and Axiom 9 respectively.

Substitution Lemma 22

It can be shown that:

t[n[x1], x2]==t[x1, t[x2, n[1]]]

Proof

We start by taking Critical Pair Lemma 24, and apply the substitution:

n[t[x1_, x2_]]->t[n[x1], x2]

which follows from Substitution Lemma 19.

Substitution Lemma 23

It can be shown that:

t[n[x1], x2]==t[x1, n[x2]]

Proof

We start by taking Substitution Lemma 22, and apply the substitution:

t[x1_, n[1]]->n[x1]

which follows from Substitution Lemma 21.

Substitution Lemma 24

It can be shown that:

t[a, n[n[a]]]==t[a, a]

Proof

We start by taking Hypothesis 1, and apply the substitution:

t[n[x1_], x2_]->t[x1, n[x2]]

which follows from Substitution Lemma 23.

Conclusion 1

We obtain the conclusion:

True

Proof

Take Substitution Lemma 24, and apply the substitution:

n[n[x1_]]->x1

which follows from Substitution Lemma 9.

# 34 steps

Lemma 1: 0=0*a (8 steps)
0
A3: a*0 + -(a*0)
A4: -(a*0) + a*0
A2: -(a*0) + a*(0+0)
A8: -(a*0) + (a*0 + a*0)
A1: (-(a*0) + a*0) + a*0
A3: 0 + a*0
A4: a*0 + 0
A2: a*0

Theorem: -a*-a = a*a (49 steps)

-a * -a
A2: (-a+0) * -a
A2: (-a+0) * (-a+0)
A3: (-a+(a+-a)) * (-a+0)
A3: (-a+(a+-a)) * (-a+(a+-a))
A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a))
A8: -a*(-a+(a+-a)) + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+0)      + a*(-a+(a+-a))
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*(a+-a)
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*-a          + a*-a + a*a + a*-a
A8: -a*-a          + (-a+a)*-a             + a*a + a*-a
A3: -a*-a          + 0*-a                  + a*a + a*-a
L1: -a*-a          + 0                     + a*a + a*-a
A2: -a*-a                                  + a*a + a*-a
A4: a*a + -a*-a + a*-a
A8: a*a + (-a+a)*-a
A3: a*a + 0*-a
L1: a*a + 0
A2: a*a

• I'm noticing a lack of parens after a while. Because association costs steps, I think it would make it easier to verify your proof if you included the parens. Sep 27 '17 at 1:04
• Am still improving and updating. Will try to include all the parens when I'm done. Sep 27 '17 at 1:13

# 25 steps

Note: based on the question, I'm assuming that the rules of logic (including equality) are implied and do not count towards the total step count. That is, things like "if x=y, then y=x" and "if ((P AND Q) AND R) then (P AND (Q AND R))" can be used implicitly.

Lemma Z [6 steps]: 0*a = 0:

0 = (0*a) + (-(0*a))       | Ax. 3
= ((0+0)*a) + (-(0*a))   | Ax. 2
= (0*a + 0*a) + (-(0*a)) | Ax. 9
= 0*a + (0*a + (-(0*a))) | Ax. 1
= 0*a + (0)              | Ax. 3
= 0*a                    | Ax. 2

Lemma M [12 steps]: (-a)*b = -(a*b)

(-a)*b = (-a)*b + 0                | Ax. 2
= (-a)*b + (a*b + (-(a*b))) | Ax. 3
= ((-a)*b + a*b) + (-(a*b)) | Ax. 5
= ((-a)+a)*b + (-(a*b))     | Ax. 9
= 0*b + (-(a*b))            | Ax. 3
= 0 + (-(a*b))              | Lem. Z [6]
= -(a*b)                    | Ax. 2

Theorem [25 steps]: (-a)*(-a) = a*a

(-a)*(-a) = (-a)*(-a) + 0                | Ax. 2
= 0 + (-a)*(-a)                | Ax. 4
= (a*a + (-(a*a))) + (-a)*(-a) | Ax. 3
= a*a + ((-(a*a)) + (-a)*(-a)) | Ax. 1
= a*a + ((-a)*a + (-a)*(-a))   | Lem. M [12]
= a*a + ((-a)*(a + (-a)))      | Ax. 8
= a*a + ((-a)*0)               | Ax. 3
= a*a + 0                      | Lem. Z [6]
= a*a                          | Ax. 2

I feel like there's room for improvement here; for example, I use the commutative property of addition, though it feels like that should be unnecessary, since (-a)*(-a) = a*a is true in algebraic structures where addition is non-commutative. On the other hand, in those structures, the additive identity is commutative, and that's all I needed for the proof. I dunno. More generally, the proof's structure seems rather directionless; I just sort of threw stuff at the problem until it worked, so I bet there's some optimization to be done.

This was fun--thanks for the interesting and creative question OP! I haven't seen challenges like these before; hopefully becomes a thing!

• I see how the approach used in Lemma Z could make an equivalent proof for 0=(-a)*0 in 6 steps. Technically it deserves its own Lemma though, doesn't it? Jul 4 '19 at 1:52

## 22 23 Steps

• The problem does not allow to add terms on both sides of an equation; rather, we can only modify an initial string.
• Multiplication is not assumed to be commutative.
• We are given a unit 1, but it plays no role whatsoever in the puzzle because it is involved exclusively in the rules that define it.

Now for the proof (notice I define n = (-a) to simplify reading):

(-a)×(-a) :=
n×n =
n×n + 0 =                                [Ax. 2]
n×n + [n×a + -(n×a)] =                   [Ax. 3]
[n×n + n×a] + -(n×a) =                   [Ax. 1]
[n×(n+a)] + -(n×a) =                     [Ax. 8]
[n×(n+a) + 0] + -(n×a) =                 [Ax. 2]
[n×(n+a) + (n×a + -(n×a))] + -(n×a) =    [Ax. 3]
[(n×(n+a) + n×a) + -(n×a)] + -(n×a) =    [Ax. 1]
[n×((n+a) + a) + -(n×a)] + -(n×a) =      [Ax. 8]
[n×((a+n) + a) + -(n×a)] + -(n×a) =      [Ax. 4]
[n×(0 + a) + -(n×a)] + -(n×a) =          [Ax. 3]
[n×(a + 0) + -(n×a)] + -(n×a) =          [Ax. 4]
[n×a + -(n×a)] + -(n×a) =                [Ax. 2]
[(n+0)×a + -(n×a)] + -(n×a) =            [Ax. 2]
[(0+n)×a + -(n×a)] + -(n×a) =            [Ax. 4]
[((a+n)+n)×a + -(n×a)] + -(n×a) =        [Ax. 3]
[((a+n)×a+n×a) + -(n×a)] + -(n×a) =      [Ax. 9]
[(a+n)×a+(n×a + -(n×a))] + -(n×a) =      [Ax. 1]
[(a+n)×a + 0] + -(n×a) =                 [Ax. 3]
[(a+n)×a] + -(n×a) =                     [Ax. 2]
[a×a+n×a] + -(n×a) =                     [Ax. 9]
a×a+[n×a + -(n×a)] =                     [Ax. 1]
a×a+0 =                                  [Ax. 3]
a×a                                      [Ax. 2]

• @H.PWiz why can't you go from n to 0 + n in one step? Isn't that just A2? The rules do say The variables can also stand in for arbitrarily complex expressions Sep 28 '17 at 0:17
• @jq170727 Axiom 2 only states that a + 0 = a not that 0 + a = a. You need one extra commutative step to get from n to 0 + n. Sep 28 '17 at 4:29
• @H.PWiz can't you read the axiom in reverse? Sep 28 '17 at 4:35
• @jq170727 No you have to use commutativity for that. Oct 1 '17 at 23:15


text:
# Periodic Trends of Zeff and Electronegativity

The effective nuclear charge $Z_\mathrm{eff}$ increases from left to right and from top to bottom. Can you explain why it increases from top to bottom?

Also can we explain the periodic trend of electronegativity using the shielding effect?

EDIT: The calculation of $Z_\mathrm{eff}$ for Li would be 1 (3 protons − 2 core electrons). For Na is 1 (11 protons − 10 core electrons). So far it doesn't seem to me that $Z_\mathrm{eff}$ should increase from top to bottom. Considering the fact though that for Na there are more electrons shielding the only valence electron than Li as well as Na's electron is relatively more distant than that of Li, the first should be experiencing less $Z_\mathrm{eff}$. This is not true however. As far electronegativity is concerned I can't come up with a neat explanation.

• Looks like homework to me. Can you share what work you've done while working towards an answer? – Todd Minehardt Aug 7 '15 at 21:01
• Your misconception: Shielding by core electrons is perfect. Truth: shielding for Li is less than 2, shielding for Na is less than 10. – orthocresol Aug 8 '15 at 18:05


text:
## Georgia on my mind

The riddle of this week was inspired by the latest presidential elections when one State after another flipped the winner from Trump to Biden. Incl. Georgia.

On election night, the results of the 80 percent who voted on Election Day are reported out. Over the next several days, the remaining 20 percent of the votes are then tallied. What is the probability that the candidate who had fewer votes tallied on election night ultimately wins the race?

Assuming many votes, perfect balance between both candidates (p=½), and homogeneity between early and late ballots, the question boils down to the probability of a sum of two normals, X+Y, ending up being of the opposite sign from X, when the variances of X and Y are α and 1-α. Which writes as the expectation

$2 \mathbb{E}_\alpha[\Phi(-X/\sqrt{1-\alpha})]$

equal to

$\frac{2}{2\pi}\left(\frac{\pi}{2} + \arctan\{\sqrt{\alpha/(1-\alpha)|}\}\right)$

which returns a probability of about 0.14 when α=0.8. When looking at the actual data for Georgia, out of 5 million voters, at some point 235,000 ballots remained to be counted with Trump on the lead. This means an α about 0.05 and implies a probability of 7% (not accounting for the fact that the remaining mail-in-ballots were more favourable to Biden.)

This site uses Akismet to reduce spam. Learn how your comment data is processed.


text:
## A minimal deep learning library implementation in Python

August 10th, 2018

This tutorial introduces the main blocks needed to build a deep learning library in a few lines of Python. You'll learn how to build your (very) light-weight version of PyTorch!

## Convolutional Neural Networks

We'll assume familiarity with Convolutional Neural Network (CNN) models. If not I strongly recommend you to first read Stanford's CS231n course on CNNs.

##### Architecture of a CNN. — Source: https://www.mathworks.com.

The module inheritance paradigm underlies the widely used PyTorch, Sonnet and Gluon deep learning libraries. The idea is to build neural networks in a hierarchical and factored way by leveraging the modularity of so-called modules.
From a mathematical perspective a module is a differentiable function. It can have parameters to be learned and then needs to also be differentiable with respect to these parameters. From a programmatic perspective, it is a class implementing a forward method $\mathbf{y} = f(\mathbf{x})$ (input $\mathbf{x}$, output $\mathbf{y}$) and a backward method $g(\mathbf{x}, \nabla\mathbf{y}) = \nabla_{\mathbf{x}} \ f(\mathbf{x}) \times \nabla \mathbf{y}$. If it has parameters $\theta$ that we wish to learn, it additionally needs these parameters as attributes, a step method that performs an optimisation step on $\theta$ when called, and the backward method to also compute and save $\nabla_{\theta} f_\theta(\mathbf{x}) \times \nabla\mathbf{y}$ before returning $g(\mathbf{x}, \nabla\mathbf{y})$. Below is the abstract Module class that will be inherited.

This design enables to build small blocks of layers than can then be assembled to build bigger blocks and so on. Factoring code in this manner reduces the number of lines needed to defined a model and eases experimentation of new architectures.

### Layers

Layers are the basic functions composing neural networks. They will be implemented by inheriting the abstract Module class. For instance, a linear layer is parametrised by a weight $\mathbf{A}$ and a bias $\mathbf{b}$, and defined by the forward function $f(\mathbf{x}) = \mathbf{A} \mathbf{x} + \mathbf{b}$, the backward function $g(\mathbf{x}, \nabla\mathbf{y}) = \nabla_{\mathbf{x}} \ f(\mathbf{x}) \times \nabla \mathbf{y} = \mathbf{A} \nabla \mathbf{y}$ and its weight and bias partial derivatives $\nabla_{\mathbf{b}} \ f_{\mathbf{A},\mathbf{b}}(\mathbf{x}) \times \nabla\mathbf{y} = 1^T \nabla\mathbf{y}$ and $\nabla_{\mathbf{A}} \ f_{\mathbf{A},\mathbf{b}}(\mathbf{x}) \times \nabla\mathbf{y} = \nabla\mathbf{y}^T \mathbf{x}$.

### Training

Neural networks can be trained via back-propagation which is the application of the chain rule to the loss's gradient up to the neural net's layers parameters. For easiness, we restrict ourselves to neural nets that can be represented as a composition of functions $f(\mathbf{x}) = f_n \circ \dots \circ f_1(\mathbf{x})$. It enables to represent explicitly the dependency between layers via a list. Some networks like ResNets are excluded by this assumption since they need the network to be represented as a DAG, but it's all right for our purpose.

Such composition of functions are implemented via a Sequential class constructed with a list of sub-modules. Then its forward method calls each sub-module's forward method, its backward calls in reverse order each sub-module's backward method, and its step method calls each trainable (having parameters to learn) sub-module's step method.

The network is trained so as to minimise a user-defined loss $L(\mathbf{X}, \mathbf{y}^{\text{true}}, \theta) = \sum_{i} l(f_{\theta}(\mathbf{x}_i), y{\text{true}}_i)$. The cross entropy is for instance widely used for classification tasks.

Hence, each trainable layer gets its parameters partial derivative automatically computed by backpropagating the loss's gradient through the sequence of layers: $$\forall i=n,\dots,1 \quad \nabla_{\theta_i} L(\mathbf{X}, \mathbf{y}, \theta) = \nabla_{\theta_i} f_i(\mathbf{X}) \times \left( g_{i+1} \circ \dots \circ g_n \left(\nabla_{X} L \left(\mathbf{X}, \mathbf{y}, \theta\right) \right) \right)$$

## Optimisation

The most straightforward optimisation scheme for neural networks is (momentum) stochastic gradient descent which applies the following update on the parameters $\theta$ $$v_t = \gamma v_{t-1} + \eta \nabla_\theta J( \theta) \\ \theta = \theta - v_t$$ with $\eta$ being the learning rate and $\gamma$ the momentum coefficient. SGD inherits from Optmizer as implemented below.

I also implemented Adam and RMSProp in optim.py. For a nice review of gradient-based optimisation schemes used for deep neural nets training, check S. Ruder's blog post.

An optimisation step can then be performed by calling

## Demonstration on MNIST

Let's demonstrate our library on the MNIST classification task dataset. We define our CNN by inheriting the Module class, thus implementing the forward, backward and step methods as shown below.

Clone the associated Github repository and then run the example script so as to load the MNIST dataset, instantiate the CNN model, train it by backpropagation and eventually predict a digit's label as plotted below.

### What's missing towards a complete library ?

We've built in this tutorial the minimum blocks towards a working deep learning library, yet some parts are still missing to have a complete library. First, an automatic-differentation (autodiff) library avoid having to explicitly manipulate the gradients. Indeed, while being (imperatively) defined, the neural net is then implicitly represented as a DAG, allowing gradients to be automatically computed in a backward manner via the chain rule. Moreover, a data-loader wrapper is really useful so as to ease downloading, loading and preprocessing datasets. More layers and optimisation schemes should also be added. GPU support is also really important for large scale training.

### Acknowledgments

I’m grateful to Thomas Pesneau and Yuan Zhou for their comments.


text:
# How to report Logistic Regression Pseudo-R^2 in publication or reports?

I have a Logisitc Regression model with a McFadden Pseudo-$$R^2=0.7113$$. Based on the answers to this question: McFadden's Pseudo-R2 Interpretation, it seems my model has a good fit. However if I want to present this result in a report, what is the interpretation of good fit? According to this link: http://www.statisticalassociates.com/logistic10.htm, Pseudo-$$R^2$$ is NOT a measure of percent of variance explained in the dependent variable by the model. This is exactly what I thought it was but apparently it is wrong.

• You'll find an excellent paper on this topic by Mittlbock and Schemper: onlinelibrary.wiley.com/doi/abs/10.1002/… In summary, they recommend the use of the squared Pearson correlation coefficient of observed outcome with the estimated probability and another $R^2$ measure like linear sum of squares. Other popular measures were found to be lacking on one of their 12 judgement criteria. – StatsStudent Jan 20 at 21:37
• Hi StatsStudent, thanks for the link. I have glanced over the paper quickly but I will take some time soon to read and understand it fully. So just to clarify, are you suggesting it is inappropriate to report on Pseudo-$R^2$ as a metric in reports? – Suraj Iyer Jan 20 at 22:48
• Well, "inappropriate" might be a bit strong and whether it's appropriate or not is somewhat subjective, depending on what criteria one chooses to judge the measure by. I like to use the squared Pearson correlation coefficient of observed outcomes with the estimated probabilities as described by Mittlbock and Schemper, because the it can attain a lower bound of zero and an upper bound of one, it has an easy interpretation, and it's not changed by linear transformations of the predictor variables. – StatsStudent Jan 20 at 23:00
• Lastly, I wouldn't spent too much time wringing your hands on which measure to use. As long as it's well reasoned and you can explain why you chose to use the measure you chose. – StatsStudent Jan 20 at 23:01
• Any particular reason you choose the squared pearson over the sum-of-squares measure? I can understand ofcourse, as you said if its only for simplicity, or are there some cases where you would pick the latter? – Suraj Iyer Jan 20 at 23:28


text:
0
Technical Brief

# Effects of Bearings and Housing on Mode Localization of a Nearly Cyclic Symmetric SystemOPEN ACCESS

[+] Author and Article Information
Y. F. Chen

Department of Mechanical Engineering,
University of Washington,
Seattle, WA 98195-2600
e-mail: yfcheng@uw.edu

I. Y. Shen

Professor
Department of Mechanical Engineering,
University of Washington,
Seattle, WA 98195-2600
e-mail: ishen@uw.edu

Contributed by the Design Engineering Division of ASME for publication in the JOURNAL OF VIBRATION AND ACOUSTICS. Manuscript received December 8, 2015; final manuscript received April 27, 2016; published online June 2, 2016. Assoc. Editor: Carole Mei.

J. Vib. Acoust 138(5), 054501 (Jun 02, 2016) (7 pages) Paper No: VIB-15-1514; doi: 10.1115/1.4033569 History: Received December 08, 2015; Revised April 27, 2016

## Abstract

This technical brief is to study how flexible bearings and housing affect mode localization of a nearly cyclic symmetric system with mistuning. This study is conducted via finite-element analyses and deductive reasoning. A reference system studied is a bladed disk with two groups of 24 localized modes. When bearings and housing are introduced into the reference system, their presence changes natural frequencies, mode shapes, and the number of the localized modes. Moreover, the mistuning causes bearing forces to surge for all the localized modes. A deductive reasoning based on the existing literature supports the observation from the finite-element analyses.

<>

## Introduction

Cyclic symmetric bladed disks have been widely studied in the last several decades for their critical industrial applications, such as turbines and compressors [1,2]. Due to manufacturing tolerance, wear, or damage, the blades vary slightly from one another, and the blade variation is known as mistuning. When mistuning is present, vibration of the bladed disks may become localized at only a few blades. The phenomenon of mode localization could cause premature high-cycle fatigue and accelerate the damage of the bladed disks [3]. Moreover, when the mode localization occurs, amplitude of a few blades is largely amplified under engine order excitation of the pressure [4].

Due to its potential impact, the mode localization has been studied via different approaches, such as component-mode synthesis [5,6], the Rayleigh–Ritz method [7,8], the Taylor series [9], and the finite-element methods [10]. In many of these studies, a simplified bladed-disk model is used as a benchmark to facilitate prediction of the model localization. The benchmark model often has a single disk with multiple blades simulating a single-stage rotor. In addition, the inner rim of the bladed-disk is fixed to simplify the analysis. Although the simplified model has successfully demonstrated the phenomenon of mode localization, the model does not account for the effects of other machine components, such as the shaft supporting the bladed disk, bearings, and housing. Therefore, how these machine components would affect mode localization remains unknown. Moreover, if these components did affect mode localization, what would be the underlying mechanisms and physics? If the mode localization was affected, what would be its implication to the performance of the entire rotor assembly?

Recently, researchers started to analyze vibration of turbomachinery rotors more accurately by modeling multistage bladed disks [1114]. A key observation is that the presence of interconnecting boundary conditions between stages affects mode localization. Specifically, some extreme localized modes present in a single-stage system are mitigated after the stages are connected together. Root causes behind the mitigation or evolution of the localized modes are not well understood. The recent studies on multistage rotor vibration echoes the three questions raised above: how would mode localization be affected, what would be the underlying mechanisms, and what would be its implications?

Motivated by the needs above, this technical brief is to study how the supporting shaft, bearings, and housing affect mode localization of a mistuned bladed disk. The study is done via two different approaches. The first approach is to observe how mode localization evolves by conducting a finite-element analysis (FEA) on a reference system. Specifically, the reference system is a mistuned, bladed disk with a fixed inner rim. To simulate the presence of bearing supports, the fixed inner rim is replaced with an elastic boundary condition. Finally, a housing is coupled with the reference system through the flexible bearings.

The second approach is via a deductive reasoning from the existing literature to obtain qualitative theoretical predictions to justify the finite-element results. For example, Chen and Shen [15] identified that mode localization in a mistuned cyclic symmetric system will only occur when the two following conditions are met: (a) there is a group of vibration modes of the tuned cyclic symmetric rotor whose natural frequencies are nearly identical and the mode shapes have similar characteristics and (b) the vibration modes in the group contain a wide range of wave numbers. Kim et al. [16] showed that the vibration modes of a rotor will evolve in a certain manner when bearings are introduced to support the rotor. Predictions of the FEA should be consistent with the conclusions drawn from these prior publications.

Although mode localization can be caused by both mass and stiffness mistuning [15,17], we only consider stiffness mistuning in this technical brief for the sake of computational efficiency. The results are also valid for mode localization from mass mistuning.

## Reference System

The reference system consists of two versions: a tuned system and a mistuned system. Both the systems are studied via FEA to establish a baseline. The reference system has the same geometry as used in Ref. [15], which consists of a circular disk and 24 identical blades with fixed boundary condition at the inner rim, see Fig. 1 of Ref. [15]. The disk has a density of 855 $kg/m3$ and a Young's modulus of 189 GPa. The tuned blades have a density of 855 $kg/m3$ and a Young's modulus of 85 GPa. The circular disk defines the xy-plane, and the out-of-plane direction is the z direction.

Figure 1 shows the natural frequencies of the tuned reference system, plotted with respect to the number of nodal diameters. Based on their mode shapes, these natural frequencies are grouped into several families as labeled. Rules of the labels and representative mode shape of each family can also be found in Ref. [15]. Natural frequencies are sorted in an ascending order, and corresponding mode numbers are also listed in Fig. 1 to index each natural frequency. Note that many natural frequencies have two mode numbers, because the natural frequencies are repeated. By constructing families of natural frequencies, we can easily identify the types of modes that contribute to a localized mode.

Based on the tuned reference system, mistuning is generated via random numbers with $2.7%$ standard deviation in Young's modulus of each blade. FEA shows that there are two sets of mode localization. The first set of mode localization occurs near 900 Hz, and there are 24 localized modes. The modes involved are from the B-in-0 family with blade in-plane vibration, see Fig. 7(a) of Ref. [15]. The second set of mode localization occurs near 1100 Hz, and there are also 24 localized modes. The modes involved are primarily from the B-out-torsional family with blade torsional vibration, see Fig. 8(a) of Ref. [15].

## Effects of Flexible Bearings

To study the effects of flexible bearings on mode localization, we modify the reference system with an elastic boundary condition at the inner rim. Specifically, two sets of contact elements are used to constrain upper and lower surfaces of the inner rim evenly. The movements of each set of contact elements are represented by a pilot point that is connected to a fixed point with a linear spring to simulate a flexible bearing. The two pilot points are located at $z=±10$ mm, respectively. The linear springs have linear stiffness of $2.16×107$ N/m in the in-plane directions (i.e., x- and y-directions), linear stiffness of $5.76×106$ N/m in the out-of-plane direction (i.e., z-direction), and rotational stiffness of 58.5 $N·m/rad$ for pitch and roll (i.e., about x- and y-axes, respectively). This formulation is referred to as the “rotor–bearing system” in the sequel. The rotor–bearing system also consists of two versions: a tuned system and a mistuned system.

Figure 2 shows the natural frequencies of the tuned, bladed disk with the elastic bearings. By comparing Fig. 2 with Fig. 1, we confirm that only vibration modes with 0 or 1 nodal diameter have changed their natural frequencies when the elastic bearings are introduced. This observation is consistent with that predicted in Ref. [16]. Moreover, modes from the D-out-2 family significantly change their natural frequencies, while modes from the B-out-torsional family do not. In other words, disk-dominant modes change their natural frequencies more than the blade-dominant modes. This result is not surprising. For blade-dominant modes, there is almost no deformation at the inner rim. Therefore, the boundary condition change at the inner rim affects minimally the natural frequencies of the blade-dominant modes.

The same mistuning of 2.7% variations in the Young's modulus is now added to the tuned rotor–bearing system. FEA shows that the mode localization occurs again in the frequency range of B-in-0 and B-out-torsional families. Moreover, the number of localized modes obtained from the FEA is listed in Table 1 for comparison. For the B-in-0 family, the number of localized modes remains 24 after the bearings are introduced. In contrast, the number of localized modes in the frequency range of the B-out-torsional family is now increased to 26 from 24. The two additional modes, due to the presence of the elastic bearings, are mode 111 (at 1102.6 Hz) and mode 112 (at 1104 Hz). Their mode shapes are shown in Fig. 3, where the pink circle in the middle of each plot represents flexible bearings.

For the rest of 24 localized modes, the presence of the bearings can change their mode shapes too. For instance, Fig. 4 shows the 16th localized mode with blade torsional vibration before and after the bearings are introduced (i.e., modes 108 and 109 of the mistuned systems). The natural frequency shifts only slightly from 1102 Hz to 1101 Hz. The mode shape, however, changes dramatically. The vibration was localized at blades 11 and 12 when the inner rim is fixed. Now the vibration is localized at blade 8 when the bearing is present. From the FEA above, we reach the first conclusion—the presence of bearings may affect mode localization via the number and shape of localized modes.

The presence of mode localization is also accompanied by unbalanced bearing forces. Figure 5 shows the Euclidean norm of the modal bearing force of the tuned and mistuned rotor–bearing system. In Fig. 5, the plus markers represent bearing forces from the tuned rotor. In contrast, the circle markers represent bearing forces from the mistuned rotor, with the larger circle markers representing contribution from modes that are extremely localized. The upper plot shows the bearing force from each mode with respect to the frequency, while the two bottom plots show the bearing forces from the B-in-0 family and the B-out-torsion family in the order of ascending frequencies. When the rotor is tuned, most vibration modes except two have small bearing forces. When the mistuning is introduced, all the vibration modes have significant bearing forces.

## Theoretical Investigation

The change in the number of localized modes and the bearing forces can be explained and justified via theoretical analyses that are available in the literature [15,16].

###### Number of Localized Modes.

According to Ref. [15], the mode localization occurs when the following two conditions are met for a tuned cyclic symmetric system. First, there must be a group of modes that have very close natural frequencies. Second, this group of modes contains a wide range of wave numbers. When mistuning is present, vibration modes in the group can be linearly combined to form localized modes whose vibration is confined only at one or two blades. Moreover, vibration modes participating in the linear combination must have similar features in their mode shapes.

For the tuned reference system, there are two groups of modes that have very close natural frequencies, see Fig. 1. One is around 1100 Hz, and the other is around 900 Hz. Let us focus on the first group of modes around 1100 Hz. When the tuned system has no bearing, this group consists of 24 modes (i.e., modes 93–116 in Fig. 1) with very close natural frequencies. These modes encompass 0–12 nodal diameters, thus containing a wide range of wave numbers. These modes all come from the B-out-torsional family with a common feature of blade torsional vibration. Therefore, all the conditions for mode localization are met, and these 24 modes are linearly combined to form 24 localized modes shown in Table 1.

When the bearing is introduced, the group with a natural frequency around 1100 Hz grows to 26 modes (i.e., modes 94–119 in Fig. 2). In addition to the original 24 modes from the B-out-torsion family, there are two modes (114 and 115) from the D-out-3 family that have a significant blade torsion, see Fig. 6. In other words, all these 26 modes share the same feature of blade torsional vibration. Besides, these 26 modes encompass 0–12 nodal diameters, thus containing a wide range of wave numbers. Again, all the conditions for mode localization are met and these 26 modes are linearly combined to form 26 localized modes in Table 1 when the mistuning is introduced.

The analysis above explains why the number of localized modes increases from 24 to 26 when the bearing is introduced. In essence, the presence of the bearings basically introduces additional degrees-of-freedom to the reference system and thus provides additional modes that could form a group for mode localization. If the bearing coefficients are properly chosen so that the conditions for mode localization are met, these additional modes would participate in the linear combination to form additional localized modes.

The same analysis above can also explain why the group around 900 Hz does not change its number of localized modes when the bearing is introduced. When the bearing is not present, there are roughly 26 modes in this group (i.e., modes 59–84 in Fig. 1). Specifically, 24 of them are from the B-in-0 family with a common feature of blade in-plane vibration. Moreover, they encompass 0–12 nodal diameters, thus containing a wide range of wave numbers. The remaining two of the 26 modes (i.e., modes 59 and 60) are from the D-out-2 family without any blade in-plane vibration. Therefore, the 24 modes from the B-in-0 family meet the conditions of mode localization and are linearly combined to form the 24 localized modes. When the bearings are introduced, there are no additional vibration modes appearing in this frequency range. Moreover, all the vibration modes in this group around 900 Hz are almost unchanged. As a result, the model localization form by the B-in-0 family remains the same.

###### Bearing Forces.

First of all, major results from Ref. [16] are summarized below to facilitate the analysis of bearing forces. Consider a tuned cyclic symmetric system consisting of N identical substructures with a fixed boundary (e.g., a bladed disk with a fixed inner rim). Every mode shape of the cyclic symmetric system is then characterized via a phase index n that defines a phase difference between the two neighboring substructures. When the bearings are introduced into the tuned cyclic symmetric system, some modes will be coupled to the bearings changing their natural frequencies. These modes are called unbalanced modes. Other modes will not be affected and are called balanced modes. Only the modes with phase indices $n=1,N−1,N$ may be the unbalanced modes.

The physics behind the balanced and unbalanced modes is quite straightforward. When the tuned system vibrates in a balanced mode, the inertial force (and its moments) arising from the vibration turns out to be zero. No net forces or moments are transmitted to the fixed boundary; therefore, introduction of the bearings will not affect the state of the vibration. On the contrary, when an unbalanced mode vibrates, the inertial force results in a net force or moment acting on the fixed boundary. When the bearings are present, the net force or moment deforms the bearings leading to a coupled bearing–rotor vibration affecting the natural frequency of the unbalanced modes.

For the tuned, bladed disk shown in the reference system, the phase index is related to the number of nodal diameters. The 0-nodal-diameter modes correspond to phase index n = N, while the 1-nodal-diameter modes correspond to phase indices n = 1 and $n=N−1$. Therefore, 0 - and 1-nodal-diameter modes may be affected when the bearings are introduced. The most prominent changes appear in the D-out-3 family in Figs. 1 and 2.

The presence of unbalanced modes can also be seen in the modal bearing forces plotted in Fig. 5. For the tuned system, the unbalanced modes have significantly larger bearing forces than the balanced modes. As shown in Fig. 5, the blue plus markers represent the modal bearing forces from the tuned system. Note that only two blue plus markers in the B-in-0 family (bottom left plot) and in the B-out-torsional (bottom right plot) have large bearing forces. They correspond to the 1-nodal-diameter modes, which are unbalanced. The 0-nodal-diameter modes in B-in-0 family and B-out-torsional family happen to have zero net inertia force and moment.

When the mistuning is present, all the localized modes can be expressed in terms of linear combinations of a group of modes from the tuned system. Since the group of modes must encompass a wide range of wave numbers, it will naturally include both balanced modes and unbalanced modes. Therefore, all the localized modes will have the contribution of unbalanced modes implying that all the localized modes will incur a large bearing force as shown in the red circle markers in Fig. 5.

## Effects of Housing

To study the effects of housing on mode localization, we attach the bladed disk and its bearings (cf. Fig. 3) to a flexible housing creating a new finite-element model. The housing is a square plate with a central stud, on which the bladed disk can be supported. The square plate has a density of 855 $kg/m3$ and a Young's modulus of 90 GPa. Moreover, it is fixed at its four corners. The contact elements are used to constrain the inner surface of the bladed disk and the outer surface of the stud, and their movements are represented via pilot points. A linear spring is then used to connect the two pilot points to model the flexible bearings. The bearing stiffness remains the same as that used in the rotor–bearing system. This system with the bladed disk, housing, and bearings will be referred as the “rotor–bearing–housing system” henceforth.

The housing in the form of a square plate is chosen for the sake of simplicity. The square plate certainly does not at all resemble a real housing in a turbomachine, but it does provide needed characteristics of a housing, such as natural frequencies and mode shapes. Tai and Shen [18] have shown that the effects of housing are primarily characterized through its natural frequencies and mode shapes in coupled rotor–bearing–housing vibration. Therefore, employment of a square plate as the housing is a simple way to showcase physical insights without incurring huge computational costs. At the same time, fundamental findings from the simulations will also be valid for housing of arbitrary geometry.

Figure 7 shows natural frequencies of the tuned rotor–bearing–housing system. In particular, Fig. 7 is zoomed in to focus only on the frequency ranges of B-out-torsional and B-in-0 families, for which mode localization will occur. With the addition of the housing, the number of degrees-of-freedom increases drastically and so does the number of modes. Many of these newly added modes present vibration patterns that are heavily dominated by housing deformation. The natural frequencies of these housing-dominant modes are marked as red diamonds in Fig. 7 without reference to the number of nodal diameters. According to the theoretical analysis above, more localized modes may appear when mistuning is present.

The blade mistuning of 2.7% variations in Young's modulus is then introduced into the tuned rotor–bearing–housing system. FEA results show that there are 26 localized modes in the frequency range of B-in-0 family and 26 localized modes in the B-out-torsional family, see Table 1. Compared with the mistuned reference bladed disk with bearings only, major changes occur in the frequency range of the B-in-0 family.

Regarding the two new localized modes, the most critical feature is the significant housing deformation. Figure 8 shows the two newly added localized modes, with the bladed disk on the left and the housing on the right. One is mode 104 with frequency of 870.56 Hz and the other is mode 107 with frequency 873.97 Hz. In both modes, the housing undergoes considerable out-of-plane vibration. FEA results in Fig. 8 clearly indicate that housing can affect mode localization via bearings.

The interaction between vibration of the housing and mode localization of the rotor is also observed in forced response. For example, Fig. 9 shows FRF of blade 3 as labeled in Fig. 4 from 850 Hz to 1120 Hz covering B-in-0 and B-out-torsional families. A sinusoidal force is applied in the out-of-plane direction at a point on the housing marked by the yellow dot in Fig. 8(b). The damping ratio is assumed to be 0.05%. Two reactions are calculated: (1) Euler norm of displacement at the left tip of blade 3 and (2) von Mises strain at the left root of blade 3. In Fig. 9, the highest peaks of the displacement are at 860.6 Hz, 870.56 Hz, 874.0 Hz, and 924.1 Hz. The three modes at 860.6 Hz, 874.0 Hz, and 924.1 Hz are out-of-plane housing-dominated modes. Since these three modes do not have rotor deformation, their von Mises strain is small (cf. Fig. 9). On the contrary, the mode at 870.56 Hz is one of the newly added localized modes that have rotor vibration localized on blade 3 with significant housing deformation. As a result, the von Mises strain at 870.56 Hz has the highest peak between 850 Hz and 1120 Hz. This example demonstrates that forces exerted on the housing may also excite a localized mode on the rotor via bearings.

According to the FEA above, the coupling between the housing and localized modes arises because some natural frequencies of the housing fall in the frequency ranges of localized modes. To alleviate the excitation of localized modes, the housing should be designed such that the natural frequencies of the housing are sufficiently far away from the frequency ranges of localized modes.

## Conclusions

Through finite-element simulations and deductive reasoning from existing theoretical analyses, we reach the following conclusions:

1. (1)Boundary conditions are critical to the mode localization phenomenon of a nearly cyclic symmetric system with mistuning.
2. (2)Presence of bearings and housing may not only introduce additional localized modes but may also dramatically change the shape of existing localized modes. Whether or not the presence of bearings and housing may affect mode localization depends on the stiffness of the bearings and housing.
3. (3)Presence of mistuning causes all the localized modes to become unbalanced, thus resulting in a net force or moment transmitted to the bearings for every localized mode.
4. (4)The conclusions above are well justified in the context of theoretical analyses developed in Refs. [15] and [16].

## Acknowledgements

This material was based upon the work supported by the National Science Foundation under Grant No. CMMI-0969024. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

## References

Srinivansan, A. V. , 1997, “ Flutter and Resonant Vibration Characteristics of Engine Blades,” ASME J. Eng. Gas Turbines Power, 119(4), pp. 742–775.
Castanier, M. , and Pierre, C. , 2006, “ Modeling and Analysis of Mistuned Bladed Disk Vibration Status and Emerging Directions,” J. Propul. Power, 22(2), pp. 384–396.
Thomson, D. E. , and Griffin, J. T. , 1999, “ The National Turbine Engine High Cycle Fatigue Program,” Global Gas Turbine News, 39(1), pp. 14–17.
Sinha, A. , 2008, “ Mistuning Analyses of a Bladed Disk: Pole-Zero and Modal Approaches,” ASME Paper No. GT2008-50191.
Ottarsson, G. , Castanier, M. P. , and Pierre, C. , 1997, “ A Reduced Order Modeling Technique for Mistuned Bladed Disks,” ASME J. Vib. Acoust., 119(3), pp. 439–447.
Bladh, R. , Castanier, M. P. , and Pierre, C. , 2001, “ Component-Mode-Based Reduced Order Modeling Techniques for Mistuned Bladed Disks—Part I: Theoretical Models,” ASME J. Eng. Gas Turbines Power, 123(1), pp. 89–99.
Griffin, J. , and Yang, M.-T. , 2001, “ A Reduced-Order Model of Mistuning Using a Subset of Nominal System Modes,” ASME J. Eng. Gas Turbines Power, 119(1), pp. 161–167.
Feiner, D. M. , and Griffin, J. H. , 2004, “ Mistuning Identification of Bladed Disks Using a Fundamental Mistuning Model—Part I: Theory,” ASME J. Turbomach., 126(1), pp. 150–158.
Sinha, A. , 2010, “ Computation of Eigenvalues and Eigenvectors of a Mistuned Bladed Disk Via Unidirectional Taylor Series Expansions,” ASME J. Turbomach., 132(4), p. 044501.
Bauchau, O. A. , 2009, “ Modeling Rotorcraft Dynamics With Finite Element Multibody Procedures,” ASME Paper No. DETC2009-86721.
Sinha, A. , 2008, “ Reduced-Order Model of a Mistuned Multi-Stage Bladed Rotor,” J. Turbo Jet Engines, 25(3), pp. 145–153.
Laxalde, D. , Lombard, J.-P. , and Thouverez, F. , 2007, “ Dynamics of Multi-Stage Bladed Disks Systems,” ASME J. Eng. Gas Turbines Power, 129(4), pp. 1058–1064.
Bladh, R. , Castanier, M. P. , and Pierre, C. , 2003, “ Effects of Multistage Coupling and Disk Flexibility on Mistuned Bladed Disk Dynamics,” ASME J. Eng. Gas Turbines Power, 125(1), pp. 121–130.
D'Souza, K. , Jung, C. , and Epureanu, B. I. , 2013, “ Analyzing Mistuned Multi-Stage Turbomachinery Rotors With Aerodynamic Effects,” J. Fluids Struct., 42, pp. 388–400.
Chen, Y. F. , and Shen, I. Y. , 2015, “ Mathematical Insights Into Linear Mode Localization in Nearly Cyclic Symmetric Rotors With Mistune,” ASME J. Vib. Acoust., 137(4), p. 041007.
Kim, H. , Colonnese, N. T. K. , and Shen, I. Y. , 2009, “ Mode Evolution of Cyclic Symmetric Rotors Assembled to Flexible Bearings and Housing,” ASME J. Vib. Acoust., 131(5), p. 051008.
Sinha, A. , 2009, “ Reduced-Order Model of a Bladed Rotor With Geometric Mistuning,” ASME J. Turbomach., 131(3), p. 031007.
Tai, W. C. , and Shen, I. Y. , 2015, “ Ground-Based Response of a Spinning, Cyclic Symmetric Rotor Assembled to a Flexible Stationary Housing Via Multiple Bearings,” ASME J. Vib. Acoust., 137(4), p. 041011.
Topics: Bearings , Disks , Rotors
View article in PDF format.

## References

Srinivansan, A. V. , 1997, “ Flutter and Resonant Vibration Characteristics of Engine Blades,” ASME J. Eng. Gas Turbines Power, 119(4), pp. 742–775.
Castanier, M. , and Pierre, C. , 2006, “ Modeling and Analysis of Mistuned Bladed Disk Vibration Status and Emerging Directions,” J. Propul. Power, 22(2), pp. 384–396.
Thomson, D. E. , and Griffin, J. T. , 1999, “ The National Turbine Engine High Cycle Fatigue Program,” Global Gas Turbine News, 39(1), pp. 14–17.
Sinha, A. , 2008, “ Mistuning Analyses of a Bladed Disk: Pole-Zero and Modal Approaches,” ASME Paper No. GT2008-50191.
Ottarsson, G. , Castanier, M. P. , and Pierre, C. , 1997, “ A Reduced Order Modeling Technique for Mistuned Bladed Disks,” ASME J. Vib. Acoust., 119(3), pp. 439–447.
Bladh, R. , Castanier, M. P. , and Pierre, C. , 2001, “ Component-Mode-Based Reduced Order Modeling Techniques for Mistuned Bladed Disks—Part I: Theoretical Models,” ASME J. Eng. Gas Turbines Power, 123(1), pp. 89–99.
Griffin, J. , and Yang, M.-T. , 2001, “ A Reduced-Order Model of Mistuning Using a Subset of Nominal System Modes,” ASME J. Eng. Gas Turbines Power, 119(1), pp. 161–167.
Feiner, D. M. , and Griffin, J. H. , 2004, “ Mistuning Identification of Bladed Disks Using a Fundamental Mistuning Model—Part I: Theory,” ASME J. Turbomach., 126(1), pp. 150–158.
Sinha, A. , 2010, “ Computation of Eigenvalues and Eigenvectors of a Mistuned Bladed Disk Via Unidirectional Taylor Series Expansions,” ASME J. Turbomach., 132(4), p. 044501.
Bauchau, O. A. , 2009, “ Modeling Rotorcraft Dynamics With Finite Element Multibody Procedures,” ASME Paper No. DETC2009-86721.
Sinha, A. , 2008, “ Reduced-Order Model of a Mistuned Multi-Stage Bladed Rotor,” J. Turbo Jet Engines, 25(3), pp. 145–153.
Laxalde, D. , Lombard, J.-P. , and Thouverez, F. , 2007, “ Dynamics of Multi-Stage Bladed Disks Systems,” ASME J. Eng. Gas Turbines Power, 129(4), pp. 1058–1064.
Bladh, R. , Castanier, M. P. , and Pierre, C. , 2003, “ Effects of Multistage Coupling and Disk Flexibility on Mistuned Bladed Disk Dynamics,” ASME J. Eng. Gas Turbines Power, 125(1), pp. 121–130.
D'Souza, K. , Jung, C. , and Epureanu, B. I. , 2013, “ Analyzing Mistuned Multi-Stage Turbomachinery Rotors With Aerodynamic Effects,” J. Fluids Struct., 42, pp. 388–400.
Chen, Y. F. , and Shen, I. Y. , 2015, “ Mathematical Insights Into Linear Mode Localization in Nearly Cyclic Symmetric Rotors With Mistune,” ASME J. Vib. Acoust., 137(4), p. 041007.
Kim, H. , Colonnese, N. T. K. , and Shen, I. Y. , 2009, “ Mode Evolution of Cyclic Symmetric Rotors Assembled to Flexible Bearings and Housing,” ASME J. Vib. Acoust., 131(5), p. 051008.
Sinha, A. , 2009, “ Reduced-Order Model of a Bladed Rotor With Geometric Mistuning,” ASME J. Turbomach., 131(3), p. 031007.
Tai, W. C. , and Shen, I. Y. , 2015, “ Ground-Based Response of a Spinning, Cyclic Symmetric Rotor Assembled to a Flexible Stationary Housing Via Multiple Bearings,” ASME J. Vib. Acoust., 137(4), p. 041011.

## Figures

Fig. 5

Bearing force comparison for tuned and mistuned rotor–bearing systems

Fig. 4

(a) Mistuned mode 108 with fixed inner rim (1102 Hz) and (b) mistuned mode 109 with bearings at inner rim (1101 Hz)

Fig. 3

Two additional localized modes for the mistuned rotor–bearing system: (a) mode 111 at 1102.6 Hz and (b) mode 112 at 1104 Hz

Fig. 2

Natural frequencies of the tuned rotor–bearing system

Fig. 1

Natural frequencies of the tuned reference system; 24 identical blades and a disk with a fixed inner rim

Fig. 6

Shape of mode 114 of tuned bladed disk with bearing

Fig. 7

Natural frequencies of tuned rotor–bearing–housing system

Fig. 8

Additional localized mode shapes with significant deformation on the housing unique to the bladed disk with bearing and housing: (a) mode shape on the rotor of mode 104, (b) mode shape on the housing of mode 104, (c) mode shape on the rotor of mode 107, and (d) mode shape on the housing of mode 107

Fig. 9

Frequency response function of for blade 3: displacement (upper plot) and von Mises strain (lower plot)

## Tables

Table 1 Number of localized modes in the frequency range of B-in-0 and B-out-torsional families

## Discussions

Some tools below are only available to our subscribers or users with an online account.

### Related Content

Customize your page view by dragging and repositioning the boxes below.

Related Journal Articles
Related Proceedings Articles
Related eBook Content
Topic Collections


text:
# Geometry Seminar

## Complete translating solitons to the mean curvature flow in R^3 with nonnegative mean curvature

Joel Spruck, JHU

Monday, March 20th, 2017
12:00 PM - 1:00 PM
Hylan 1106A

We prove that any complete immersed two sided mean convex translating soliton Sigma in R^3 for the mean curvature flow is convex. As a corollary it follows that any entire mean convex graphical translating soliton in R^3 is the axisymmetric “bowl soliton’’. We also show that if the mean curvature of Sigma tends to zero at infinity, then Sigma can be represented as an entire graph and so is the bowl soliton . Finally we classify all translating solitons defined over strip regions which are the only other nontrivial solutions

Event contact: skleene at ur dot rochester dot edu


text:
Presentation is loading. Please wait.

# 11.1 An Introduction to Sequences & Series p. 651.

## Presentation on theme: "11.1 An Introduction to Sequences & Series p. 651."— Presentation transcript:

11.1 An Introduction to Sequences & Series p. 651

Sequence: A list of ordered numbers separated by commas.A list of ordered numbers separated by commas. Each number in the list is called a term.Each number in the list is called a term. For Example:For Example: Sequence 1 Sequence 2 2,4,6,8,10 2,4,6,8,10,… Term 1, 2, 3, 4, 5Term 1, 2, 3, 4, 5 Domain – relative position of each term (1,2,3,4,5) Usually begins with position 1 unless otherwise stated. Range – the actual terms of the sequence (2,4,6,8,10)

Sequence 1 Sequence 2 2,4,6,8,102,4,6,8,10,… 2,4,6,8,102,4,6,8,10,… A sequence can be finite or infinite. The sequence has a last term or final term. (such as seq. 1) The sequence continues without stopping. (such as seq. 2) Both sequences have a general rule: a n = 2n where n is the term # and a n is the nth term. The general rule can also be written in function notation: f(n) = 2n

Examples: Write the first 6 terms of a n =5-n.Write the first 6 terms of a n =5-n. a 1 =5-1=4a 1 =5-1=4 a 2 =5-2=3a 2 =5-2=3 a 3 =5-3=2a 3 =5-3=2 a 4 =5-4=1a 4 =5-4=1 a 5 =5-5=0a 5 =5-5=0 a 6 =5-6=-1a 6 =5-6=-1 4,3,2,1,0,-14,3,2,1,0,-1 Write the first 6 terms of a n =2 n.Write the first 6 terms of a n =2 n. a 1 =2 1 =2a 1 =2 1 =2 a 2 =2 2 =4a 2 =2 2 =4 a 3 =2 3 =8a 3 =2 3 =8 a 4 =2 4 =16a 4 =2 4 =16 a 5 =2 5 =32a 5 =2 5 =32 a 6 =2 6 =64a 6 =2 6 =64 2,4,8,16,32,642,4,8,16,32,64

Examples: Write a rule for the nth term. The seq. can be written as: Or, a n =2/(5 n ) The seq. can be written as:The seq. can be written as: 2(1)+1, 2(2)+1, 2(3)+1, 2(4)+1,… Or, a n =2n+1

Example: write a rule for the nth term. 2,6,12,20,…2,6,12,20,… Can be written as:Can be written as: 1(2), 2(3), 3(4), 4(5),… Or, a n =n(n+1)

Graphing a Sequence Think of a sequence as ordered pairs for graphing. (n, a n )Think of a sequence as ordered pairs for graphing. (n, a n ) For example: 3,6,9,12,15For example: 3,6,9,12,15 would be the ordered pairs (1,3), (2,6), (3,9), (4,12), (5,15) graphed like points in a scatter plot * Sometimes it helps to find the rule first when you are not given every term in a finite sequence. Term # Actual term

Series The sum of the terms in a sequence.The sum of the terms in a sequence. Can be finite or infiniteCan be finite or infinite For Example:For Example: Finite Seq.Infinite Seq. 2,4,6,8,102,4,6,8,10,… Finite SeriesInfinite Series 2+4+6+8+102+4+6+8+10+…

Summation Notation Also called sigma notationAlso called sigma notation (sigma is a Greek letter Σ meaning sum) The series 2+4+6+8+10 can be written as: i is called the index of summation (its just like the n used earlier). Sometimes you will see an n or k here instead of i. The notation is read: the sum from i=1 to 5 of 2i i goes from 1 to 5.

Summation Notation for an Infinite Series Summation notation for the infinite series:Summation notation for the infinite series: 2+4+6+8+10+… would be written as: Because the series is infinite, you must use i from 1 to infinity () instead of stopping at the 5 th term like before.

Examples: Write each series in summation notation. a. 4+8+12+…+100 Notice the series can be written as: 4(1)+4(2)+4(3)+…+4(25) Or 4(i) where i goes from 1 to 25. Notice the series can be written as:

Example: Find the sum of the series. k goes from 5 to 10.k goes from 5 to 10. (5 2 +1)+(6 2 +1)+(7 2 +1)+(8 2 +1)+(9 2 +1)+(10 2 +1)(5 2 +1)+(6 2 +1)+(7 2 +1)+(8 2 +1)+(9 2 +1)+(10 2 +1) = 26+37+50+65+82+101 = 26+37+50+65+82+101 = 361

Special Formulas (shortcuts!)

Example: Find the sum. Use the 3 rd shortcut!Use the 3 rd shortcut!

Assignment

Similar presentations

Ads by Google


text:
# Measurement of the ratio of inclusive jet cross sections using the anti-kt algorithm with radius parameters R = 0.5 and 0.7 in pp collisions at sqrt(s) = 7 TeV

Abstract : Measurements of the inclusive jet cross section with the anti-kt clustering algorithm are presented for two radius parameters, R=0.5 and 0.7. They are based on data from LHC proton-proton collisions at sqrt(s) = 7 TeV corresponding to an integrated luminosity of 5.0 inverse femtobarns collected with the CMS detector in 2011. The ratio of these two measurements is obtained as a function of the rapidity and transverse momentum of the jets. Significant discrepancies are found comparing the data to leading-order simulations and to fixed-order calculations at next-to-leading order, corrected for nonperturbative effects, whereas simulations with next-to-leading-order matrix elements matched to parton showers describe the data best.
Document type :
Journal articles

http://hal.in2p3.fr/in2p3-00998919
Contributor : Sylvie Flores Connect in order to contact the contributor
Submitted on : Tuesday, June 3, 2014 - 7:07:09 AM
Last modification on : Monday, March 28, 2022 - 9:39:18 AM

### Citation

S. Chatrchyan, S. Baffioni, F. Beaudette, P. Busson, C. Charlot, et al.. Measurement of the ratio of inclusive jet cross sections using the anti-kt algorithm with radius parameters R = 0.5 and 0.7 in pp collisions at sqrt(s) = 7 TeV. Physical Review D, American Physical Society, 2014, 90, pp.072006. ⟨10.1103/PhysRevD.90.072006⟩. ⟨in2p3-00998919⟩

Record views


text:
RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
 General information Latest issue Forthcoming papers Archive Impact factor Subscription Guidelines for authors License agreement Submit a manuscript Search papers Search references RSS Latest issue Current issues Archive issues What is RSS

 Izv. RAN. Ser. Mat.: Year: Volume: Issue: Page: Find

 Izv. RAN. Ser. Mat., 2015, Volume 79, Issue 2, Pages 45–76 (Mi izv8094)

Estimates for the error of approximation of functions in $L_p^1$ by polynomials and partial sums of series in the Haar and Faber–Schauder systems

S. B. Vakarchuka, A. N. Shchitovb

a Dnepropetrovsk University of Economics and Law
b Ukrainian Academy of Customs, Dnipropetrovsk

Abstract: We find exact estimates for the error of approximation of functions in the classes $L_p^1$ by polynomials in the Haar system and partial sums of the Faber–Schauder series in the metrics of the spaces $L_p$. The error in approximating a function $f\in L_p^1$ is estimated in terms of the norms of the first derivatives $\|f^{(1)}\|_{L_p}$ and $\|f^{(1)}-\overline S^{(1)}_n(f)\|_{L_p}$. The resulting bounds are unimprovable for some values of $n$.

Keywords: Haar system of functions, Faber–Schauder system of functions, best approximation of functions by polynomials, one-sided approximation of functions by polynomials.

DOI: https://doi.org/10.4213/im8094

Full text: PDF file (717 kB)
References: PDF file   HTML file

English version:
Izvestiya: Mathematics, 2015, 79:2, 257–287

Bibliographic databases:

UDC: 517.5
MSC: 41A25
Revised: 31.07.2014

Citation: S. B. Vakarchuk, A. N. Shchitov, “Estimates for the error of approximation of functions in $L_p^1$ by polynomials and partial sums of series in the Haar and Faber–Schauder systems”, Izv. RAN. Ser. Mat., 79:2 (2015), 45–76; Izv. Math., 79:2 (2015), 257–287

Citation in format AMSBIB
\Bibitem{VakShc15} \by S.~B.~Vakarchuk, A.~N.~Shchitov \paper Estimates for the error of approximation of functions in $L_p^1$ by polynomials and partial sums of series in the Haar and Faber--Schauder systems \jour Izv. RAN. Ser. Mat. \yr 2015 \vol 79 \issue 2 \pages 45--76 \mathnet{http://mi.mathnet.ru/izv8094} \crossref{https://doi.org/10.4213/im8094} \mathscinet{http://www.ams.org/mathscinet-getitem?mr=3352590} \zmath{https://zbmath.org/?q=an:06443923} \adsnasa{http://adsabs.harvard.edu/cgi-bin/bib_query?2015IzMat..79..257V} \elib{https://elibrary.ru/item.asp?id=23421422} \transl \jour Izv. Math. \yr 2015 \vol 79 \issue 2 \pages 257--287 \crossref{https://doi.org/10.1070/IM2015v079n02ABEH002742} \isi{http://gateway.isiknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&DestLinkType=FullRecord&DestApp=ALL_WOS&KeyUT=000353635400003} \elib{https://elibrary.ru/item.asp?id=24513473} \scopus{https://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-84928714603}


text:
0
Research Papers

# A Study of Acoustic Wave Resonance in Water-Filled Tubes With Different Wall Thicknesses and Materials

[+] Author and Article Information
Alireza Mokhtari

Department of Mechanical Engineering,
University of Manitoba,
75A Chancellors Circle, Winnipeg, MB R3T 5V6, Canada
e-mail: ummokhta@myumanitoba.ca

Vijay Chatoorgoon

Department of Mechanical Engineering,
University of Manitoba,
75A Chancellors Circle, Winnipeg, MB R3T 5V6, Canada
e-mail: vijay.chatoorgoon@umanitoba.ca

1Corresponding author.

Manuscript received July 3, 2015; final manuscript received February 1, 2016; published online June 17, 2016. Assoc. Editor: Mark Anderson.

ASME J of Nuclear Rad Sci 2(3), 031011 (Jun 17, 2016) (14 pages) Paper No: NERS-15-1144; doi: 10.1115/1.4032781 History: Received July 03, 2015; Accepted February 01, 2016

## Abstract

Acoustic resonance of a fluid-filled tube with closed and open outlet ends for zero and turbulent mean flows is investigated both experimentally and numerically for different wall materials and thicknesses. The main goal is to create a data bank of acoustic wave resonance in fluid-filled tubes at a frequency range of 20–500 Hz to validate and verify numerical prediction models used by the nuclear industry and to determine if there is a better method with existing technology. The experimental results show that there is a strong effect of turbulent flow, wall material, and wall thickness on resonant amplitudes at frequencies above $∼250 Hz$. A numerical investigation is performed solving the linear wave equation with constant and frequency-dependent damping terms and a computational fluid dynamic (CFD) code. Comparing the one-dimensional (1D) and CFD results shows that CFD solution yields better predictions of both resonant frequency and amplitude than the 1D solution without the need for simplified added damping methods, which are required by the 1D methodology. This finding is valid especially for frequencies higher than $∼300 Hz$.

<>

## Figures

Fig. 1

Schematic diagram of the experiment

Fig. 2

Comparison between results of the “6.13 m long 10 mm OD SS closed-end experiment,” LWS and CFD predictions. (a) First resonant mode, (b) second resonant mode, (c) third resonant mode, and (d) fourth resonant mode

Fig. 3

Comparison between results of the “6.13 m long 12 mm OD SS closed-end experiment,” LWS and CFD predictions. (a) First resonant mode, (b) second resonant mode, (c) third resonant mode, and (d) fourth resonant mode

Fig. 4

Prediction methods RMSE for SS and Al tubes: (a) Frequency and (b) amplitude

Fig. 5

Resonant amplitude prediction relative errors for SS tubes

Fig. 6

Comparison between results of the “6.13 m long 12 mm OD Al closed-end experiment,” LWS and CFD predictions. (a) First resonant mode, (b) second resonant mode, (c) third resonant mode, and (d) fourth resonant mode

Fig. 7

Resonant amplitude prediction relative errors for Al tube

Fig. 8

Radial profiles of the computed axial velocity with CFD at two different resonant frequencies for a period of time

Fig. 9

Comparison between no flow and turbulence results of the “6.13 m long 10 mm OD SS open-ended experiments” at (a) 1.46, (b) 2.54, and (c) 4.65 m

Fig. 10

Comparison between zero mean flow results of the “10 mm OD SS open-ended experiments at 1.46 m,” LWS and CFD predictions. (a) First resonant mode, (b) second resonant mode, (c) third resonant mode, and (d) fourth resonant mode

Fig. 11

Comparison between zero mean flow results of the “10 mm OD SS open-ended experiments at 2.54 m,” LWS and CFD predictions. (a) First resonant mode, (b) second resonant mode, (c) third resonant mode, and (d) fourth resonant mode

Fig. 12

Comparison between zero mean flow results of the “10 mm OD SS open-ended experiments at 4.65 m,” LWS and CFD predictions. (a) First resonant mode, (b) second resonant mode, (c) third resonant mode, and (d) fourth resonant mode

Fig. 13

Resonant amplitude prediction relative errors for zero flow

Fig. 14

Zero mean flow amplitude prediction RMS: (a) frequency and (b) amplitude

Fig. 15

Resonant amplitude prediction relative errors for turbulent flow

Fig. 16

Radial profiles of the computed axial velocity with CFD at the fourth resonant frequency, at P3. (a) Turbulent flow and (b) zero mean flow

Fig. 17

Turbulent kinetic energy and turbulence eddy dissipation at the fourth resonant frequency, at P3

## Discussions

Some tools below are only available to our subscribers or users with an online account.

### Related Content

Customize your page view by dragging and repositioning the boxes below.

Related Journal Articles
Related Proceedings Articles
Related eBook Content
Topic Collections


text:
## Cryptology ePrint Archive: Report 2019/661

Mind the Portability: A Warriors Guide through Realistic Profiled Side-channel Analysis

Shivam Bhasin and Anupam Chattopadhyay and Annelie Heuser and Dirmanto Jap and Stjepan Picek and Ritu Ranjan Shrivastwa

Abstract: Profiled side-channel attacks represent a practical threat to digital devices, thereby having the potential to disrupt the foundation of e-commerce, Internet-of-Things (IoT), and smart cities. In the profiled side-channel attack, adversary gains knowledge about the target device by getting access to a cloned device. Though these two devices are different in real-world scenarios, yet, unfortunately, a large part of research works simplifies the setting by using only a single device for both profiling and attacking. There, the portability issue is conveniently ignored in order to ease the experimental procedure. In parallel to the above developments, machine learning techniques are used in recent literature demonstrating excellent performance in profiled side-channel attacks. Again, unfortunately, the portability is neglected. In this paper, we consider realistic side-channel scenarios and commonly used machine learning techniques to evaluate the influence of portability on the efficacy of an attack. Our experimental results show that portability plays an important role and should not be disregarded as it contributes to a significant overestimate of the attack efficiency, which can easily be an order of magnitude size. After establishing the importance of portability, we propose a new model called the Multiple Device Model (MDM) that formally incorporates the device to device variation during a profiled side-channel attack. We show through experimental studies, how machine learning and MDM significantly enhances the capacity for practical side-channel attacks. More precisely, we demonstrate how MDM is able to improve the results by $>10\times$, completely negating the influence of portability.

Category / Keywords: Side-channel attacks, Machine learning, Portability, Overfitting, Multiple Device Model

Date: received 4 Jun 2019, last revised 12 Jun 2019

Contact author: picek stjepan at gmail com, annelie heuser@irisa fr, sbhasin@ntu edu sg, anupam@ntu edu sg, djap@ntu edu sg

Available format(s): PDF | BibTeX Citation

Short URL: ia.cr/2019/661

[ Cryptology ePrint archive ]


text:
## A Brauer-Clifford-long group for the category of dyslectic Hopf Yetter-Drinfel'd $(S,H)$-module algebras

### Summary

Brauer-Clifford groups are equivariant Brauer groups for which a Hopf algebra acts or coacts nontrivially on the base ring. Brauer-Clifford groups have been established previously in the category of modules for a skew group ring $S\#G$, the category of modules for the smash product $S\#H$ over a cocommutative Hopf algebra $H$, and its dual category of ($S,H$)-Hopf modules $_S\Cal M^H$ over a commutative Hopf algebra $H$. In this article the authors introduce a Brauer-Clifford group for the category of dyslectic Hopf Yetter-Drinfel'd ($S,H$)-modules for an $H$-commutative base ring $S$ and quantum group $H$. This is the first such example in a category of modules for a quantum group, and it gives a new example of an equivariant Brauer group in a braided monoidal category.

### Mathematics Subject Classification

16W30, 16K50, 16T05, 18D10

### Keywords/Phrases

Hopf algebras, Yetter-Drinfel'd modules, braided monoidal categories, Brauer groups