v1.3.0 — two proved theorems in the note, the proof of one of them, and a referee pass that flagged everything

Released 2026-08-18. Previous: v1.2.0 (2026-08-17).

This release adds; it corrects nothing that was public. Every statement in v1.2.0 that this version touches was true when it was written. What changed is that two of the note's open questions became theorems.

Two proved theorems in the standalone note

paper/note1.tex — Two speeds at the boundary — grows from 11 to 12 pp., with paper-ja/note1_ja.tex moving in the same round.

thm:monotone — a lower bound for every non-increasing profile. Let w_0 ≥ … ≥ w_{k−1} ≥ 0 and t > 0. If arctan(2t) ≤ π/k then F_k(½+it) ≥ 1, so there is no zero on 0 < t ≤ ½tan(π/k). Two lines from an exact summation-by-parts identity, now displayed. The previous version had this for constant weights only. Monotonicity is doing work in the strong sense: the increasing ramp w_j = (j+1)/k drives F_k to −25.93 at k = 64 inside the window, so the conclusion fails and not merely the bound — and it is not necessary, since a bump and an alternating profile stay above 1 without being monotone. Proved, two routes.

thm:decayrate — the exact rate above the kink. Fix s > 1, w_j = (j+1)^−s. Then for all large k a first zero t₁(k) exists and 2k t₁(k)²/log k → s − ½. This is the first complete analytic theorem in the programme at the level of the rate, and it answers, for s > 1, the note's own section What a proof of the decaying case would have to supply. Proved, two routes.

rem:shape — the shape, statuses split rather than averaged. λ_∞(s) = max(s/2, s − ½), kink exactly where Σ_j w_j stops converging: above it the theorem, below it a measurement (s = 0.5, 0.75 at k = 32768, the two candidates separated by 22.2 and 20.5 times the observable's own quantum), at s = 1 derived by two routes. Near the kink the measurement cannot decide, and the remark now says so with the numbers.

The proof is in the deposit, because the status says proved

paper/proof_decayrate.md is new to this repository. It was written at r229, repaired at r231, and lived in a design document that .gitignore excluded — so the note carried STATUS{proved} on its headline theorem while a reader holding the note could not reach a line of the proof.

A statement that lives one artefact away from its reader has not been made.

The referee pass, reported in full because it did not go well

Before this release the new section went through the standing referee pass: a reader in fresh context, given exactly three jobs — restate the claim, name what would falsify it, flag any single word whose deletion changes it — and nothing else.

It flagged all nine units. The text was green on all twenty-two mechanical checks and built in both languages with zero undefined references.

what it caught	why no check could
"its limit is 2ζ(s)" — false as written; the sine series tends to 0, and the quantity with that limit is the series divided by t	valid mathematics, wrong claim
STATUS{proved} on a theorem whose proof the repository excluded	no check reads whether a cited proof is reachable
"appears to satisfy" hedging a branch the same status block calls proved	a status cannot fix a verb, and no check reads adverbs
"decisively", "twenty times the observable's resolution" — a tier not in the note's vocabulary, and a resolution the note never defines	the numbers were right; the reader could not find them
"Consequently the first zero…" — presupposing a zero the hypotheses do not give	quantifier presupposition, invisible to a grep
"drives F_k well below 1" — unquantified, and below 1 is the wrong threshold for the claim	the stronger, true statement was in a log we already had
"fix the shape", "has stopped being a table of measurements"	the statuses were right; the prose overtook them

Eight flags accepted, one word defended with its reason recorded and its secondary finding accepted. The pass and every adjudication are in lean/pnp/refpass_r233.log.

Grepping outward from one flag found a stale count in both editions: "the twenty-one mechanical checks". There are twenty-two. C22 was added the day after v1.2.0 was tagged — true when written, and the artefact kept asserting it.

Everything else

• The sweep before the tag — what did this release make false? — returned four artefacts, none of them a paper and so none covered by any check: the deposit's page count, the README's release line and log count, the homepage (which still called Part III's three headline theorems conditional, eight days after they stopped being so, and did not mention the note at all), and the check count above.
• New artefacts: paper/proof_decayrate.md, lean/pnp/refpass_r233.log.
• The Lean canon is unchanged, and still replays through an independent kernel that must first reject three deliberately corrupted modules.

What has not changed

Not peer-reviewed. Every statement declares its own status where it is stated. The s < 1 branch is still a measurement, and the note says so at the statement rather than in a footnote.

A DOI makes a version permanent; it does not make it true.