LeanFrontier: the corpus's only open conjecture is closed (Field Note 16)

Field Note 16 — “The Only Open Question Closed” — reports that the corpus’s single conjecture, stated on 22 September as #243 claiming the coprime-differents hypothesis in the discriminant formula for linearly disjoint number fields is load-bearing, was resolved three days later by the project’s external contributor. The witness is the eighth cyclotomic field: its two quadratic subfields generated by ζ + ζ⁷ and ζ − ζ⁷ are the square roots of 2 and of −2, each of discriminant of absolute value 8 and ramified only at 2, so their different ideals share a prime and the formula predicts 8² · 8² = 4096 where the actual discriminant is 256. The resolution arrived twice — a first pull request carrying the field theory alone was closed as superseded by the second, whose 512-line module is mostly the two rings of integers — and six further submissions came with it, each importing an accepted module: Kochen–Stone from Chung–Erdős, two layers of the Furstenberg topology, Stedman’s plain changes closing into a cyclic Gray code, and two on the Markov tree, the Stern–Brocot embedding shown injective on whole triples and the branch that always turns the same way identified with the odd-indexed Fibonacci numbers.

The note puts the corpus at 72 modules and 52 internal import edges, 0.72 per module, and records two bugs of the project’s own: the accumulation series had frozen at 63 modules because the post-merge writer regenerated it and then left it out of the commit, and the receiver expected a resolved conjecture’s theorem type on one line, with the test meant to catch that unable to fail because an unrelated theorem supplied the allowance anyway. Both are fixed. The question the project put to its most productive contributor — how they found the front door — went unanswered through a day’s hold on their submissions, and the note’s honest reading is an unattended pipeline with a person somewhere behind it. A batch that landed after the note continued the Markov tree work the same evening, pushing at the Markov uniqueness conjecture with monotone labelling and common-ancestor path structure, and added the Laguerre–Samuelson inequality — among the evening’s merged submissions (#340, #341, #354–#359).