One Lemma of Its Own.

An identity found on the way

On Saturday afternoon the contributor's agent submitted an identity it had derived, by its own account, during exploratory work on reductions toward Markov uniqueness; the operator then asked for it to be formalized and submitted. For coprime integers x and y and odd M, the quadratic pair x² + y² + 3Mxy and y² − x² has exactly the same common divisors as the linear pair 3Mx + 2y and 3My + 2x, so the two pairs have the same greatest common divisor. The sum of the quadratic pair is y(3Mx + 2y) and their difference is x(3My + 2x). Coprimality of x and y carries a common divisor from the quadratic pair to the linear one, and M being odd carries it back. The Markov equation is not used.

Most claims in the corpus end with the sentence "No claim of new mathematics is made." This one ends "No claim of publication-level novelty is made", the only claim worded that way. The wording is right. The identity may well appear nowhere in this form. It is also a few lines of algebra, of the kind someone working on the problem writes in a margin and does not publish.

And it stands apart. It imports nothing from the corpus and nothing imports it, so it added a module and no edges, and edges per module dipped.

The prime-power step

The Sunday-morning submission builds on Saturday's collision identity. Take two Markov triples that share a coordinate c, with the relevant coordinates prime to c as they are in positive triples, and an odd prime p dividing c. The two factors in that identity cannot both be divisible by p, so if pᵏ divides c, then p²ᵏ divides one factor entirely. In the language of the week's other modules, the two alternatives are the two triples carrying the same square root of −1 modulo pᵏ, or opposite ones.

It is the arithmetic core of the elementary proofs that a Markov number which is a prime power determines its triple. That case has been known since the work of Baragar, Button and Schmutz around the turn of the century, with shorter proofs by Lang and Tan and by Zhang in 2007, and an elementary one by Srinivasan in 2009, which is the one these modules follow. The pull request names the next two: uniqueness for odd prime powers, and the case 2pᵏ, both already passing the receiver in the contributor's fork and waiting for this one. If they land, the corpus will hold the known partial results on the conjecture it states. Not the conjecture.

What six submissions add up to

Read in order, the Markov submissions since Friday formalize one line of the literature: a square root of −1 modulo every Markov number, the collision identity, the residues modulo four, the prime-power split. Five of the six claims end by saying their mathematics is not new, and they are right. The sixth is the gcd identity, and it is the piece nothing depends on.

That is a plausible place for something new to turn up first: a small lemma pulled out of exploratory work, before anyone knows whether it is useful. It is also a limit of the accumulation series worth stating plainly. The series counts imports. It cannot tell a chain of textbook steps from a new idea, and this week it recorded a great deal of the first and very little of the second.

With those two the corpus stood at 89 modules and 72 internal import edges, 0.81 per module. The deepest chain is nine modules, and the most-imported module still has four consumers.

Two more before the note went up

While this note was being drafted, two submissions outside the Markov line were merged. The first is about OEIS A053067, a sequence whose terms are formed by writing decimal numbers side by side. For every modulus m, infinitely many terms are congruent to 1 modulo m, so no finite set of congruence obstructions can rule out further primes in the sequence. It does not find one. At 777 lines it is one of the larger modules in the corpus, and like the gcd identity it imports nothing from the corpus and nothing imports it.

The second proves that periodic points are dense for the tent map on the unit interval, and carries the result to the logistic map at parameter four through the topological conjugacy that landed on Thursday. That conjugacy completed a module a friend of the project submitted on 18 August, so this is the third layer on one piece of dynamics, and the first two came from different contributors.

The contributor also refreshed the roadmap they had written for the project. All six of its directions from Wednesday have landed, and the new version replaces them with five different ones. It moves further work on Markov uniqueness into a research-only section that asks for named results from the literature, which is a fair reading of what the week's Markov submissions were.

And one after it went up: Hlawka's inequality, that in any real inner-product space the norms of the three pairwise sums of x, y, z add up to at most |x| + |y| + |z| + |x + y + z|. It is classical, and like the A053067 theorem it neither imports anything from the corpus nor is imported.

An afternoon of geometry

Three more followed, all classical and all in one style. Weitzenböck's inequality: a triangle's area is at most (a² + b² + c²) / (4√3). Euler's quadrilateral theorem: the squared sides of any quadrilateral add up to the squared diagonals plus four times the squared distance between the diagonals' midpoints. Varignon's theorem: the midpoints of any quadrilateral's sides form a parallelogram. Each is short and rests on Mathlib alone: none imports anything from the corpus.

That makes five of the day's seven submissions that stand alone, against one of the six Markov submissions since Friday. Edges per module fell from 0.81 in the morning to 0.77, and the share of modules connected to another from 0.63 to 0.60. The accumulation series was registered to measure this, and here it measures something plain: the same producer, turned to a different kind of target, builds very differently. The corpus stands at 95 modules and 73 internal import edges.

What changed underneath

The catalogue's import graph, unreadable at ninety modules, is now drawn by Graphviz, one picture per connected group of modules. Getting there broke two things for an afternoon, both ours. A test added with it assumed the published catalogue is always current; on a submission's branch it never is, so every new submission failed a check until the test was fixed. And the merge queue, asked to merge the first of them, waited an hour on that failed check without noticing: its test for a failure could never succeed, because of how a shell pipeline reports a command's exit status. It now stops, says why, and gives up cleanly before its credentials expire.

A clarification about the last conjecture

Field Note 16 called the discriminant statement the corpus's one conjecture, and its resolution the closing of an open question. Both are true inside the corpus, and neither should be read as more. The statement was open in the protocol's sense: a proposition stated formally that the receiver's bounded tactics could neither prove nor refute. As mathematics it was known. The eighth cyclotomic field is a standard example of the discriminant formula failing when the two fields ramify at the same prime, and the claim that stated the conjecture named that witness itself and called the discriminants classical. What the resolution added was a formal computation of two rings of integers, which is real work of another kind.

The conjecture that replaced it is open in the other sense. Frobenius asked it in 1913, and it is still open.