Tony's Wiki

wp Transitivity via Cover Routing (v3 → v4 → Option C)

3 min read

wp Transitivity via Cover Routing

How transitivity of wp (wp_trans_gen, with ISub_trans as its ∅;∅ instance) is being mechanized, and the architectural wall that dominated the 2026-05-31 → 06-05 bcd-full work. Distilled from Claude Code session transcripts.

The reduction

ISub := wp ∅ ∅ is definitional, so ISub_trans is just wp_trans_gen at empty contexts (confirmed repeatedly — it is not mutually inductive with a lifting lemma; see the correction in Size-Stratified Mutual Transitivity). wp_trans_gen is by depth induction; every case closes except wp_mu_compose_case — the μ-vs-μ composition — which is gated on a single lemma route_per_entry_v3.

The core problem: routing a transitivity cover

To compose wp A M ∘ wp M (μC), the proof must build a cover cov'' for A <: μC out of A’s cover and M’s cover (cov_BC, from inverting wp M (μC)). Each cov'' entry needs a CLIMB or RIGID certificate. The composition table (proven, musub_compose):

CLIMB ∘ CLIMB = CLIMB    CLIMB ∘ RIGID = CLIMB
RIGID ∘ CLIMB = CLIMB    RIGID ∘ RIGID = RIGID

— because a CLIMB on either side contributes the add X to the unioned context (via the IH’s context union), so the only RIGID output is RIGID∘RIGID.

The wall

The failing case is cov_BC RIGID at X while a cov_A entry is CLIMB at X. The v3 construction merged all of A’s μ-leaves into one source cover_src cov_A per cov_BC entry; but cover_src_fwd absorbs the CLIMB marker (it shrinks each cert to a bare forward, dropping the add X and the RIGID reverse). So the merged source can satisfy neither leg, and a spurious sub-obligation like wp ∅ ∅ X Int appears that no rule discharges.

It is NOT an algorithmic incompleteness

The decisive 2026-06-05 finding (after the user asked whether the wall implies an incomplete example): no counterexample to wp_trans exists — the wall is a proof-strategy artifact, not a gap in the rule. Verified on cov_example (A = (μa.a→Int) ∧ (μb.Int→(b∧Int)), M = μc.((c→Int)∧(Int→c))): the merged source manufactures wp ∅ ∅ X Int (false), but that sub-obligation never occurs in a real derivation — it is spurious to the merge. (Contrast the genuine rule-level incompleteness fixed earlier by deep splitting: Incompleteness of the Algorithmic Mu-Rule.)

The fix: per-entry source, never merged

  • v4 (i,k)-flat — invert wp M (μC) per cov_BC entry B'_i (not once at the merged source); cov'' = flat over (i,k) with each entry’s source a single cov_A entry A'_{i,k}. Per-entry CLIMB is preserved because the body-level transport runs at empty contexts, so the IH union ∅ ∪ (D1,D2) keeps cov_A’s add X.
  • Option C — polarity-dispatch per cov_BC entry: RIGID-i → v4 (i,k)-flat with a structural-transport target D'_image_{i,k}; CLIMB-i → a single merged entry (cover_src cov_A_i, D_i), where the needed +X is supplied externally by cov_BC’s CLIMB cert, so cover_src_fwd’s absorption no longer matters.

The remaining concrete work is the structural transport bridge wp ∅ ∅ (D'_{i,k})^X (D'_image_{i,k})^X by induction on dpart D'_{i,k} (mcod B'_i)^X (~150–200 LOC, no axioms). Open sub-concern: the global ≡ premise under a CLIMB cov_BC entry — see Global equiv premise under CLIMB cov_BC.

Split-Cover and Polarity Certificates · Weakly Positive Subtyping · Incompleteness of the Algorithmic Mu-Rule · Size-Stratified Mutual Transitivity · Does the cover CLIMB-RIGID wall imply algorithmic incompleteness · Proof Engineering Lessons (Rocq wp_isorec)

Sources

Claude Code sessions 25ab7e44 (05-31), 271dc5fa (06-04), 1f01730a/2eecaeb4/ed9a9e97 (06-04), 11cf3241 (06-05). See 2026-06-04, 2026-06-05.

Graph View

Backlinks