Cross-tier coherence for the relational RelWP carriers

The three relational tiers (Qualitative, Probabilistic, Quantitative) form a chain of refinements analogous to the unary case (see VCVio/ProgramLogic/Unary/Loom/Coherence.lean):

                       indicator                       .val
  α → β → Prop  ─────────────────────▶  α → β → Prob  ─────────▶  α → β → ℝ≥0∞
  (CouplingPost)                        ([0, 1])                  (eRelWP)

Both edges have coherence lemmas relating their rwp values:

• Probabilistic ↔ Quantitative (definitional, rfl): the underlying ℝ≥0∞ value of a probabilistic rwp is the quantitative rwp on the same post, viewed under Subtype.val. This is already proved as OracleComp.Rel.Probabilistic.rwp_val_eq_eRelWP in …/Loom/Probabilistic.lean.
• Qualitative ↔ Quantitative (this file, non-trivial): a coupling satisfying a Prop-valued relation R exists iff the quantitative eRelWP on the indicator of R equals 1. This reduces to the existing relTriple'_iff_couplingPost bridge in VCVio/ProgramLogic/Relational/Quantitative.lean.

Why state these against eRelWP rather than Std.Do'.rwp?

Both OracleComp.Rel.Qualitative.instRelWP and OracleComp.Rel.Probabilistic.instRelWP_prob are scoped instances. To use Std.Do'.rwp for both at once we would have to open two namespaces simultaneously, and Std.Do'.RelWP's Pred is an outParam, which would back out instance synthesis. Stating the lemmas against eRelWP (and CouplingPost) directly sidesteps the conflict; once a downstream user has chosen a single carrier, they can rewrite from Std.Do'.rwp _ _ _ _ _ to eRelWP _ _ _ (or CouplingPost _ _ _) via the keystone rfl lemmas in the per-carrier files (rwp_eq_eRelWP, rwp_eq_couplingPost, rwp_val_eq_eRelWP).

See .ignore/wp-cutover-plan.md §"Three-tier carrier design" for the broader story.

Bound: eRelWP on an indicator post is always ≤ 1

The relational expectation of an indicator post is bounded by 1, since the indicator itself is ≤ 1 pointwise and any coupling has total mass ≤ 1.

theorem OracleComp.Rel.Loom.Coherence.eRelWP_indicator_le_one {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : ProgramLogic.Relational.RelPost α β) : ProgramLogic.Relational.eRelWP oa ob R.indicator ≤ 1

Probabilistic ↔ Quantitative

The probabilistic Std.Do'.rwp agrees with the quantitative eRelWP under Subtype.val by rfl; that statement lives in …/Loom/Probabilistic.lean as OracleComp.Rel.Probabilistic.rwp_val_eq_eRelWP. We do not restate it here because pulling OracleComp.Rel.Probabilistic.instRelWP_prob into scope to talk about Std.Do'.rwp requires open OracleComp.Rel.Probabilistic, which then occludes the qualitative tier discussed below.

Qualitative ↔ Quantitative (coupling-existence vs total mass)

For an OracleComp pair, the support-based Prop-valued relational WP (CouplingPost) holds iff the quantitative eRelWP on the indicator post equals 1.

theorem OracleComp.Rel.Loom.Coherence.couplingPost_iff_eRelWP_indicator_eq_one {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : ProgramLogic.Relational.RelPost α β) : ProgramLogic.Relational.CouplingPost oa ob R ↔ ProgramLogic.Relational.eRelWP oa ob R.indicator = 1

Qualitative ↔ Quantitative coherence: a Prop-valued relation holds along some coupling iff the indicator of that relation has quantitative eRelWP equal to 1.

This is the relational analogue of OracleComp.Loom.Coherence.wp_qual_iff_wp_prob_indicator_eq_one in the unary file, and it reduces to the existing relTriple'_iff_couplingPost bridge plus the upper bound eRelWP_indicator_le_one.

theorem OracleComp.Rel.Loom.Coherence.couplingPost_iff_relTriple' {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : ProgramLogic.Relational.RelPost α β) : ProgramLogic.Relational.CouplingPost oa ob R ↔ ProgramLogic.Relational.RelTriple' oa ob R

Convenience: rewrites the couplingPost_iff_eRelWP_indicator_eq_one bridge as a RelTriple' equivalence. The RelTriple' form is the eRHL-style triple with pre = 1.