Three spec lines written in notation the language does not have - #2791
Merged
Conversation
Spec-side, not parser-side. Of the eight lines using a single `=` where t27
needs `==`, three can be repaired without inventing meaning:
assert G_MEASURED = 6.67430e-11 +/- 1.5e-15
-> assert abs(G_MEASURED - 6.67430e-11) < 1.5e-15
assert LOG3_2 * LOG2_3 = 1.0 within 1e-6
-> assert abs(LOG3_2 * LOG2_3 - 1.0) < 1e-6
assert BRACKET_UNKNOT = 1.0
-> assert BRACKET_UNKNOT == 1.0
AND I VALIDATED THE FIRST TWO AGAINST A BROKEN LINE. My first rewrite used
`assert |x - y| < tol`, because specs/vsa/jones_polynomial.t27:318 writes it that
way -- and that line is itself one of the discarding ones. The parser has no
vertical-bar absolute value. Measured: the rewrite moved 2 tokens.
`abs(...)` is the corpus's actual idiom; specs/math/radix_economy.t27 uses it
four times in clauses that lower cleanly. With it:
discarded tokens 23644 -> 23624
constants 11 -> 10 fallback events
radix_economy 5 -> 4
jones_polynomial 4 -> 3
all three still generate with every backend
THE OTHER FIVE ARE NOT MECHANICAL, and are left alone:
* three carry quantifier prose (`for all positive integer n`,
`for any a, b in {1, -1}`) and belong to #2774
* `assert E_OPTIMAL = 1/e` references an `e` the spec never defines; the
constant's own definition line says `= 0.36787944117144233; // 1/e`, so the
assertion is a restatement of the definition and needs an author, not an edit
* `assert jones_polynomial(...) = jones_polynomial(...)` is followed by
`when bracket1 and bracket2 are related by Reidemeister moves` -- an English
sentence, not a clause
suite --ratchet RATCHET: CLEAN, three entries re-blessed
check_specs_generate.py / check_seal_coverage.py / check_elab_ratchet.py exit 0
Refs #2754
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 07:57:47 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 08:07:03 UTC
Summary
Seal Status
|
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.
Refs #2754
Spec-side, not parser-side. Of the eight lines using a single
=where t27 needs==, three can be repaired without inventing meaning:I validated the first two against a broken line
My first rewrite used
assert |x - y| < tol, becausespecs/vsa/jones_polynomial.t27:318writes it that way — and that line is itself one of the discarding ones. The parser has no vertical-bar absolute value. Measured: the rewrite moved 2 tokens.abs(...)is the corpus's actual idiom;specs/math/radix_economy.t27uses it four times in clauses that lower cleanly.constantsfallback eventsradix_economyjones_polynomialAll three still generate with every backend.
The other five are not mechanical, and are left alone
for all positive integer n,for any a, b in {1, -1}— and belong to #2774assert E_OPTIMAL = 1/ereferences anethe spec never defines. Its own constant reads= 0.36787944117144233; // 1/e, so the assertion restates the definition and needs an author, not an editassert jones_polynomial(…) = jones_polynomial(…)is followed bywhen bracket1 and bracket2 are related by Reidemeister moves— an English sentence, not a clause🤖 Generated with Claude Code