Express spectroscopy characterization theorem

[benkeks]

Write down Theorem 1.

(This is not yet about actually proving the theorem, but about bringing together #4, #7, #5, #2, and #9.)

• [x] Statement 1
• [x] Statement 2

[TheHllm]

We can now express the 2nd statement via

in_wina e (Attacker_Immediate p Q)

in #9.

[betawave]

With

28 and #56

we can now complete the statement of theorem 1: ∃φ ∈ 𝒪 e. distinguishes_from φ p Q = in_wina e (Attacker_Immediate p Q)

[benkeks]

Very cool, anyone wanna have the privilege of writing this down in a branch & pull request? =)