Blog [0005]

A “color scheme” isn’t just a set of colors found randomly via a search engine or produced by a generator. Most such schemes are just a collection of color blocks and RGB values. They might look okay at first glance, but for a non-professional like me, it’s hard to directly apply them to actual designs. This is just a mere collection of colors, not a truly usable color scheme. For me, a color scheme should meet these criteria:

• Clearly defines the purpose of each color, such as background color, text color, accent color, etc.

• Based on the defined color purposes, meets certain accessibility standards, including:

  • Sufficient contrast between text and background.
  • Colorblind-friendly.

After several fruitless attempts, I decided not to waste time on search engines anymore. My inspiration came one day when I was staring at my Emacs. At that moment, I suddenly realized that code editor color schemes are arguably a perfect solution because they:

• Have very clear color purposes.
• Usually don’t have too many primary colors.
• Every code editor has a huge number of color schemes to choose from.
• These schemes are usually carefully designed rather than randomly generated.
• Many schemes meet certain accessibility requirements.
• You can experience the effect of these schemes right in the code editor.
• Provide a sense of visual unity with one’s daily workflow.

The only concern is the copyright issue. Although colors themselves are not protected by copyright (at least as far as I know), to avoid unnecessary trouble, one should try to use schemes that are explicitly licensed for use.

Palette Tester is a tool for testing the contrast of a color scheme. It can test contrast under WCAG 2.1 (AA) or APCA Contrast standards. Coloring for Colorblindness and Who Can Use are two tools for testing the colorblind-friendliness of colors. They can show how the same set of colors appears to people with different types of color blindness.

I have always used the Modus Themes color scheme in Emacs. Coincidentally, this color scheme was designed with accessibility in mind, achieving the WCAG AAA standard, and provides variants friendly to two types of color blindness (deuteranopia and tritanopia). The color scheme of the webpage you are currently viewing comes from the tinted variant of Modus Themes.

Before the function it self, there are some auxiliary functions that need to be defined.

First we come up with the quotient and remainder functions. For all , let and be the quotient and remainder of divided by , respectively, if , and otherwise.

Then follows the (floored) square root and exceedence functions. For all , let be the largest number that , and .

Now comes the and functions, named after what Gödel named them. Let , and . The definitions may seems weird at first glance, but they would soon show their power. And they have great properties: for all , and . The proof goes as follows.

For that property of and , it suffices to show that , and this can be brought out by the fact that

That property of and is also easy following similar approach. These two properties means that the arguments of can be extracted from the result of it, and that means is an 1-1 function.

Finally, the Gödel’s β function is defined by . (Note that this is not the original definition (3-ary) but a simplified 2-ary one.) The definition is also a bit of complicated, but the following lemma tells us about why it is amazing.

For all , there exists a such that

for all .

And the the proof entails an algorithm to calculate such an .

Before the proof, we need to prove two preliminary propositions.

(Note that this lemma is a weaken version of the original theorem.)

If and they are coprime, then for some integers and .

Proof: Let , i.e. the set of all positive (integral) linear composition of and . Thus there must be a minimum value for this non-empty set (the non-emptiness is trivial). What this proof wants to show is that . We prove this by contradiction. Assume that . Take , let , we have . And since and are both (integral) linear composition of and , so must be , otherwise it contradicts with the minimality of . Then we have for all . Note that and , so is a common divisor of and , which leads to the contradiction toward the coprimality of and if .

For all , if are pairwise coprime and for all , then there exists a such that for all .

Proof: For each , let . Since are pairwise coprime, and are coprime. By Bézout’s Lemma, there are integers and such that . The insight here is that for each , we construct the number that its remainder divided by is , and compose these constructed numbers in a way that they won’t affect each other. Note that cannot be divided by , can be divided by for any where , and there is an on the right hand side of the equation we got from the Bézout’s Lemma. It is easy to see that, now it suffices to take

where is any natural number such that .

Finally we come to the proof of the lemma. From the definition of and , we can see that we only need to find a proper value of such that the numbers for each coprime, then construct the value of by Chinese Remainder Theorem, and calculate the . For convenience, denote by for each .

What conditions should the value of satisfy? First, it must make , which is one of the conditions asked by Chinese Remainder Theorem. Second, it makes those ‘s pairwise coprime. To prove propositions like ‘there is no prime such that and for different ‘, consider proof by contradiction. Think about what if there is some prime such that and for different , i.e. and . Assume without loss of generality, we have . It will be good if we have , which would lead to the contradiction that . So things become evident: find a construction of such that . This can be achived by making divisible by the product of all the possible values of , which ranges from to . This is to say, making would be a good idea. With the first condition that should satisfy, it suffices to take , where . I take instead of there for better elegance with the same effect.

The above is not a strictly stated proof, however it is easy to rewrite it into one.

The reason I write this post is not that the ability of Gödel’s β Function to encode a finite sequence into a number is amazing (there are many other techniques to achive this, e.g. encode the sequence into the exponents of an initial segment of primes), nor that the proof is elegant (though it is). It is just because I recalled the confusion that those two preliminary propositions caused to me, and realized that they seems easy for me now, and can be used to prove such lemmas. This feels strange, so I decided to write it down.