prove C_conseq: monotonicity of jointCondition modality

[pirapira]

Summary

• Proves C_conseq (issue Proof obligation for C_conseq in src/Bluebell/Logic/JointCondition.lean #183): the consequence/monotonicity rule for the 𝑪_ modality
• Reuses the same existential witnesses (P, p, κ) and applies the entailment hypothesis to convert K₁ v to K₂ v for each v in the PMF support

Closes #183

🤖 Generated with Claude Code

[github-actions]

🤖 Gemini PR Summary

This PR formalizes a key property of the 𝑪_ (joint condition) modality within the Bluebell logic framework. It specifically addresses the monotonicity rule, allowing for the substitution of weaker conditions within the modality.

Features

• Formal Proof of C_conseq: Successfully implemented the consequence/monotonicity rule for the joint condition operator.
• Logic Formalization: Leverages existential witnesses ($P$, $p$, $\kappa$) to demonstrate that if an entailment holds between two predicates $K_1 \implies K_2$, the joint condition modality preserves this relationship across the PMF (Probability Mass Function) support.

Fixes

• Closes Proof obligation for C_conseq in src/Bluebell/Logic/JointCondition.lean #183 (Implementation of the C_conseq theorem).

---

File-level changes

• src/Bluebell/Logic/JointCondition.lean: Contains the formal Lean proof for the C_conseq theorem.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	3
❌ Lines Removed	1

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• theorem C_conseq (h : ∀ v, K₁ v ⊢ K₂ v) : 𝑪_ μ K₁ ⊢ 𝑪_ μ K₂ in src/Bluebell/Logic/JointCondition.lean

---

🎨 **Style Guide Adherence**

All changes adhere to the style guide.

---

📄 **Per-File Summaries**

• src/Bluebell/Logic/JointCondition.lean: Formalizes the proof of the C_conseq theorem, establishing monotonicity for the joint condition operator.

---

Last updated: 2026-02-17 16:54 UTC.

[pirapira]

This should be held back till the foundation changes.