bench: amend Tseitin ladder registration — raise the 4x5 cap (mid-run) - #69
Merged
Merged
Conversation
Recorded while the run is in progress, before any conclusion is drawn. No registered prediction is edited; only a timeout cap changes. A cap is an operational parameter, not a hypothesis -- 4x5 produces the same number whenever it is produced. 4x4 closed in 429s at 95,516 resolutions, matching the previously banked figure exactly through the budgeted-session path. 4x5 then exhausted its 90-minute cap without closing, at 452,569 resolutions and still climbing. So the 4xN axis is materially slower at min=4 than the rows=3 reference suggested, and the 3h caps on 4x6/4x7 will near-certainly time out too -- spending ~6h on lower bounds for the cheap axis while 4x5, the case that actually tests prediction 2, stays unmeasured. tseitin_second_pass.sh waits on the ladder lock and re-runs 4x5 with a 4.5h cap in the idle window before the ~05:57 reboot. Prediction 2 standing: observed >= 4.74x and UNFINISHED, so a lower bound, not a measurement. The predicted 1.3x-5x band will be exceeded; whether the two-axis story breaks depends on where 4x5 lands, which a lower bound cannot settle. That is why the cap was raised rather than the prediction reworded. Prediction 1 is unaffected and can still be confirmed by a timeout: it is a >= claim, so a 5x5 that passes ~1.9M resolutions without closing confirms it from below. Only a 5x5 that closes small could falsify it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Mid-run amendment, recorded before any conclusion is drawn. No registered prediction is edited — only a timeout cap changes. A cap is an operational parameter, not a hypothesis; 4×5 produces the same number whenever it is produced.
What happened
Why change anything
The 4×N axis is materially slower at
min = 4than the rows=3 reference suggested. So the 3h caps on 4×6 and 4×7 are near-certain to time out too — spending ~6h producing lower bounds on the cheap axis while 4×5, the case that actually tests prediction 2, stays unmeasured.tseitin_second_pass.shwaits on the ladder lock (4GB box — one heavy job at a time) and re-runs 4×5 with a 4.5h cap in the idle window before the ~05:57 reboot.Standing of the predictions
Prediction 2 (1.3×–5× per 4×N step, ~20× = falsification): observed ≥4.74× and unfinished — a lower bound, not a measurement. The narrow band will be exceeded. Whether the two-axis story actually breaks depends on where 4×5 lands, and a lower bound cannot settle it. That is precisely why the cap was raised rather than the prediction reworded.
Prediction 1 unaffected — and note a timeout can still confirm it. It is a
≥claim (5×5 ≥ ~1.9M resolutions), so a 5×5 that passes that figure without closing confirms it from below. Only a 5×5 that closes small could falsify it.🤖 Generated with Claude Code