voyager: production corrections from the 2026-08-05..10 runs

skills/voyager/HANDOVER.md

@@ -24,16 +24,17 @@ again. When in doubt, skip; the result will still be true tomorrow.
 | thing | value |
 |---|---|
 | credentials | `~/.zuliprc` (bot email `Voyager-bot@leanprover.zulipchat.com` — capital V; never echo the key) |
-| watermark | newest self-DM: `commit=02d13f9307fc… pr=1692` (DM id 614590157) |
-| messages posted | 613614529 (first-run backlog, 2026-07-30, edited in place per channel feedback; now 9,473 codepoints — **do not let it grow**), 613886812, 614078696, 614179130, 614350642, 614590153 |
+| watermark | newest self-DM: `commit=54d9297295d9… pr=1770` (DM id 614796848) — always re-read the DM; this row is a snapshot |
+| messages posted | 613614529 (first-run backlog, 2026-07-30, edited in place per channel feedback; now 9,473 codepoints — **do not let it grow**), 613886812, 614078696, 614179130, 614350642, 614590153 (edited 2026-08-05 to note the `ModularForm.L` overlap Thomas Browning raised), 614796841 (seventh, 13 bullets — too many; see the curation rule below) |
 | cadence | daily, 16:03 UK; the window always ends at TauCeti's `docgen` branch |
-| scheduling | a self-renewing session cron job in Chris's Claude session (currently `a22e2578`). Session-only: it dies if that session closes, and it fires late if the machine is asleep or the session busy at 16:03 — this has happened three times and is harmless (the watermark defines the window, not the clock). The sturdier long-term home is a GitHub Actions workflow in the TauCeti repo; Chris knows |
+| scheduling | a macOS launchd agent, `com.tauceti.voyager`, fires a fresh **headless** run (`claude -p`, claude3 account) daily at 16:03 — see `launchd/README.md` beside this file. It replaced the self-renewing session cron on 2026-08-12 after two production lessons: a session cron dies with its session (the 2026-08-11 credits incident forced a takeover), and macOS App Nap delayed every idle-session firing by 20–40 minutes. launchd fires on the wall clock and logs to `~/Library/Logs/voyager.log`; a machine asleep at 16:03 runs once on wake. Any leftover session cron is a harmless backup — the freshness abort resolves double-fires |
 | first-run.md | dead weight — the backlog was posted once (2026-07-30) and must never be reposted; ignore that file entirely |
 
 Owner decisions already made, not yours to revisit: no `sorry` counts in the stats block
 (the no-`sorry` rule stays as an announcement gate); daily cadence at 16:03 UK; quiet windows
 with merged PRs still get a short check-in; only a genuinely empty window posts nothing; the
-loop keeps running until Chris says otherwise.
+bullet list is curated rather than exhaustive, and short is fine (2026-08-05 — see the
+curation rule under House style); the loop keeps running until Chris says otherwise.
 
 ## The shape of a run
 
@@ -73,6 +74,34 @@ back-reference to the earlier PR.
 The messages have earned trust by sounding like a mathematician telling colleagues what is
 now proved, not like release notes. Every rule below came from feedback or a near-miss.
 
