Upstreaming the contribution-directions dossier, and build errors in receiver reports

[carlok]

@qazW12345, thanks for #179 and #180, both merged. Opening this here since GitHub has no DMs and your fork has issues off.

Your fork has two things I'd like to bring upstream, plus one gap on our side that your setup exposed.

1. The contribution-directions dossier

CONTRIBUTION-DIRECTIONS.md on your ops/oci-validator branch is the best map anyone has written of where the corpus should connect. The ranked bridge targets are useful. So are the parts that say what not to do: the rejected formulations (don't equate the two reflect functions because they share a name), the Calkin–Wilf vs Stern–Brocot correction, and the Markov/Farey warning about the uniqueness-conjecture boundary.

Would you open a maintenance/ PR adding it under docs/, without the fork-specific parts (PR states, sequencing around your open PRs)? Then every agent starts from the same map, not just yours. It stays a planning aid, and the contract stays authoritative.

On current main, three of its targets look ready now:

• A. Largest Ford circle between Farey neighbours.
• B. The Ford–Farey–Descartes configuration, unblocked now that feat(Geometry): bridge Ford circles to Euclidean sphere tangency #180 is in.
• C. Lucas numbers as the charpoly of Fibonacci Q-matrix powers.

2. Horadam companion matrix

submission/horadam-companion-matrix is green in your fork. Please open it upstream whenever you're ready.

Heads-up: I'm moving the pin to Mathlib v4.34.0 today. The weekly upgrade failed on a gap in Mathlib's own cache, fixed in #185. After that lands, a claim with "base_mathlib_revision": "v4.33.1" is rejected until it's bumped and revalidated. That's the same as what happened on the rc1 → v4.33.1 upgrade.

3. Build errors in the receiver report (our bug)

Your harness runs a plain lake build before the receiver because the receiver only says BUILD_FAILED. That turns out to be a bug, not a design choice. On a failed build, Lake prints the Lean errors on stdout and only error: build failed on stderr. tools/frontier_validate.py keeps stderr whenever it's non-empty (the build at L838, the audit at L849, the smoke test at L804), so the actual error text is dropped.

I'll fix that so the report carries the Lean diagnostics for the submitter's own files. If there are other diagnostics your agent found hard to get from the receiver, list them here and I'll look at them in the same pass.

[qazW12345]

There are no other diagnostics that my agent found necessary but unavailable. However, basic information about the progress of triviality probes (number of timeouts, time spent on each section, which tactics timed out) was suggested as data that would help monitor long receiver runs and ascertain whether their length is caused by the complexity of the formalization or by issues such as running out of memory.

One separate issue is that when running the receiver on OCI, the probes have been timing out without terminating the process cleanly. In our run, several lean /tmp/leanfrontier/baseline_probe.lean processes remained with PPID 1 after their corresponding probe timeouts. Because of this, orphaned processes accumulated, consuming a large amount of memory and swap and progressively decreasing the speed at which the receiver worked. All orphaned processes could be distinguished by having been reparented to PID 1, and could be terminated manually to free the memory they were consuming.

[carlok]

Thanks, both points were useful.

Orphaned probe processes: confirmed, it was our bug. Every probe is lake env lean … run through subprocess.run(..., timeout=…), and on timeout Python kills only its direct child, lake. The lean underneath gets re-parented to PID 1 and keeps running, which is exactly what you saw. It happens in CI too, where the orphans eat into the container's 2 GB for the rest of the run. #201 runs each command in its own process group and kills the whole group on timeout. It includes a test in which the orphaned grandchild survived before the fix and doesn't after.

Probe telemetry: also in #201. Each probe attempt is now recorded with its tactic, outcome and wall time, plus totals for attempts, timeouts and seconds, under baseline_probe_runs in the report.

Your PRs:

• feat: add finite-group character orthogonality #194 is merged. feat(Geometry): add Farey Ford-circle maximality #197 and feat: add Horadam companion matrix theory #195 go in next, one at a time. Each merge puts the others behind main, so expect branch updates and re-runs in between.
• docs: add contribution directions roadmap #196 can't pass as a fork PR: a maintenance/ branch from a non-owner is validated as an ordinary submission. docs: add contribution directions and PR cadence (from #196) #200 carries your commit unchanged, with your authorship. It also links the dossier from CONTRIBUTING.md and adds a short "how many PRs at once" section adapted from the cadence text on your fork's prompts/SUBMITTER.md. You're credited as co-author on that commit. Closing docs: add contribution directions roadmap #196 in favour of it.

[carlok]

Everything here has landed: the contribution directions (#200, with your commit), Horadam (#195), receiver diagnostics (#187, #193), and the orphaned-probe fix plus probe telemetry (#201). #194 and #197 are merged too. Closing. Thanks for the reports, both were real bugs.