The Same Fact, Twice.

The ninth lands

The identity of Srinivasan's that the last note recorded as lost came back: its branch was rebuilt that evening and the pull request reopened. For two Markov triples (a₁, b₁, c) and (a₂, b₂, c) that share a coordinate, (a₁a₂ − b₁b₂)(a₁b₂ − b₁a₂) = c²(a₁b₁ − a₂b₂). It comes from Anitha Srinivasan's 2009 paper on Markov numbers and ambiguous classes, and it is pure algebra: nothing about positivity, and nothing about which coordinate is largest.

Its one import is the module that put the Markov equation into the corpus on 17 August. Only one other module imports that equation directly: the descent step accepted on 21 September, through which every module of the tree development reaches it. The collision arithmetic has no use for the tree, and the new module does not touch it.

The same fact, twice

Late on Friday evening two submissions were opened forty-six seconds apart from the same contributor's fork. Both prove that −1 is a square modulo every Markov number m. The first says it in the integers modulo m, obtains it from Mathlib's theorem on primitive sums of two squares, and adds the classical corollary that no prime factor of a Markov number is congruent to 3 modulo 4. The second says there is an integer r with r² ≡ −1 (mod m), and obtains it from the Bezout lemma the same contributor had landed earlier that evening. The first one's claim says it combined the accepted interfaces rather than duplicating their proofs. It did. The duplication was one level up.

The receiver accepted both, correctly by its own rules. It compares each new statement with Mathlib and with the corpus, exactly, after elaboration, and runs a handful of bounded tactics to catch statements that are trivial. Two notations for one fact are two statements to it. Deciding whether two statements say the same thing is not something it attempts. The corpus now holds a result twice, and the only reason anyone knows is that a person read both.

It also moved the series. The second module's four imports tie the largest number of edges a single submission has added, and they lifted edges per module from 0.78 to 0.81, the largest step of the day, for a result the corpus already had. Field Note 16 made the same point about agents that go looking for unconnected modules. The series counts imports; it cannot tell a new result from an old one reached by a longer road.

On Friday the contributor asked whether projects like this one coordinate to avoid duplicated work. This is the smallest version of that problem: two efforts forty-six seconds apart, from the same place, and nothing between them that noticed.

Modulo four

The fourth submission starts from Wednesday's theorem that every positive Markov triple is reached from (1, 1, 1) by Vieta moves. The moves preserve four residue patterns modulo 4: (1, 1, 1) and the three arrangements of (2, 1, 1). So every positive triple has one of them, and an even coordinate is 2 modulo 4 while the other two are 1. The known statement is sharper, 2 modulo 32 for an even Markov number, but the claim says what this one is for: Markov numbers of the form 2pᵏ, a case Srinivasan's paper treats alongside prime powers.

Nine deep

The first of the two square-root modules extends the corpus's deepest chain to nine modules: the Markov equation, the descent step, the path layer, the orientation, the Stern–Brocot bridge, the injectivity of that embedding, the Markov-number label, the divisibility that comes from the equation, and the residue. The first was accepted on 17 August. The other eight are the external contributor's, seven of them from the last four days.

By half past twelve the corpus was at 87 modules and 71 internal import edges, 0.82 per module, and the most-imported module, the Stern–Brocot bridge, still had four consumers.

By hand

None of the four went through the merge queue. The maintainer did what the queue does, one pull request at a time: bring the branch up to date, wait for the receiver to run again, merge, wait for the two automated commits that follow every merge, move on. From the first branch update to the last merge took a little over three hours.

Three of the four branches were brought up to date less than a minute before the previous merge's automated commits landed. Each fell behind again at once, and had to be updated and revalidated a second time. The queue waits for those commits before it touches the next branch, and this is why. Its comments say it automates the waiting and never the decision. The waiting turns out to be the part a person gets wrong.