Servers in dawn-dusk orbit

Posted on 25 September 2026 by John

Despite the predictions that no one would ever put build data centers in space, Google is starting on Thursday. Google’s prototype satellite will be one of 130 payloads on SpaceX’s Transporter 18 mission on October 1.

The server will follow a dawn-dusk orbit, a special case of a sun-synchronous orbit (SSO), following the terminator line between daylight on dark on the earth below. A dawn-dusk orbit allows the satellite’s solar panels to stay in nearly continuous daylight, while also being in a relatively inexpensive low earth orbit (LEO). Geostationary orbit (GEO) would allow solar panels to always receive sunlight, but launching a satellite into GEO requires more fuel and so is more expensive.

Another advantage of LEO is that radiation levels are a couple orders of magnitude less than at GEO. Lower radiation means electronics do not need to be as hardened against radiation.

A dawn-dusk orbit would not be possible if the earth were perfectly spherical. The earth’s equatorial bulge makes it possible to design an orbit that precesses once per year. David Hammen explains this in an answer to a question on the Space Exploration Stack Exchange site.

If the Earth had a spherically distributed gravitational field, a satellite’s right ascension of ascending node would be constant. … Fortunately, the Earth’s gravitational field is not spherical. The Earth’s rotation results in an equatorial bulge. This equatorial bulge causes RAAN to precess (or recess). …

Sun synchronous orbits are chosen so that RAAN precesses by 360 degrees per year, or a bit less than one degree per day. …

A dawn-dusk satellite is a special case of a sun synchronous orbit. … A dawn-dusk orbit typically does not quite follow the terminator. Following the terminator would require a rather high orbit.

Nathaniel Bowditch

Posted on 22 September 2026 by John

A couple days ago a friend told me about the book Carry On, Mr. Bowditch, a fictional account of the life of Nathaniel Bowditch (1773–1838). I’ve been listening to the book on Audible, and apparently it’s only lightly fictionalized.

Bowditch was a self-educated mathematician and astronomer, best known for his book The American Practical Navigator, first published in 1801. The book has been continually revised over the last two centuries and is still in print, available for download from the National Geospatial-Intelligence Agency. The latest edition begins with a brief account of Bowditch’s life, confirming the essential details of the fictional biography.

Two things stand out about Bowditch: his attention to detail and his desire to make ideas accessible. He taught himself Latin in order to read Newton’s Principia and followed the text so closely that he found a number of errors.

Bowditch’s navigation book grew out of the numerous corrections he made to error he found in John Hamilton Moore’s The Practical Navigator, the leading navigation text of the time.

At the beginning of the 19th century it was theoretically possible to determine time, and hence longitude, from lunar observation. However, the method required ideal observation conditions and laborious calculation. Bowditch developed a way to make the necessary measurements under more general conditions, and simplified the necessary calculations. According to the biographical preface mentioned above,

Bowditch vowed while writing this edition [of his navigation text] to “put down in the book nothing I can’t teach the crew,” and it is said that every member of his crew including the cook could take a lunar observation and plot the ship’s position.

After completing The American Practical Navigator, Bowditch began an English translation of Pierre Laplace’s encyclopedic Mecanique Celeste, filling in details to make the work accessible to a wider audience. He was able to translate four out of the five volumes by the end of his life.

Phone words

Posted on 17 September 2026 by John

I recently bought a copy of Los Alamos Rolodex, a book displaying business cards from Los Alamos Nation Labs from 1967 to 1978. You can find some examples of the cards here.

One of the cards in the book is for Eugene Frank, President of B & F Instruments. His card lists his phone number as

(215) MErcury 9-7100

At first glance I thought the “E” in “MErcury” had been accidentally capitalized. Then I realized the intention was that someone would dial ME (i.e. 63) and ingore “rcury”. So the phone number would be (215) 639-7100.

This card was from 1968, the height of the space race. Maybe the card was alluding to the Project Mercury or the planet Mercury, or both. [1]

The telephone keypad mapping (ITU E.161 standard) is a poor attempt at making phone numbers more memorable. For starters, there’s no way to encode 0 or 1 [2]. It’s unlikely a phone number will correspond to anything memorable unless you come up with the word first and then try to obtain the phone number, such as 800 FLOWERS.

