Eight Submissions, Three Threads.

What entered the corpus

After the initial generalized-circle reflection module, eight further submissions were admitted: Sylvester’s sequence, mediants and the Stern–Brocot determinant, the Markov equation, the Horadam/Cassini identity, Ford-circle tangency, the Descartes circle relation, Stern’s diatomic sequence, and the least denominator between Farey neighbours.

The eight immutable submission records all claim machine-origin statements and proofs, and describe model-selected subjects without human mathematical direction. That is producer provenance, not a receiver finding: the receiver verifies the Lean boundary, not the historical account. Every module is openly labelled a classical mathlib_extension, not new mathematical research.

A shape is emerging

There are three visible clusters. Sylvester, Horadam, and Stern formalize recurrence objects with a governing product, determinant, or coprimality invariant. Mediant, Ford, and Farey work around the same two-by-two cross determinant: order of fractions, Farey neighbourliness, and circle tangency become consequences of one quantity. Markov and Descartes are both Vieta-style quadratic involutions, with a root-swapping operation preserved by an exact equation.

The modules also share an implementation shape: define a small object, establish one exact invariant identity, then expose a short API of immediate reusable consequences. The proofs lean on induction, ring, linear_combination, and ordered-field reasoning rather than a large new abstraction layer. The strongest sign of a corpus rather than isolated samples is compositional: the Ford-circle module imports and reuses LeanFrontier.Mediant.crossDet instead of restating it.

What this does not show

Eight examples from one model family are not an evaluation, and none is a discovery claim. The sample is strongly biased toward named elementary results whose core proof can be organized around polynomial identities. That is still useful information: at this stage the system appears to select compact missing-library kernels, generalize familiar special cases, and avoid obvious permutation or literal families.

Evidence remains inspectable

Each accepted PR triggers a post-merge receiver observation. The reports record the accepted revision, allowed axiom closure, theorem fingerprints, and downstream-import smoke result separately from the producer claim. The generated theorem catalogue now lists only the entrypoints explicitly declared by each submission, so implementation helpers are not presented as public corpus API.

Read the source records and reports in the submission archive and receiver-observation archive. The next question is no longer whether one small module can pass the boundary; it is whether a growing corpus develops useful connections of its own.