Consolidate two clauses that say the same thing, when it can be proved

[OsherElhadad]

Closes #82.

proposals.merges was typed never[], so the offline pipeline could add a clause and retire one and
never consolidate two. It is now MergeFinding[] and populated — but by a narrower rule than the
design asked for, and on a different channel, and both of those are the substance of the PR.

The design question: what evidence justifies proposing a merge?

11-mine-v2.md §8.3 offers three detections. One survives, and it is the one that needs no window
at all.

Accepted — containment, same tier and same level. The kept clause's matched set is a proven
superset of the dropped clause's, so the pair decides exactly what the kept clause alone decides and
the dropped one is dead text. This is a static fact about the pattern strings: no window, no replay,
no traffic. It therefore holds on a corpus that has never been exercised, and it does not weaken when
the decision trail rotates at 4 MiB keeping one generation — the bound that makes every
replay-derived claim in this pipeline a claim about a window rather than about a rule.

Containment is proved two ways and no others:

• substring containment, when both matchers are plain substrings, or when a substring is contained
  in the command literal of an anchored matcher. A substring matches anywhere in the haystack, so it
  is enough that it occurs inside the other pattern's text.
• command-prefix containment, between two instances of the anchored form this pipeline emits
  (commandMatcher). subsumesMatcher recognises that form by parsing back its own literal parts
  — it is a closed, versioned shape we generate — and compares the literals. A longer command prefix
  matches strictly fewer commands, but only when the extra text starts on a token boundary: np
  does not subsume npm test, because nothing after np in npm is whitespace, so the shorter
  matcher's own lookahead refuses the very command the longer one accepts. That off-by-one is the
  whole reason this is a function with a test rather than a startsWith.

Any other regex returns null. There is no regex prover here and there should not be: a containment
prover would be subtly wrong for two years, and wrong in the direction that merges an exception away.

Same level is not decoration on the containment rule — it is what makes containment sufficient.
The objection in the ticket is exactly right: a broad clause and a narrow exception are supposed to
overlap. But that is a level difference. An exception that decides the same way as the rule it
excepts is a no-op, so a same-level narrower clause carries no information the broader one does not
already carry. Different levels with intersecting patterns is never a merge.

Rejected — patterns that intersect without containment, which §8.3 would propose when "both
ablate to the same changed set". Two reasons, either sufficient:

1. The evidence is a bounded claim wearing an unbounded one's clothes. "These two never disagreed in
   this window" is not "these are the same rule", and the window is one rotating generation.
2. The case is not detectable anyway. Between two anchored command matchers, either one literal is
   a token prefix of the other — which is containment, case 1 — or no command can start with both and
   the languages are disjoint. There is no third outcome. Between two arbitrary substrings,
   intersection-without-containment needs the prover we just refused to write.

So it emits nothing at all, not even a report. A list of candidate pairs assembled by a heuristic
is worse than no list: it teaches a reviewer to skim, and the first time it is wrong it will be wrong
about an exception.

Rejected — different levels. Left as-is. It is a conflict report, not a merge, and #83/#81 are
closer to that surface than this ticket is.

Why the output is a retirement and not a new clause carrying supersedes

§8.3 shapes a merge as one new proposed clause with supersedes: [A, B], forced by assertWritable
— the pipeline cannot edit or delete an existing clause file. That shape is right for a merge whose
matcher is neither clause's. That is the intersection case, and it is refused.

For containment the merged matcher would be the kept clause's, byte for byte. The new file would be
a duplicate of a clause already in the corpus under a fresh id, and its arithmetic (+1 −2 = −1) is
exactly the arithmetic of retiring the subsumed clause (−1). It buys nothing and costs the two failure
modes #60 had to add refusals for: a supersedes naming an id that does not exist, and a supersession
cycle — which a containment merge would have walked straight into, because a content-derived id over
the kept clause's own matcher can collide with the kept clause's own id and produce a self-supersession.

So the finding goes on the channel planRetirements already uses: a run-line entry, no file written, a
human acts. This lane writes no supersedes at all. That is not a weaker guarantee than "our
supersedes is acyclic"; it is the same guarantee with nothing left to get wrong.

Non-widening, and it is set equality

L(keep) ⊇ L(drop) gives L(keep) = L(keep) ∪ L(drop), so the corpus after the retirement decides
exactly what it decided before: a green allows no command it did not allow, and a red denies every
command it denied. Asserted behaviourally with the runtime's own evaluator rather than argued —
ablate(drop, corpus, records).changed === 0.

Three narrowings keep that proof true rather than merely plausible:

• Only a learned clause is ever dropped. A machine proposal does not initiate retiring a human's
  practice, in either direction — the same rule compareLadder encodes. Clause.origin absent means
  human, and that default is the safe one.
