Gate subsumption — when passing A lets you skip B

Parent: gate-theory

Status: exploratory

The observation

Gates cost P×C, and gating everything is over-control: each gate destroys variety (Ashby). Sometimes checking gate A makes checking gate B redundant — A's acceptance guarantees B would accept. Then A subsumes B, and skipping B is free safety.

Subsumption

Gate A subsumes gate B (relative to the trajectory segment between them) iff every state that passes A and follows the verified dynamics to B necessarily passes B. Then B's check adds no information and may be skipped.

Two mechanisms

Static entailment — A's checks logically imply B's, independent of dynamics. Example: a type check subsumes a "no undefined variables" lint; a stronger test suite subsumes a weaker one. This makes the gate set a partial order under entailment; the economical harness runs only a minimal basis — the strongest antichain — and gets the rest for free.

Dynamic propagation (tube invariance) — A sits upstream, B downstream, and the segment between them provably preserves the property (an invariant, or a contraction k<1 on that segment, per gates-are-neighborhoods): in-the-tube at A ⟹ still-in-the-tube at B. This is exactly the Hoare-logic shape {P} S {Q}: verify P once at A, the verified segment carries it to Q at B — no re-check needed. Control-theory version: an invariant set — once inside, the dynamics keep you inside; gates are only needed at invariance boundaries, where new variety enters (external input, a reassembly join, a fallible move).

The economy: place gates only at boundaries

Subsumption turns gate placement from "gate everything" into a coverage problem: place gates exactly at the points NOT covered by propagation from earlier gates — where invariance can break. Fewer gates, same guarantee, less P×C spent on verification, less variety destroyed.

The catch: the subsumption claim is itself an artifact

"A ⟹ B" is a claim about the checks and the dynamics between them — and it needs its OWN verification, or it silently rots: the implication was true yesterday, then the segment was re-planned or the code changed, and B is now silently unguarded. Skipping B is safe only with a certificate of the implication (types, proofs, mechanical dependency analysis); assumed subsumption is precisely how gates silently disappear and the funnel becomes a tunnel. Also the tolerances compose: skipping B on the strength of A costs α_A + α_implication, not just α_A (honest-caveats).

First answers to the open questions

Discovery — measure, don't prove. Proving "check A implies check B" in general is hopeless (checks are programs; implication between programs hits Rice / undecidability). So measure it: kill-set inclusion. Feed the same corpus of seeded-bad artifacts (mutants) through both gates; if every mutant B kills, A also kills, then empirically A ⊇ B — this is exactly test subsumption from the mutation-testing literature. It comes with its own confidence α (relative to the corpus): a subsumption claim is itself a softened gate — the theory applies to itself. (Between mechanical tools the hierarchy is an a-priori certificate instead: a type check provably implies a no-undefined-vars lint.)

Invalidation — build-cache semantics. Record each claim as {A, B, content-hash of its support set} (the checks' definitions + the segment between them). Any edit that touches the support changes the hash → the claim dies → B's gate resurrects until re-certified. This is make/Bazel incrementality; and it is the dual of no-goods: no-goods cache failures (which worlds collapsed), subsumption claims cache successes (which checks are entailed) — both are monotone knowledge with dependency-scoped validity.

Fallible moves reset the tube — and that yields a placement theorem. Every fallible (LLM) move is a variety-injection point = an invariance boundary; dynamic subsumption never crosses one. Hence: the minimal gate basis = one gate after each fallible move, scoped to that move's write-set / blast radius; whatever the move didn't touch has an unchanged content-hash = trivially preserved (this is test-impact analysis). Between mechanical segments, propagation is free. This matches practice: you re-test after the LLM edits, not after the compiler runs.

The useful formalization is kill-sets, not the abstract lattice. Map each gate to the set of failure modes it catches; subsumption = set inclusion; then "which gates to run" = weighted set cover (weights = each gate's P×C, constraint = cover the target failure modes) — NP-hard, greedy gives the classic ln n approximation. So gate placement is itself an optimization problem: the logic→optimization migration closes the loop on the control layer itself — even the controller's design lands in optimization.