Inserting extra letters, as Mr. Frank did, greatly increases the chances of encoding a phone number as a word. But then you need to denote which letters count and which ones are filler, so there’s not much advantage. Still, I wanted to play around with it for fun. I found 109 words [3] containing the letters from a telephone encoding of 4228646. (I’m using the file /usr/share/dict/words on my laptop as my list of words.)

Here are some of the more interesting hits.

semicatholicism
heartburning
gladiatorism
diabetogenic
galactogenetic
xanthocreatinine

There are over 30,000 words containing an encoding of the area code 832. One of these is traditional, and so I could write my phone number as

TraDitionAl semICAThOlIcisM.

Another choice for 832 is intercosmic, so

inTErCosmic GAlaCTOGeNetic

is another possibility.

Galactogentic can refer to the production of milk by the mammary glands or to the formation of galaxies (e.g. the Milky Way). Here intercosmic fits with the later sense.

I got greedy and tried to find a word containing the full phone number, 8324228646, but didn’t find anything.

Here’s my business card in the style of the Los Alamos Rolodex cards, created by Grok, using (832) GlAdiATOrIsM as the phone number.

Now suppose you remembered “gladiatorism” but not which letters were capitalized. Then you’d have to try up to 792, i.e. 12 choose 7, possible numbers, so this really isn’t a practical mnemonic. If you remembered “traditional semicatholicism” without capitalization it would be worse, with over a million possibilities (11 choose 3 times 15 choose 7). Some possibilities are counted twice, since different ways of selecting letters can lead to the same phone number, but still there are too many possibilities to try.

[1] Thanks to Andrew for pointing out in his comment that it was common at one time to encode the first two numbers of the exchange (the second triplet of numbers in a phone number) as letters, and assign a word to those letters. Sometimes this was standardized, such as Pennsylvania 6 for 736, an example made famous by Glenn Miller. But from what I can tell, not all exchanges had standard names, and proposed standards weren’t always adopted in practice.

In the example above, I don’t know whether it was common to encode 639 as Mercury 9, or even ME 9, or whether Mr. Frank chose this. It was common chose some encoding for the first two numbers of the exchange, though that practice was going away by 1968. Perhaps Mr. Frank was an older man who retained a habit he acquired when it was more common. None of the other cards in the book spelled out the exchange.

Update: Thanks to Chuck for pointing out this list of recommended words for exchanges. Note that there are multiple suggestions for most exchanges, including six for 63X.

[2] Not only are there no letters for 0 and 1, the letters O and I represent digits. At one point in time the first digit of an exchange (the middle three digits) could not be a 0 or 1, but these digits could appear anywhere else.

[3] I initially found a list of 185 words, but some of these were duplicates: a word can represent a phone number in more than one way.

Guessing the meaning of a number

Posted on 14 September 2026 by John

Suppose I give you an n-digit number and ask you what it represents. This seems impossible, and in theory it is impossible. But in practice it’s often possible.

Apps on a phone may automatically interpret a 10-digit number as a phone number or a 16-digit number as a package tracking number. And very often these interpretations are correct, given the kinds of things most people use their phones for.

It’s not surprising that a 10-digit number on a phone is a phone number. It’s more interesting that a 16-digit number is likely a tracking number. It could be other things, such as a credit card number. But people don’t usually write out credit card numbers in a text note; credit card numbers likely saved in some more opaque way.

I run into a variation of this problem routinely, trying to infer what a number represents inside medical notes.

A five-digit number could be a US postal code, or it could be a medical procedure code.

A six-digit number could be a date in MMDDYY format, or it could be a medical record number.

A ten-digit number could be a phone number, or it could be an NPI (National Provider Identifier) number.

It’s interesting that it’s possible make a good guess at what a number means inside unstructured text. Context has been lost, but not all context: you know you’re looking at medical notes. And that meager bit of context can be surprisingly useful.

Bayesian OCR

Posted on 10 September 2026 by John

The Greek letter β (beta) and the German letter ß (eszett) look similar, especially in some fonts.

Now suppose an OCR program sees some character that could be a beta or could be an eszett. It could calculate some kind of distance between between the pixel pattern of the character and the pixel patterns of beta and eszett. But that would be discarding context.

