docs(missions): wall backlog map -- 25 unproved nodes mapped, and the grant-gate hole that #569 closes - #574
Merged
Merged
Conversation
Maps every not-proved node across rh/mirrormere/anduril/bg onto six facets
cut along the uniformity-vs-instance seam, with a verdict per node.
Headline finding (registry health question c), demonstrated with a throwaway
probe campaign rather than inferred: the grant gate can mark a node proved on
a false premise. A node whose registered statement is RiemannHypothesis was
granted proved with closure_clean=true off an artifact proved by `sorry`,
while its declared dependency sat at draft -- and `mission verify` reported OK
with zero errors and zero warnings. Three composing defects:
G1 grant_status decides by normalized text containment only; normalize_lean
strips a trailing sorry with a $-anchored regex, so a sorry-carrying
artifact matches by design. The right checker already exists
(telperion audit, cli.py:635) and the gate never calls it.
G2 grant_status never inspects depends_on; dep-awareness lives only in
open_leaves, a scheduling query, not a gate.
G3 closure_clean is recomputed only for via="reduction"; 44 of 44 live proof
links are via="direct", so the cascade guard has never run on a real node.
Nothing errors on a proved node with closure_clean=false either.
Fixes R11-R14 proposed in priority order; R11 is a call into existing code.
Also: 5 nodes whose deps claim what the corpus does not support (the D3
exemplar is still unfixed on its branch; RH_bl_explicit_formula's title
refutes both its own edges), root-caused to the absence of any cross-campaign
edge mechanism; 2 genuinely stale drafts (MM_torus_section_dictionary blocks
an open node and replaced a statement caught as trivially rfl, never
re-audited); and the structural gap that facet F1 rests on facet F2, which
has one registered node.
No Lean built, no node status changed, no registry file touched.
conjecture1_proved = False
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.
Every not-proved node across all four campaigns (25: rh 6, mirrormere 9, anduril 4, bg 6) mapped onto the wall-assault facets, one table row each, plus 14 concrete registry operations and three registry-health answers.
The health finding that matters, and it was demonstrated rather than inferred. The grant gate could mark a node proved on a false premise. On a throwaway probe campaign, a node whose registered statement was
RiemannHypothesiswas grantedprovedwithclosure_clean = truefrom an artifact whose only proof wassorry, while its declared dependency sat atdraft, andmission verifyreported OK with zero errors.I confirmed the mechanism independently:
normalize_leanstrips a trailing:= by sorrybefore comparing, so a stub's normalized text is the bare statement and containment passes. #569 (merged) closes it by rejectingsorry/admit/native_decidein artifact code, comments and strings stripped first. I tested the fixed gate against a fake proof of the conjecture: rejected.Two further health findings, recorded with root causes rather than patched blind:
via = direct; thereductionmechanism has zero instances across all four campaigns. The registry supports a reduction relation that nothing uses.Docs only; no registry file touched by this PR.
conjecture1_proved = False.🤖 Generated with Claude Code