Global ≡ premise under a CLIMB cov_BC entry

Status: open (the live frontier of the transitivity proof as of 2026-06-05)

For wp_mu’s global ≡ premise, the transitivity cover cov'' must satisfy ⋀ D'_image ≡ Cbody at empty contexts. The chain factors per cov_BC entry i as ⋀_k D'_{i,k} ≡ (mcod B'_i)^X ≡ D_i^X ≡ Cbody.

• RIGID cov_BC entry: mcod B'_i ≡ D_i holds both ways at empty (via wp_shrink), so the chain closes.
• CLIMB cov_BC entry: the cert is wp (add X Dr1) Dr2 (mcod B'_i)^X (D_i)^X — the +X is essential; at empty contexts only the forward leg survives (wp_shrink gives mcod B'_i^X → D_i^X, not the reverse). So mcod B'_i ≢ D_i at empty, and ⋀_k D'_{i,k} need not reassemble to D_i.

Proposed resolution (Option C, paper-verified, not mechanized)

Polarity-dispatch per entry: for CLIMB-i, emit a single merged cov'' entry (cover_src cov_A_i, D_i) whose +X is supplied externally by cov_BC’s CLIMB cert, so the global ≡ rides on cov_BC’s own pre-existing global premise rather than on reassembling cov_A_i’s pieces. Paper check passes all 5 clauses if (1) per-entry polarity is X-uniform, (2) the RIGID-i structural transport tiles D_i faithfully, (3) the depth bounds hold for the IH.

What would settle it

Mechanize Option C and confirm clause (e) under a non-pathological CLIMB cov_BC entry. (Note: the iso-recursive setting has no bottom type — μa.a is not ⊥ — so the earlier μa.a <: μm.(m∧Int) worry was a non-issue and was cut.)

Sources

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