Split-Cover and Polarity Certificates
The algorithmic engine of wp subtyping. To decide A <: C, the algorithm builds a cover: it matches each cont-leaf of the target C against an entry (A', D) where A' is an AllMu part of the source A, each entry carrying a certificate with a single polarity.
The two polarities
- CLIMB — covariant entry; allows subsumption (
A1 <: T1). Used when the matched position is covariant. - RIGID — contravariant/invariant entry; demands an exact match (
A2 ≈ T2). Forced when a contravariant occurrence is present (wp_rigid_to_climbis false — you cannot weaken RIGID to CLIMB).
The core limitation
A cover certificate carries one polarity for a whole cont-leaf.
When a single ordinary leaf (e.g. an arrow Int → (T1 & T2)) mixes a covariant part (T1, wants CLIMB) and a contravariant part (T2, wants RIGID), no single certificate can satisfy both. The leaf cannot be split among entries at ordinary-leaf granularity. This coarse bundling is the root cause of both:
- Incompleteness of the Algorithmic Mu-Rule, and
- the stuck point in transitivity — the
(RIGID ‖ CLIMB) ∘ RIGIDmerge.
The fix is to refine the cover: see Deep Target Splitting.
Mechanization status (as of 2026-06-04)
Structural side — cont_leaves, and_fold, global premise, dpart, completeness — largely Qed. wp_trans_gen / ISub_trans stuck on wp_mu_compose_case per-entry cert; current frontier is the A-RIGID-coarse ∘ cov-RIGID back-propagation/precision lemma and the wp_mu case of wp_weaken_fresh.
Composing certificates (transitivity)
The proven composition table (musub_compose), through a shared middle:
CLIMB ∘ CLIMB = CLIMB CLIMB ∘ RIGID = CLIMB
RIGID ∘ CLIMB = CLIMB RIGID ∘ RIGID = RIGID
A CLIMB on either side contributes its add X to the unioned context via the IH, so RIGID output requires RIGID on both. The transitivity trap is that aggregating sources via cover_src_fwd absorbs the CLIMB marker (drops the add X), so a merged source can serve neither leg — the wall analyzed in wp Transitivity via Cover Routing.
Related
Weakly Positive Subtyping · Distributivity Subtyping Laws · Deep Target Splitting · Incompleteness of the Algorithmic Mu-Rule · wp Transitivity via Cover Routing