If you’re scanning a Greek document and run into a beta-like symbol, it’s very likely a beta. If you’re scanning a German document and run into a beta-like symbol, it could be a beta. For example, it could be a scientific paper that mentions beta particles or beta carotene. But most likely the symbol is an eszett.

The previous paragraph is saying you should compute the conditional probability of a set of pixels representing a character given the language of the document. You could be more sophisticated and look at the position of the symbol in a word as well. For example, if you see a symbol at the end of a Greek word that could either be ο (omicron) or σ (sigma), it’s likely an omicron because Greek has a different symbol ς for final sigma.

This post is a follow-on to my earlier post on the error rate in Google’s Ngram database. OCR errors are fairly common in that database, so why don’t they “just” fix the errors by using some sort of Bayesian method? OCR software probably does use some sort of Bayesian method, but it’s not that simple.

In that post I looked at the use of the word grok in English. The Ngram database shows the word being used before it was coined in 1961 due to OCR errors. Why didn’t Google compute the probability of a word being “grok” conditional on the publication date? That would be circular. We happen to know exactly when grok was coined, but in general we might try to determine when a word was coined by looking at a large set of scanned books, like the Ngram database!

Now we could compute the probable value of an ambiguously scanned word by conditioning on the language of the surrounding text. That would be a reasonable thing to do in general, but it could also lead to exactly the kind of errors we see in the Ngram data for grok.

Suppose you see an ambiguously scanned word in a book written in English. There is a higher prior probability that the word is an English word than a German word. Now suppose you see “gro?” where ? could be β, ß, or k. Without any context, perhaps the probability of the symbol being a k is small. But grok is an English word and groß is a German word which may lead you to conclude “?” is a k and the ambiguous word is grok.

Assigning higher prior probability to English words in English texts is the best thing to do on average, but in particular instances it will lead to errors. That’s life.

The Ngram database includes millions of scanned books. Google had to use OCR algorithms that work well on average. A linguist with a special interest in a particular word can be more careful and create a more sophisticated probability model (explicit or implicit) customized for their interests. Google did what they could operating at such a large scale.

The part of Navier-Stokes no one is talking about

Posted on 9 September 2026 by John

Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.

Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.

Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious. In 2005, Henk Barendregt and Freek Wiedijk wrote

To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.

That was the rule of thumb: forty hours per page. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.

Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.

I’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.

Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.

Ngram error rate

Posted on 7 September 2026 by John

The Online Etymological Dictionary gives the following etymology for grok:

grok (v.)

“understand empathically,” 1961, an arbitrary formation by U.S. science fiction writer Robert A. Heinlein (1907-1988) in his book “Stranger in a Strange Land.” In the book it is a transliteration of a Martian word and is said to mean etymologically “to drink.” It attained popular use in 1960s-70s counterculture but is perhaps obsolete now except in internet technology circles.

I don’t believe anything in the statement above is disputed. And yet Google’s Ngram Viewer tells a very different story.

The plot implies that use of the word grok had been increasing before Heinlein’s book came out and is now much more common than it was in the 1970s. Note that the plot ends before the Grok AI came out in late 2023.

Apparently the Ngram data is unreliable, mainly for two reasons: OCR errors and inaccurate date attribution. Presumably the blip around 1900 was due to the former, OCR causing words like crok or grog to be cataloged as grok. And presumably the rise in usage before 1961 was due to the latter, misattributing the date of sources published after 1961.

The supposed rise in usage before 1961 is interesting. You’d expect some lag between the time a word circulates in conversation and when it appears in books, but apparently this lag can be smaller than the effect of date misattribution.

Etymonline speculates that grok is “perhaps obsolete now except in internet technology circles.” That matches my experience. Even in technological circles, the word was uncommon before Grok was released. Maybe it was more common in print than in conversation.

Previous posts with Ngram stats. The effects are so large that they’re probably directionally correct after adjusting for a substantial error rate.

Hugging Face Easter Egg

Posted on 3 September 2026 by John

NVIDIA has offered to buy Hugging Face for $12,930,300,000.

129303 is the Unicode code point for the Hugging Face emoj (U+1F917), which you can verify with the following Python code.

>>> import unicodedata
>>> 129303 == 0x1F917
True
>>> unicodedata.name(chr(0x1F917))
'HUGGING FACE'

