pRHL up-to-bad and rectangular rules

• ProgramDenotation.relE.up_to_bad — the Fundamental Lemma of game-playing as a corollary of a relE judgment whose post says "the bad flags agree, and on good runs the win indicator agrees". Note the post is parameterized by the indicator G rather than demanding full state equality on good runs: in real games the related states may still differ in parts G cannot see (e.g. the random-oracle entry at the challenge point).
• ProgramDenotation.rel.of_unary — the rectangular rule: a relational judgment from two unary facts ("p almost surely lands in P" and "q has mass 1 on Q"). Needed when the two sides genuinely diverge (e.g. after the bad event) and the only maintainable invariant is one-sided.

theorem GaudisCrypt.ProgramDenotation.relE.up_to_bad {s α : Type} {p q : ProgramDenotation s α} {bad : s → Prop} [DecidablePred bad] {Post : α × s → α × s → Prop} (G : α × s → ENNReal) (h : p.relE q Eq Post) (h_bad : ∀ (x y : α × s), Post x y → (bad x.2 ↔ bad y.2)) (h_good : ∀ (x y : α × s), Post x y → ¬bad x.2 → G x = G y) (σ : s) : p.wp G σ ≤ q.wp G σ + p.wp (fun (x : α × s) => if bad x.2 then G x else 0) σ

Up-to-bad (Fundamental Lemma, relational form). From a diagonal relE whose post forces agreement of the bad flag and of G on good runs, conclude Pr[p : G] ≤ Pr[q : G] + Pr[p : bad ∧ G].

theorem GaudisCrypt.ProgramDenotation.relE.bad_eq {s α : Type} {p q : ProgramDenotation s α} {bad : s → Prop} [DecidablePred bad] {Post : α × s → α × s → Prop} (h : p.relE q Eq Post) (h_bad : ∀ (x y : α × s), Post x y → (bad x.2 ↔ bad y.2)) (σ : s) : p.wp (fun (x : α × s) => if bad x.2 then 1 else 0) σ = q.wp (fun (y : α × s) => if bad y.2 then 1 else 0) σ

The bad-event probabilities agree under the same relE judgment (companion to ProgramDenotation.relE.up_to_bad; in the unary development this took a separate mass-conservation chain).

theorem GaudisCrypt.ProgramDenotation.rel.of_unary {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {P : α × s₁ → Prop} [DecidablePred P] {Q : β × s₂ → Prop} [DecidablePred Q] (hP : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → p.wp (fun (x : α × s₁) => if P x then 0 else 1) σ₁ = 0) (hQ : ∀ (σ₁ : s₁) (σ₂ : s₂), Pre σ₁ σ₂ → q.wp (fun (y : β × s₂) => if Q y then 1 else 0) σ₂ = 1) : p.rel q Pre fun (x : α × s₁) (y : β × s₂) => P x ∧ Q y

Rectangular rule: if p almost surely lands in P (from Pre-related states) and q has full mass on Q, then p ~ q at the rectangular post P × Q. The two sides need not be coupled at all.