From e85a508e164e09cd0396b553668fed60c283f198 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 11:54:23 +0200 Subject: [PATCH 1/2] Record receiver changes as a pre-registration deviation Three arm-tagged submissions exist, so this is a dated deviation record, not an amendment. It lists #193, #201, #216 and #239, notes that the add-only rule creates import edges by construction and so interacts with the primary metric, and commits the analysis to splitting the metric at 22 September 2026. Co-Authored-By: Claude Opus 5 --- PREREGISTRATION.md | 48 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/PREREGISTRATION.md b/PREREGISTRATION.md index a4d5c916..f1b9e048 100644 --- a/PREREGISTRATION.md +++ b/PREREGISTRATION.md @@ -146,3 +146,51 @@ distinguish a prompt effect from an interaction between the prompt and one generator's habits. If arm B succeeds, the honest claim is that this instruction changes what these models do, and replication with a different producer becomes the obvious follow-up rather than an optional extra. + +## Deviation, 22 September 2026 + +Recorded after data exists: three accepted submissions carry an arm (A: 2, +B: 1), all landed on or before 20 August. This is not an amendment to the +design. It records receiver changes made for security and maintenance reasons +between then and now, so that the analysis can account for them. The +hypothesis, the primary metric, the stopping point and the decision rule are +unchanged. + +The receiver is still identical across arms, as the design requires. Four +changes landed: + +- **#193**: a rejected build now reports the Lean errors in the submitter's own + files instead of only `error: build failed`. This changes the feedback a + producer iterates on, not what is admitted. +- **#201**: a timed-out probe no longer leaves `lean` running, and each probe's + outcome and time are recorded. This changes resources and observations, not + admission. +- **#216**: ordinary submissions may only **add** files, and code that runs at + build or import time is rejected. +- **#239**: deprecation warnings in the submission's own files are rejected as + `DEPRECATED_API`. + +**The add-only rule interacts with the primary metric.** Before #216, a +submission could extend an accepted module by editing it, which creates no +import edge. Now it must add a module that imports the one it extends, which +creates an edge by construction. The metric can therefore rise for reasons that +have nothing to do with the launcher, and plausibly more in arm B, whose +paragraph asks for exactly that kind of extension. Of the corpus's accepted +submissions before the change, one (#169, unassigned) extended a module by +editing it. + +To keep this separable, the analysis will: + +- report the primary metric separately for arm-tagged submissions accepted + before and after 22 September 2026; +- count, for each arm, the edges whose target is a module the same submission + could previously have edited instead: an accepted module extended rather than + merely used. + +If the two periods disagree, the pre-change submissions are the cleaner test of +the hypothesis. The post-change result will be reported as conditional on the +add-only rule. + +The deprecation rule can reject submissions that would have been accepted +before. It applies identically to both arms and counts toward neither arm's +stopping point until a corrected resubmission is accepted. From db16dfc009a0f6834c8a1a71ff3ce961415fc627 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 12:12:24 +0200 Subject: [PATCH 2/2] Add #241 to the receiver deviation record Co-Authored-By: Claude Opus 5 --- PREREGISTRATION.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/PREREGISTRATION.md b/PREREGISTRATION.md index f1b9e048..bed0283c 100644 --- a/PREREGISTRATION.md +++ b/PREREGISTRATION.md @@ -156,7 +156,7 @@ between then and now, so that the analysis can account for them. The hypothesis, the primary metric, the stopping point and the decision rule are unchanged. -The receiver is still identical across arms, as the design requires. Four +The receiver is still identical across arms, as the design requires. Five changes landed: - **#193**: a rejected build now reports the Lean errors in the submitter's own @@ -169,6 +169,9 @@ changes landed: build or import time is rejected. - **#239**: deprecation warnings in the submission's own files are rejected as `DEPRECATED_API`. +- **#241**: a conjecture the claim does not list as an entrypoint is now probed + in both directions, as the contract always required. It was silently skipped + before. None of the three arm-tagged submissions is a conjecture. **The add-only rule interacts with the primary metric.** Before #216, a submission could extend an accepted module by editing it, which creates no