Does the cover CLIMB/RIGID wall imply algorithmic incompleteness?

Status: resolved (2026-06-05) — No.

The transitivity proof stalls on the case cov_BC RIGID at X + a cov_A entry CLIMB at X (wp Transitivity via Cover Routing). The question (raised by the user): does this stuck case witness an incomplete example — a judgment that holds in the declarative system (via transitivity + dist-mu) but that the algorithmic wp rule cannot derive?

Answer

No counterexample to wp_trans exists. Verified on cov_example as the transitivity middle (A = (μa.a→Int) ∧ (μb.Int→(b∧Int)), M = μc.((c→Int)∧(Int→c))): the v3 merged-source construction manufactures a spurious sub-obligation wp ∅ ∅ X Int (false), but that obligation never arises in a real derivation — it is an artifact of merging A’s leaves. The v4 (i,k)-flat construction, with each cov'' entry sourced from a single cov_A entry, derives the same composition with no spurious obligation. So the wall is a proof-strategy artifact, not a rule incompleteness.

This is a different layer from the genuine rule-level incompleteness fixed earlier by deep splitting: that one was the rule failing on a real declarative judgment; this one is only the merged-source proof tactic failing.

Residual

The fix (v4 (i,k)-flat / Option C) is designed but not yet mechanized; it leaves an open sub-question on the global premise — Global equiv premise under CLIMB cov_BC.

Sources

Session 11cf3241 (2026-06-05). See 2026-06-05.