• Same tier. A missing tier is skipped by the loader, so a clause in another tier may not be
  present in the context this one is. Equality of decided sets only follows when both are loaded
  together.
• Red and orange are listed, never proposed, at any proof strength. The containment argument is
  sound for a red too; the house rule stands regardless — the pipeline does not get to initiate
  disarming a safety clause.

The trap that test found

The first draft of the non-widening test passed against a window in which nothing could ever change.
RECORDED injections replay a model-allowed call's own recorded allow, so removing a green over an
all-allow window reports changed: 0 whatever the clause does. Another instance of the wave's bug
shape — a silence that reads as success. The window is now built from fail-closed denies, which is both
the traffic a green is actually learned from and the only traffic a green's ablation can move, and the
zero sits next to a liveness assertion: removing the kept clause does move decisions.

What could not form a cycle, and the test for it

Findings are directed edges keep → drop. Two properties prevent a ring:

• At most one finding names any clause as drop. Otherwise a reviewer is asked to retire the same
  clause once per clause that covers it.
• Mutual containment is broken by id, keeping the lower. Two clauses whose patterns say the same
  thing each subsume the other, and emitting both directions is a two-cycle: accept both and the rule
  disappears entirely, which is the annihilation supersessionCycles exists to refuse. This was a
  real bug in the first implementation, not a hypothetical. Across the kinds of proof mutual
  containment cannot arise — an anchored matcher never subsumes a free substring — so the tie-break
  only ever fires on genuinely equal languages.

The test asserts acyclicity structurally and hands the findings to the real compilePolicy as the
supersedes edges §8.3 would have written, through the real parseLearnedClause. So even the shape
this PR declined to emit compiles. Removing the tie-break fails it.

Mutation evidence

Every guard reverted independently, propose.test.ts + pipeline.test.ts (108 tests) each time:

reverted	fails
same level / same tier	a broad clause and its narrower exception at a different level are never merged, never merges across tiers — 2 failed, 106 passed
safety-level exclusion	a red containment is listed, never proposed — 1 failed, 107 passed
mutual-containment tie-break	two clauses saying the same thing yield one finding, not a two-cycle, the findings can never form a supersession cycle — 2 failed, 106 passed
human-clause guard	never drops a human clause, whichever way containment runs — 1 failed, 69 passed
empty-pattern guard	never proposes retiring a prose clause on the strength of it having no matchers — 1 failed, 69 passed
the command-prefix prover	4 failed — its own detection test plus the three guard tests that need a detected pair to guard. The expected dependency: a guard on a detection cannot be exercised without the detection.

Surfaces

• RunLine.proposals.merges — never[] can now be typed properly, and is: MergeFinding[], with
  keep, drop, tier, level, proof, proposed and a verbatim note. Still [] rather than
  absent when there is nothing, so a reader never has to distinguish "no merges" from "this version
  did not report merges".
• candidates.merged counts only the proposed ones, and it now enters both the headline arithmetic
  (clauses: +1 −0 merge 1 = net 0) and exitReasonFor. A run whose only output is a merge finding
  has something a reviewer can act on; reporting it as no-shape-cleared-floor would be the same
  silence-reads-as-success bug pointing the other way.
• session-sitter learn prints one line per finding, = proposed, ? listed.
• --no-retire suppresses the static pass too. It is cheap and window-independent, and it is still a
  retirement — the flag's own help text says "so no retirement is proposed", and one flag meaning two
  things is how a governance surface starts lying.

Relationship to what ablation already finds

Ablation does reach the same clauses, as shadowed — the dropped clause matches real calls and
removing it changes nothing, so shadowed_by names the other clause. Two differences make the static
finding worth having beside it:

• Ablation needs the traffic. Subsumption is visible on a corpus with an empty window.
• shadowed is deliberately ambiguous — "delete as redundant or narrow to cover what the other
  rung does not" — because ablation cannot tell those apart. Same-level containment can: there is
  nothing to narrow onto, because a same-level narrower clause adds nothing.

Constraints

Zero runtime dependencies, TypeScript only, no model on the path, nothing written outside
assertWritable's permitted set (this lane writes nothing at all). Every fixture invented.

make check green: 2,722 → 2,736 tests, 106 files. make plugin run last;
ci/check-plugin-lib.sh reports plugin/lib is the current build of src/.

Known ceilings, marked in the source

• O(n²) over accepted clauses. A few hundred nodes; upgrade path is an index on the first pattern
  token.
• expires is not consulted, because nothing consumes it yet (the schema gap The pipeline can add and retire a clause, but never merge two #82's sibling tickets
  are about). Once decay ships, a pair whose expires differ must be refused: the kept clause could
  expire first and take the dropped clause's coverage with it. Noted at the call site.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.