CLAIMS C6: name the defect class — three instances, all found rather than prevented - #61
Merged
Merged
Conversation
…han prevented C6 recorded a dangling FORMAL.md citation in gate. Fixing it turned up something worse in the same file, and then a pattern. Gate's README stated T1 as invariance under 'arbitrary corruption of who-copied-whom', omitting the root-set-preservation hypothesis. Orphaning a claim creates a new origin and T1 says nothing about the result. The implementation was correct throughout -- aggregator.py says side-preserving AND root-preserving -- so only the public headline claim was wrong, which is the worse place for it. Fixed in minority-prophet-gate#12 along with the missing FORMAL.md. That is the third instance of one defect: a theorem restated away from its proof with a hypothesis left out, making the restatement strictly stronger than what was proved. The research repository's original T5 omitted the same-assertion hypothesis; gate's README omitted root preservation; and this file's A1 omitted the same-assertion hypothesis of T1 -- the document written to prevent the defect committing it. Three for three, in a programme whose central discipline is not overclaiming. The common cause is restating a theorem away from its proof, so gate's new FORMAL.md refuses to restate and points at the ledger. That is a mitigation and not a fix: nothing prevents the next restatement and no check detects one. Recorded that way rather than as a closed item, and with the observation that the interesting question about a fourth instance would be why three rounds of review did not make the pattern visible before the third.
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
2 participants
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.
C6 recorded a dangling
FORMAL.mdcitation in gate. Fixing it turned up something worse in the same file, and then a pattern.The worse thing
Gate’s README stated T1 as invariance under "arbitrary corruption of who-copied-whom" — omitting root-set preservation. Orphan a claim and you create a new origin; T1 says nothing about the result.
The implementation was correct throughout (
aggregator.py: "side-preserving, root-preserving"). Only the public headline claim was wrong — the worse place for it. Fixed in minority-prophet-gate#12, along with the missingFORMAL.md.The pattern
Three instances of one defect: a theorem restated away from its proof with a hypothesis left out, making the restatement strictly stronger than what was proved.
CLAIMS.mdA1 — omitted the same-assertion hypothesis of T1. The document written to prevent the defect committed it.Three for three, in a programme whose central discipline is not overclaiming.
Mitigation, not a fix
The common cause is restating a theorem away from its proof, so gate’s new
FORMAL.mdrefuses to restate and points at the ledger. But nothing prevents the next restatement and no check detects one.