Pointwise ↔ Update-Theoretic Bridge

@cite{charlow-2021} @cite{muskens-1996} @cite{charlow-2019}

Connects the pointwise DRS S := S → S → Prop type (Dynamic Ty2, @cite{muskens-1996}) to the update-theoretic StateCCP W E := State W E → State W E type.

The key operations are @cite{charlow-2021}'s ↑ (lift) and ↓ (lower):

• liftPW: promotes a pointwise DRS to a context-level update
• lowerPW: extracts a pointwise relation from a context update

The central result: liftPW D is always distributive, meaning pointwise meanings can never produce irreducibly context-level effects. Cumulative readings require non-distributive M_v, which lives only in StateCCP.

def Semantics.Dynamic.Core.PointwiseUpdate.liftPW {W : Type u_1} {E : Type u_2} (D : DynProp.DRS (Assignment E)) : StateCCP W E

Charlow's ↑ (equation 76): lift a pointwise DRS to an update on states. liftPW D s = {⟨w, h⟩ | ∃ ⟨w, g⟩ ∈ s, D g h} Each world-assignment pair in the output comes from applying D to some input assignment in s, preserving the world.

Equations

• Semantics.Dynamic.Core.PointwiseUpdate.liftPW D s = {p : W × Core.Assignment E | ∃ (q : W × Core.Assignment E), q ∈ s ∧ p.fst = q.fst ∧ D q.snd p.snd}

def Semantics.Dynamic.Core.PointwiseUpdate.lowerPW {W : Type u_1} {E : Type u_2} (K : StateCCP W E) (w₀ : W) : DynProp.DRS (Assignment E)

Charlow's ↓ (equation 77): extract a pointwise DRS from a state update. Evaluates K on a singleton context at an arbitrary world.

Equations

• Semantics.Dynamic.Core.PointwiseUpdate.lowerPW K w₀ g h = ((w₀, h) ∈ K {(w₀, g)})

theorem Semantics.Dynamic.Core.PointwiseUpdate.lowerPW_liftPW {W : Type u_1} {E : Type u_2} (D : DynProp.DRS (Assignment E)) (w₀ : W) : lowerPW (liftPW D) w₀ = D

Round-trip identity: lowering a lifted DRS recovers the original.

↓(↑D) = D because the singleton context {(w₀, g)} passes through ↑ with only (w₀, g) as witness, leaving exactly the pairs h with D g h.

theorem Semantics.Dynamic.Core.PointwiseUpdate.liftPW_injective {W : Type u_1} {E : Type u_2} [Nonempty W] (D₁ D₂ : DynProp.DRS (Assignment E)) (h : liftPW D₁ = liftPW D₂) : D₁ = D₂

↑ is injective: distinct DRSs yield distinct state updates.

Follows from the round-trip: D = ↓(↑D), so ↑D₁ = ↑D₂ implies D₁ = ↓(↑D₁) = ↓(↑D₂) = D₂. Requires W to be nonempty for the lowering witness world.

theorem Semantics.Dynamic.Core.PointwiseUpdate.liftPW_preserves_distributive {W : Type u_1} {E : Type u_2} (D : DynProp.DRS (Assignment E)) : IsDistributive (liftPW D)

Lifted pointwise DRSs are always distributive (@cite{charlow-2021}, §6, key lemma).

↑D processes each element of the input state independently — the output at p depends only on whether some q ∈ s satisfies D q.2 p.2 with matching world p.1 = q.1. This is exactly the singleton decomposition (↑D)(s) = ⋃_{i∈s} (↑D)({i}), which is the definition of distributivity.

theorem Semantics.Dynamic.Core.PointwiseUpdate.liftPW_lowerPW_not_id {W : Type u_1} {E : Type u_2} [Nonempty W] [Nonempty E] : ∃ (K : StateCCP W E), ∃ (w₀ : W), liftPW (lowerPW K w₀) ≠ K

↑↓ ≠ id: there exist irreducibly update-theoretic meanings K such that liftPW (lowerPW K w₀) ≠ K.

The simplest witness is K _ = {(w₀, g₀)} (constant function ignoring input). Then K ∅ = {(w₀, g₀)}, but liftPW (lowerPW K w₀) ∅ = ∅ because ↑ has no input pairs to draw.

Requires Nonempty W and Nonempty E to construct the witness.