Size-Stratified Mutual Transitivity

The plan (2026-05-23) for proving transitivity of wp in the presence of the lifting lemma, resolving an apparent circularity.

Superseded framing (2026-06-04 transcripts)

On the bcd-full branch the mutual lifting ↔ transitivity scheme below was not how transitivity was actually structured. Because ISub := wp ∅ ∅ definitionally, ISub_trans is just the ∅;∅ instance of wp_trans_gen (by depth induction), confirmed repeatedly to be not mutually inductive with a lifting lemma. The real live obstruction became cover-routing in wp_mu_compose_case — see wp Transitivity via Cover Routing. Keep this page as the historical 05-23 idea.

The circularity

Orbit reasoning requires transitivity of ISub. But the lifting lemma (weakly-positive) is used in proving transitivity. So transitivity and the lifting lemma appear mutually dependent.

The resolution: stratify by size

Assume transitivity only for types strictly smaller than those in the premise, then run a mutual induction:

1. Transitivity-for-smaller-types ⇒ proves the lifting lemma for weakly positive.
2. The lifting lemma ⇒ proves transitivity in full power.

The size measure breaks the cycle: each use of the assumed transitivity is at a strictly smaller type.

The stuck point (2026-06-04)

wp_trans_gen / ISub_trans are blocked on wp_mu_compose_case — the per-entry certificate of a matched cover. The hard residual is the (RIGID ‖ CLIMB) ∘ RIGID merge: composing a coarse RIGID certificate with a covariant RIGID one needs a back-propagation / precision lemma. This is the same coarse-granularity bundling that causes incompleteness — so Deep Target Splitting (uniform-polarity pieces) is expected to unstick transitivity too.

Also open: the wp_mu case of wp_weaken_fresh.

Related

Weakly Positive Subtyping · Split-Cover and Polarity Certificates · Deep Target Splitting · Distributivity Subtyping Laws

Sources

2026-05-23, 2026-06-04