Proof obligation for `C_unit_left` in `src/Bluebell/Logic/JointCondition.lean`

[alexanderlhicks]

A proof in src/Bluebell/Logic/JointCondition.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem states that the joint conditioning modality 𝑪_ behaves as a unit element when applied to a deterministic probability distribution.

The goal is to prove an equivalence (⊣⊢) between two hyper-assertions:

1. 𝑪_ (MeasureTheory.Measure.dirac v₀).toPMF K: This is the joint conditioning modality applied with a probability mass function (PMF) that is deterministic. The dirac v₀ measure concentrates all probability mass at the single point v₀, so this models a situation where the outcome is known to be v₀ with certainty.
2. K v₀: This is the hyper-assertion from the family K corresponding to the single outcome v₀.

In essence, the theorem says that conditioning on a certain event v₀ is logically equivalent to simply asserting the hyper-assertion associated with v₀.

Context

This theorem is a fundamental "unit law" or "elimination rule" for the jointCondition modality (𝑪_). The 𝑪_ modality is designed to reason about properties that hold across all possible outcomes of a random process described by a PMF μ. This theorem provides a crucial sanity check: when the random process is not random at all (i.e., it's deterministic), the complex modality should simplify to a direct assertion.

This is analogous to unit laws in other contexts, for example, (return x) >>= f simplifying to f x in monads. It connects the general, probabilistic reasoning power of 𝑪_ back to the simpler, non-probabilistic fragment of the logic. Such properties are essential for ensuring the modality is well-behaved and for simplifying proofs involving deterministic cases.

Proof Suggestion

The proof goal is an equivalence (⊣⊢), which corresponds to proving entailment in both directions. You should structure your proof accordingly, likely using apply iff_entails.mpr; split or a similar tactic.

1. Direction 1: 𝑪_ (MeasureTheory.Measure.dirac v₀).toPMF K ⊢ K v₀

This is the more straightforward direction.

1. Start with intro a ha to assume a is a resource where the left-hand side holds.
2. Unfold the definition of jointCondition in ha. This will give you existential witnesses: a family of probability spaces P, permissions p, compatibility proofs h, and kernels κ.
3. You will also have three conditions relating these witnesses to a and K.
4. Simplify these conditions using the properties of μ := (MeasureTheory.Measure.dirac v₀).toPMF.
   • The support μ.support is the singleton set {v₀}. This simplifies the universal quantification over the support to a single case for v₀.
   • The measure μ.toMeasure is Measure.dirac v₀. The condition (P i).μ = μ.toMeasure.bind (κ i) will simplify to (P i).μ = κ i v₀.
5. Use this equality to show that the resource passed to K v₀ in the third condition is precisely the resource res := (fun i => ⟨⟨WithTop.some (P i), p i⟩, h i⟩) constructed from the witnesses.
6. You now have res ≤ a (from the first condition) and res ∈ K v₀ (from the third, simplified condition).
7. Since K v₀ is a HyperAssertion, it is an UpperSet and thus upward-closed. From res ≤ a and res ∈ K v₀, you can conclude a ∈ K v₀.

2. Direction 2: K v₀ ⊢ 𝑪_ (MeasureTheory.Measure.dirac v₀).toPMF K

This direction is more challenging as it requires constructing witnesses.

1. Start with intro a ha, where ha : a ∈ K v₀. The goal is to show that a is in the set defined by jointCondition, which means proving an existential statement.
2. You need to provide witnesses for P, p, h, and κ. The key is to construct a resource res of the "concrete" form fun i => ⟨⟨WithTop.some (P i), p i⟩, h i⟩ that satisfies two properties:
   • res ≤ a (inclusion in the CMRA sense).
   • res ∈ K v₀.
3. A natural first attempt is to use a itself to construct res. If a is already in this concrete form (i.e., none of its PSp components are ⊥), you can extract P, p, and h directly from a. In this case, res would be a, res ≤ a is trivial, and res ∈ K v₀ is exactly the hypothesis ha.
4. The main difficulty is the general case where a may contain ⊥ components for some probability spaces. You need to find a way to construct a "concrete" resource res that is included in a (res ≤ a) and for which you can prove res ∈ K v₀. This step might require a lemma about the structure of the IndexedPSpPm CMRA, possibly showing that any resource a can be decomposed into a concrete part and a remainder.
5. Once you have such a res (built from P, p, h), you can define the kernel κ as κ i v₀ := (P i).μ (and some arbitrary measure for v ≠ v₀) to satisfy the measure equality condition. The sorry for IsProbabilityMeasure in the definition of jointCondition can be discharged because (P i).μ is a probability measure by construction.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_unit_left [Countable β] [MeasurableSingletonClass β] {v₀ : β} :
    𝑪_ (MeasureTheory.Measure.dirac v₀).toPMF K ⊣⊢ K v₀ := by
  sorry