bench: bank the Tseitin ladder outcome — axis separation measured - #71
Merged
Conversation
4x5 closed at 551,098 resolutions in 6,285s, which is the measurement the night was reallocated to get. Predictions are unedited; this appends an outcome section and copies banked.log into the repo. PREDICTION 2 -- band missed, core claim CONFIRMED. Predicted 1.3x-5x per fixed-expansion step with ~20x as the falsification threshold; measured 4x4 -> 4x5 = 5.77x. The narrow band is wrong at the margin, but 5.77x is nowhere near the 20x that would mean the rectangular axis is also exponential. The axis separation is now measured on both sides with closed cases: expansion (min(r,c) grows) 3x3 -> 4x4 x48.4 fixed-expansion (formula grows) 4x4 -> 4x5 x5.77 The expansion axis is 8.4x steeper per step. That is the ladder's central result and it holds. Practical consequence recorded in CLAUDE.md: scale the square dimension for hardness, the rectangular one for a bigger formula at constant hardness. PREDICTION 3 -- CONFIRMED. size/space (resolutions/peak_learnts) climbs 14 -> 115 -> 340 across 3x3/4x4/4x5, so learnt-DB reduction bounds clause space rather than letting it track proof size. PREDICTION 4 -- correct, 5x5 exceeded its cap and the trajectory bounded it from below as designed. PREDICTION 1 -- still open. 5x5 needs >=~1.9M resolutions to confirm and the 6h attempt reached 1,194,575 without closing. Relaunched with an 8.5h cap. Note the asymmetry: a timeout can confirm this prediction but cannot falsify it; only a closed 5x5 can. A 5x5 closing BELOW ~1.9M would falsify it and would be the more interesting outcome, since it would mean the expansion-axis multiplier is decreasing (48.4x then under 20x) against the rising-multiplier pattern pigeonhole shows. CALIBRATION LESSON. 4x5 closed at 6,285s against an original 5,400s cap -- missed by 884 seconds, under 15 minutes, and banked nothing but a bound. A case that nearly closes banks exactly as little as one that never started. Budget caps with real margin, and prefer one case with headroom over several that each nearly finish. 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.
4×5 closed at 551,098 resolutions in 6,285s — the measurement the night was reallocated to get. Predictions unedited; this appends an outcome section and copies
banked.loginto the repo.Closed cases
Prediction 2 — band missed, core claim CONFIRMED
Predicted 1.3×–5× per fixed-expansion step, ~20× as falsification. Measured 5.77×. The narrow band is wrong at the margin; the claim it was testing survives cleanly, because 5.77× is nowhere near the 20× that would mean the rectangular axis is also exponential.
Axis separation, now measured on both sides with closed cases:
min(r,c)grows)Expansion axis is 8.4× steeper per step. That's the ladder's central result and it holds. Practical rule now in CLAUDE.md: scale the square dimension for hardness, the rectangular one for a bigger formula at constant hardness.
Prediction 3 — CONFIRMED
size/space (
resolutions/peak_learnts) climbs 14 → 115 → 340. Learnt-DB reduction is bounding clause space rather than letting it track proof size. If that ratio ever stops climbing, suspect reduction before suspecting the family.Prediction 4 — correct
5×5 exceeded its cap; the trajectory bounded it from below as designed.
Prediction 1 — still open
5×5 needs ≥~1.9M to confirm; the 6h attempt reached 1,194,575 without closing. Relaunched with an 8.5h cap.
Note the asymmetry: a timeout can confirm this prediction but cannot falsify it — only a closed 5×5 can. And a 5×5 closing below ~1.9M would falsify it and be the more interesting outcome: it would mean the expansion-axis multiplier is decreasing (48.4× then under 20×), against the rising-multiplier pattern pigeonhole shows (×5.4, ×6.1, ×9.7).
Calibration lesson
4×5 closed at 6,285s against the original 5,400s cap — missed by 884 seconds, under 15 minutes, and banked nothing but a bound. A case that nearly closes banks exactly as little as one that never started. Budget caps with real margin, and prefer one case with headroom over several that each nearly finish.
🤖 Generated with Claude Code