+**Curate, don't enumerate — and there is no target length.** Chris, 2026-08-05, after the
+seventh update ran to thirteen bullets: *"don't feel obliged to make the list long, it's more
+important to keep it interesting and mention significant results."* Every bullet in that
+message had passed all three gates, which is exactly the trap — the gates decide what is
+*allowed*, and you still have to decide what is *worth reading*.
+
+Chris sharpened this on 2026-08-09, after a message came in at five bullets and dropped an
+interesting one to stay there: *"there is no rule to cut it to 5. the rule is that there doesn't
+need to be a minimum or maximum, but you just need to make them be interesting."* Both failure
+directions are real and the second is the sneakier: padding a thin window is obvious, whereas
+cutting a good bullet to hit a self-imposed count looks like discipline. It isn't. Judge every
+candidate on its own interest and keep exactly those that pass, whether that is one or ten.
+Nothing is lost by leaving a dull one out — the dedupe keys on *cited* PR numbers, so it stays
+announceable the day it matters. Message 614796841 (thirteen bullets, padded) and message
+615474670 (five bullets, one good one cut for the count) are the two calibration points, one in
+each direction.
+
+**Read every PR's contents — titles are not a filter.** Chris, 2026-08-10, after asking why
+no elliptic-curve result had ever appeared: *"you can't rely on PR title, don't be lazy, this
+is meant to be a slow methodical and careful check. you need to look at the contents of each
+PR and from that make your list."* The record that prompted it: 105 bullets announced, zero
+elliptic-curve results, while fifteen `feat(EllipticCurve)` PRs landed in two windows —
+Silverman III.10 on Aut(E) for j ∉ {0, 1728} (TauCeti#2248), the quadratic twist and its
+invariants (TauCeti#2254), and quadratic Galois descent (TauCeti#2268) among them, none
+opened because the directory's titles read as bookkeeping. SKILL.md §2 now requires reading
+every body in the window, and adds that the window bounds discovery, not eligibility: a
+result found late is announced late, not never.
+
 **The bullet is the unit.** Its anatomy, fixed:
 
 > - **[Standard name](verified docs anchor)** — one sentence, for a mathematician who does
@@ -152,7 +181,7 @@ a bug. No sorry counts.
 
 **The quiet check-in**, when PRs merged but nothing survived the gates:
 
-> **Voyager · Tau Ceti check-in**
+> **Voyager · Tau Ceti check-in** *(AI-generated summary)*
 >
 > No notable named results landed in this window (as judged by the voyager AI bot).
 >
@@ -227,6 +256,16 @@ message, not a silent rewrite of history.
   working (stats, anchors, sorry gate) while it runs.
 - The sorry gate greps *mentions*: read the hits; a docstring saying "the `sorry`-goal in
   Suggested.lean" is not a proof hole.
+- Python's TLS can break independently of `curl`. On this machine the python.org 3.12 build
+  lost its CA file (`ssl.get_default_verify_paths().cafile` is `None`), so `zulip.py check`
+  died with `CERTIFICATE_VERIFY_FAILED` while `curl` kept working. The run path is curl-only
+  and was unaffected — but do not read a failing probe as a dead bot. Fix with
+  `export SSL_CERT_FILE=$(python3 -c 'import certifi;print(certifi.where())')`, or run the
+  installer's "Install Certificates.command".
+- The state DM's SHA must be copied, never retyped or padded — see the watermark protocol in
+  SKILL.md, rule 5.
+- A freshness abort is a *success*. If a human asked for the post early and the cron then
+  fires, the gate stops the double-post; report the abort and move on.
 - Never post from a fallback channel or invent output when credentials fail — report loudly
   and exit.
 

skills/voyager/SKILL.md

@@ -41,6 +41,24 @@ Do **not** post:
   Mathlib is worse than useless;
 - a result whose proof still contains `sorry` in its dependency cone.
 
+**Curate; do not enumerate** (owner decision, 2026-08-05, sharpened 2026-08-09). Passing the
+bar above earns a result *eligibility*, not a bullet. The message is a digest, not a changelog:
+keep the ones a mathematician outside the project would actually want to hear about — a named
+theorem with content, a construction the subject is phrased in, something that closes a
+milestone or unblocks upstream.
+
+**There is no target length: no minimum and no maximum.** Interest is the only test. Do not pad
+a thin window to look productive, and — the failure that prompted this sharpening — do not drop
+an interesting result to hit a number. A one-bullet day and a ten-bullet day are both correct if
+that is what the window actually held. Any rule of thumb about "a handful" is a description of
+past windows, never a quota to hit or a cap to respect; if you find yourself cutting a bullet
+you would have been glad to read, the count is driving and it should not be.
+
+Incremental strengthenings, small computations, and infrastructure that happens to carry a name
+are eligible but seldom interesting — drop those on their merits, not to make room. Nothing is
+lost by omitting a genuinely dull result: the permanent dedupe keys on *cited* PR numbers, so
+anything left out today stays announceable the day it matters.
+
 ## Where Voyager posts
 
 Voyager is a **Zulip bot named `voyager`** on the **Lean Zulip**
@@ -95,12 +113,14 @@ confirms channel subscription without posting. Run it first after setup.
 
 ## Prerequisites
 
-Tools: `gh` CLI (authenticated), `git`, python3 stdlib only, the **chatgpt-math MCP** for
-the significance gate, and a local Mathlib checkout for the novelty gate (the roadmap
-repo's `.lake/packages/mathlib` is fine).
+Tools: `gh` CLI (authenticated), `git`, python3 stdlib only, and a local Mathlib checkout
+for the novelty gate (the roadmap repo's `.lake/packages/mathlib` is fine). The
+**chatgpt-math MCP** drives the significance gate when it is reachable, but is **not**
+required — see §4.
 
-If credentials are missing, **stop and report** — do not post to a fallback channel and do
-not invent a message.
+If Zulip credentials or `gh` are missing, **stop and report** — do not post to a fallback
+channel and do not invent a message. This rule is about *those* credentials: a missing or
+quota-blocked chatgpt-math MCP is not a reason to stop, and never a reason to skip a post.
 
 ## Running it
 
@@ -168,6 +188,12 @@ Each run:
    `pr=` to the merged-PR count at that time, write the DM, then proceed.
 4. **After every successful channel post, send the updated state DM** — post first, DM
    second; if the DM write fails, retry it before ending the run.
+5. **Never reconstruct the commit hash.** Put the *full* SHA in the DM exactly as
+   `git rev-parse origin/docgen` prints it. Do not pad an abbreviated hash you had on screen,
+   and do not retype it: a plausible-looking 40-character string that names no object makes
+   the next run's window unresolvable, and nothing downstream will notice. This happened
+   (2026-08-08) — the fix is a second DM superseding the first, since the protocol reads the
+   newest. Cheap check before sending: `git cat-file -t <sha>` prints `commit`.
 
 ## Never double-post
 
@@ -214,15 +240,34 @@ same tree the window ends at.
 
 ### 2. Extract candidates
 
-**Work PR-by-PR — the merged PRs are the unit of discovery.** TauCeti squash-merges, so
+**Work PR-by-PR — the merged PRs are the unit of discovery, and read every one of them**
+(owner instruction, 2026-08-10: *"you can't rely on PR title, don't be lazy — this is meant
+to be a slow, methodical and careful check. You need to look at the contents of each PR and
+from that make your list."*). TauCeti squash-merges, so
 `git log --format='%s' <watermark>..HEAD` lists exactly the window's PRs, one per commit,
-with the number in the subject (`feat: prove the double centralizer theorem (#1435)`).
-Triage by title: `feat:` is where announcements live; `chore:`/`refactor:`/`fix:` almost
-never are. Then, for each candidate,
-`gh pr view <n> --repo TauCetiProject/TauCeti --json title,body` — the body typically says
-what was proved, names the result, and cites the roadmap and references, which is exactly
-the raw material for the significance gate and for writing the one-sentence description.
-The PR is also the attribution unit, so this hands you the link for free.
+with the number in the subject. For **every** PR in the window — `feat:`, `chore:`,
+`refactor:`, `fix:`, all of them — fetch the body and decide from **what it says was proved
+or defined**, never from the title alone. Batch the fetches
+(`gh pr list --repo TauCetiProject/TauCeti --state merged --search "merged:>=<date>" --json
+number,title,body`) rather than skipping any. The body names the result and cites the
+roadmap and references — the raw material for the significance gate and the one-sentence
+description — and the PR is the attribution unit, so this also hands you the link for free.
+
+**Titles are labels, not filters.** Title-tone triage is the lazy shortcut, and it produced
+the worst miss so far: fifteen `feat(EllipticCurve)` PRs across two windows all read as
+bookkeeping by title and none was opened, while 105 bullets went out with zero
+elliptic-curve results among them. Reading the bodies later surfaced the automorphism group
+of an elliptic curve with j ∉ {0, 1728} (TauCeti#2248 — Silverman III.10, uniform in the
+characteristic), the quadratic twist of a Weierstrass curve with its invariant theory
+(TauCeti#2254), and quadratic Galois descent for changes of variables and affine points
+(TauCeti#2268). A `refactor:` body can likewise reveal a completed proof or a newly named
+object. A body costs seconds to read; a miss is invisible until someone asks why a whole
+subject never appeared.
+
+**The window bounds discovery, not eligibility.** The permanent dedupe keys on *cited* PR
+numbers, so a result missed in an earlier window stays announceable the day it is found.
+When a triage lapse comes to light, fold the missed items into the next run's candidates
+and gate them normally.
 
 **Cross-check with the module-title sweep — a bland PR title can hide a named result.** Every
 Tau Ceti file opens with a `/-! # Title` naming what it contains, and named results are named
@@ -320,8 +365,26 @@ docstring's *Main results* before believing any title.
 
 ### 4. Significance gate — the ChatGPT second opinion
 
-Batch **all** surviving candidates into **one** `mcp__chatgpt-math__ask_chatgpt_math`
-call. Operational facts learned the hard way:
+**The gate is best-effort, not a precondition for posting.** Probe it with one cheap call
+**before** reading the window: if it is going to be unavailable, that should cost seconds,
+not a full read of every PR body. When it answers, its ranking drives bullet order and it
+serves as the second opinion on how noteworthy each result is. When it does not — codex
+quota exhausted, the account's plan refusing reasoning models, the MCP absent, a timeout —
+**run without it**: select and order on your own judgement, post as normal, and record one
+line in the run's final output naming why it was skipped.
+
+Do not hold the post, do not substitute a different model, and **do not mention the gate or
+its absence in the Zulip message** — that belongs in the log, not in front of readers.
+Holding is the worse failure: it takes a window that plainly contains notable results and
+publishes nothing, which is indistinguishable to readers from a quiet week.
+
+This was learned on 2026-08-15, when both codex accounts were out (`~/.codex` on quota,
+`~/.codex2` on quota *and* refusing `gpt-5.6-sol`/`gpt-5.4`/`gpt-5.3-codex` outright with
+HTTP 400) and two separate runs read all 138 PRs in the window, assembled a slate, and then
+declined to post because the gate was documented as mandatory.
+
+When the MCP *is* reachable: batch **all** surviving candidates into **one**
+`mcp__chatgpt-math__ask_chatgpt_math` call. Operational facts learned the hard way:
 
 - use `reasoning_effort: "high"`. **`max` reliably times out** on long prompts (the MCP
   aborts after ~30 min of silence) — `high` has been reliable;
@@ -344,19 +407,39 @@ worth announcing. For EACH numbered item below, answer with one of:
 
 For each ANNOUNCE, add: (a) the standard name of the result, (b) one sentence, for a
 mathematician who does not know it, saying what it asserts, (c) whether it has a
-Wikipedia page, and (d) a standard reference if you know one.
+Wikipedia page, and (d) a standard reference if you know one. Finally, rank the
+strongest candidates in order of how noteworthy they are to a general mathematical
+audience — this ranking, not the order of discovery, decides which result leads.
 
 Be conservative: if a result is only interesting inside its own proof, say SKIP. Do not
 be polite about it — a false ANNOUNCE is more costly than a false SKIP.
 
 <numbered list: name, Lean statement, docstring summary>
 ```
 
+**The gate is the second opinion on interest, not only on eligibility** (owner
+instruction, 2026-08-10: get ChatGPT's view on *how interesting or noteworthy* each
+result is, every pass). ANNOUNCE/SKIP feeds the cut; the per-item reasons and the
+ranking feed the curation — which bullets run, in what order, and which eligible
+results wait for a better day. Curation stays the operator's call (§What counts), but
+it is made with the gate's reading in hand, never instead of it.
+
 Take its verdicts as **advice, not authority**. It has been wrong before on this project —
 it misnumbered a Wedhorn theorem and mis-attributed a Mathlib file's authors. If a verdict
 looks wrong, check the primary source and use your judgement. Never post a description you
 have not sanity-checked against the actual Lean statement.
 
+⚠ **The gate can only judge the summary you give it, so a summary that overstates a strand
+gets you an ANNOUNCE for something unproved.** Describe each candidate in the words of the
+file's own `## Main results`, not in the words of the roadmap milestone it serves. Worked
+instance (2026-08-08): a batch of adic-spaces PRs was described to the gate as "the machinery
+establishing that the valuation spectrum is a spectral space"; the gate duly said to announce
+"Spv is spectral", and only extracting the anchor revealed that no `SpectralSpace` conclusion
+exists anywhere in the tree — the patch criterion and the pro-constructible calculus had
+landed, the endpoint had not. This is the Bochner trap arriving through the gate rather than
+through the directory listing, so the same rule applies: find the theorem statement, or do
+not announce it.
+
 ### 5. Attribute each result to a PR
 
 Readers must be able to click through. TauCeti squash-merges, so the PR number is already in
@@ -385,7 +468,7 @@ report the same PR, that is the bug. Check with `test -f .git/shallow` and
 Format (Zulip markdown):
 
 ```markdown
-**Voyager · what's new in Tau Ceti**
+**Voyager · what's new in Tau Ceti** *(AI-generated summary)*
 
 *Named results*
 - **[<Standard name>](<link to the source file at main>)** — <one sentence on what it asserts>. (TauCeti#123)
@@ -402,8 +485,11 @@ Format (Zulip markdown):
 
 …then send the updated state DM (see the watermark protocol).
 
-Zulip-specific rules, each learned from reader feedback on the first message:
+Zulip-specific rules, most learned from reader feedback on the first message:
 
+- **The header carries the disclosure suffix `*(AI-generated summary)*`** (owner request,
+  2026-08-19): every channel message — full update and quiet check-in alike — states in its
+  top line that an AI wrote it. The suffix survives any trimming done for the codepoint cap.
 - **One physical line per paragraph and per bullet.** Zulip keeps single newlines as line
   breaks, so hard-wrapped prose renders with ragged mid-sentence breaks. Never wrap.
 - **Use the realm linkifiers**: bare `TauCeti#NNN` for TauCeti PRs, `mathlib4#NNN` for
@@ -453,11 +539,15 @@ the result; no marketing adjectives; no "exciting"/"major milestone". State what
 theorem says, not how impressive it is. If a result is a strengthening of Mathlib, say so
 in the sentence.
 
+Length is neither a virtue nor a vice. The bullet list is **curated, not exhaustive**
+(§What counts), and carries no target count in either direction — put the most interesting
+result first, and let the message end when the interesting ones do, however many that is.
+
 **Quiet runs still report.** If the window contains newly merged PRs but nothing survives
 the gates, post this short check-in instead of the full format:
 
 ```markdown
-**Voyager · Tau Ceti check-in**
+**Voyager · Tau Ceti check-in** *(AI-generated summary)*
 
 No notable named results landed in this window (as judged by the voyager AI bot).