Partial proof for bang_valid_of_allQuest

[aleph-prover-dev]

⚠️ Your proof request could only be partially completed
Some theorems may only have informal proofs available.
Some hard-to-prove facts may have been replaced with axioms.

---

Proven lemmas: 8/9

The main goal is to prove a “promotion” soundness theorem for phase semantics of linear logic: if Γ is a ?-context (Γ.allQuest) and the sequent ⟦a⟧ ⅋ ⟦Γ⟧ is valid, then (!⟦a⟧) ⅋ ⟦Γ⟧ is also valid. The proof has been decomposed into semantic lemmas that translate validity of a par (⅋) into an order condition, show how ? and ! interact with negation, and show that in an all-? context the interpretation of Γ is closed under applying ?. Concretely, several key steps are already proved: (G ⅋ H).IsValid ↔ (Gᗮ ≤ H), a duality lemma ʔ(Gᗮ) = (!G)ᗮ, monotonicity of ?, and the reduction that if X ≤ interpSequent Γ then ʔX ≤ interpSequent Γ when Γ.allQuest. Using these, the main theorem bang_valid_of_allQuest is essentially finished: validity gives ⟦a⟧ᗮ ≤ ⟦Γ⟧, closure gives ʔ(⟦a⟧ᗮ) ≤ ⟦Γ⟧, duality turns that into (!⟦a⟧)ᗮ ≤ ⟦Γ⟧, and then validity of (!⟦a⟧ ⅋ ⟦Γ⟧) follows.

At this point, 7 out of 8 sub-results are solved; the only remaining blocker is the lemma quest_closed_parr_quest_quest: ʔ((ʔG) ⅋ (ʔH)) ≤ (ʔG) ⅋ (ʔH). This lemma is the semantic heart needed inside the induction proving that interpSequent Γ is ?-closed when every formula in Γ is a ?. The current challenge is that straightforward automation (“grind”) fails after unfolding definitions, because the goal becomes a fairly intricate orthogonality/set-membership statement involving products and the idempotent set I. The intended strategy is to unfold ʔ and ⅋ to orthogonals, then explicitly build the needed idempotent “test element” in I (using the already-proved closure I_mul_mem) and feed it into the hypothesis to derive the required orthogonality; once that lemma is in place, the rest of the development should close with the existing chain of lemmas.