Incompleteness of the Algorithmic μ-Rule

A concrete witness (2026-05-31) that the algorithmic μ-rule is incomplete relative to the declarative system, independent of transitivity — even just deciding A <: C fails.

The witness

A  = μa.(Int→A1) & μa.(Int→A2)
C  = μa.(Int→(T1&T2))
with   A1 <: T1   (covariant, CLIMB)
       A2 ≈ T2    (contravariant, RIGID)

Declarative side holds:

A = μ(Int→A1) & μ(Int→A2)
  <: μ((Int→A1)&(Int→A2))     (dist-mu)
  <: μ(Int→(A1&A2))           (dist-arrow, under μ)
  <: μ(Int→(T1&T2)) = C       (A1<:T1, A2<:T2 ⇒ A1&A2 <: T1&T2)

The algorithm produces no cover. C’s body opens to a single cont-leaf Int→(T1&T2) (one ordinary arrow), which must be covered by one entry (A', D):

• A' = μ(Int→A1) → needs A1 <: T1&T2; A1 unrelated to T2. ✗
• A' = μ(Int→A2) → symmetric, A2 <: T1 fails. ✗
• A' = A (the merge) → forward works (dist-arrow), but the leaf codomain T1&T2 mixes a contravariant part (via T2), so the certificate cannot be CLIMB (wp_rigid_to_climb false) → forced RIGID → reverse needs T1&T2 <: A1, contradicting strict A1 <: T1. ✗

No fourth option (a single ordinary leaf can’t be split among entries) — so no cover exists though A <: C declaratively.

Why — the same wall as transitivity

A cover certificate carries one polarity for a whole cont-leaf. When that leaf’s arrow codomain mixes a covariant part (wants CLIMB) and a contravariant part (wants RIGID), no single certificate fits. The declarative system escapes because dist-arrow decouples the covariant subsumption from the rigid match. This coarse bundling is the same stuck point as the (RIGID ‖ CLIMB) ∘ RIGID merge in transitivity.

The fix

Deep Target Splitting — push intersection-splits down into arrow codomains (and μ) so every piece has a determinate single polarity.

Don’t confuse this with the transitivity-proof wall

This is a rule-level incompleteness (the algorithmic rule rejected a genuine declarative judgment), fixed by deep splitting. A later, superficially similar wall — cov_BC RIGID + cov_A CLIMB while mechanizing transitivity of the fixed rule — turned out not to be an incompleteness at all, but a proof-strategy artifact of a merged-source cover. See wp Transitivity via Cover Routing and Does the cover CLIMB-RIGID wall imply algorithmic incompleteness.

Sources

2026-05-31; transcript session 25ab7e44.