Hugging Face emoji

Three-term recurrences

Posted on 24 August 2026 by John

There many examples of families of functions where each function can be computed as a linear combination of the two previous terms

$f_{n+1}(x) = a(x) f_n(x) + b(x) f_{n-1}(x)$

where a and b are functions of x and possibly n. This is called a three-term recurrence formula.

It’s amazing how often you can run into three-term recurrence formulas. There are theorems that give conditions for such recurrences to hold, but I haven’t reached the bottom of that rabbit hole [1].

For this post I just want to give examples.

NB: before using any of the recurrences below, see the next post for a numerical pitfall to avoid.

Bessel functions of the first and second kind:

$\begin{align*} J_{\nu+1}(x) &= \frac{2\nu}{x}\,J_\nu(x) - J_{\nu-1}(x) \\ Y_{\nu+1}(x) &= \frac{2\nu}{x}\,Y_\nu(x) - Y_{\nu-1}(x) \end{align*}$

Modified Bessel functions of the first and second kind:

$\begin{align*} I_{\nu+1}(x) &= I_{\nu-1}(x) - \frac{2\nu}{x}\,I_\nu(x) \\ K_{\nu+1}(x) &= K_{\nu-1}(x) + \frac{2\nu}{x}\,K_\nu(x) \end{align*}$

Chebyshev polynomials of the first and second kind:

$\begin{align*} T_{n+1}(x) &= 2x\,T_n(x) - T_{n-1}(x) \\ U_{n+1}(x) &= 2x\,U_n(x) - U_{n-1}(x) \end{align*}$

Hermite polynomials (physicists’ convention):

$H_{n+1}(x) = 2x\,H_n(x) - 2n\,H_{n-1}(x)$

Legendre polynomials:

$P_{n+1}(x) = \frac{2n+1}{n+1}\,x\,P_n(x) - \frac{n}{n+1}\,P_{n-1}(x)$

[1] See Bochner’s theorem for orthogonal polynomials, the Nikiforov–Uvarov method, and Infeld-Hull factorization.

How NASA’s Mariner 9 probe encoded images

Posted on 13 August 2026 by John

NASA set Mariner 9 to photograph Mars in 1971. The images had to be encoded for transmission using an error-correcting code, otherwise they would be significantly corrupted when they were received on Earth.

The images were encoded for transmission using a code based on Hadamard matrices, specifically a (32, 6, 16) Hadamard code. This means that each 6-bit pixel value was encoded as a 32-bit code word, with all code words differing in at least 16 positions.

The previous post explained a way to construct Hadamard matrices of order 2ⁿ. Use this process to create a 32 × 32 Hadamard matrix H and create a 64 × 32 matrix M by stacking H on top of −H. Then form a matrix M′ by changing all the −1 entries to 0. The rows of M′ are the code words.

For a 6-bit photo pixel value, one of the bits determines whether to read a code word from the top half or bottom half of M′. The other five bits determine which row to choose.

So a pixel is transmitted as a 32-bit codeword c, one of the 64 rows of M′. Ideally c would be received, but possibly some corrupted versions c′ is received with some of bits flipped.

Replace all the 0’s in c′ with −1 to create c″. Now multiply M by c″, thinking of the latter as a column vector. This yields a column vector of length 64. The largest component of this vector corresponds to the row of M′ that was most likely sent.

To see this, suppose there was no corruption: c was transmitted and c was received. Then the product Mc″ has a 32 in the entry corresponding to c and zeros everywhere else. If no more than 7 bits in c were corrupted, the row with the largest entry corresponds to the row that was transmitted.

In practice the product Mc″ can be computed using an algorithm analogous to the FFT using fewer operations than it would take to multiply a general 64 × 32 matrix by a 32 × 1 matrix.

Uncategorized

Servers in dawn-dusk orbit

Related posts

Nathaniel Bowditch

Related posts

Phone words

Related posts

Guessing the meaning of a number

Bayesian OCR

Related posts

The part of Navier-Stokes no one is talking about

Related posts

Ngram error rate

Related posts

Hugging Face Easter Egg

Related posts

Three-term recurrences

How NASA’s Mariner 9 probe encoded images