Observations: the information lattice of a single move

This file defines Multiparty.Observation X, the maximally general single-projection form of a local view at a node whose move space is X, together with its information-lattice algebra.

Observation X = Σ Obs : Type u, X → Obs is one quotient morphism X → Obs packaged with its codomain. Three independent literature traditions converge on this exact object:

• Halpern-Vardi epistemic logic ("Reasoning About Knowledge"): an agent's observation is a projection from global state to local indistinguishability classes;
• Goguen-Meseguer noninterference / Sabelfeld-Myers info-flow: per-level projection of observable outputs;
• Honda-Yoshida-Carbone multiparty session types and Cruz-Filipe-Montesi endpoint projection: projection of a global type / global play to one role's local view.

Polynomial substrate

Observation is built directly on top of the polynomial-functor library in ToMathlib/PFunctor, mirroring the pattern by which Interaction.Spec is built from Spec.basePFunctor:

Observation X := PFunctor.Idx (Observation.basePFunctor X)

where Observation.basePFunctor X : PFunctor.{u+1, u} has positions Type u (one position per observation codomain) and a child family Obs ↦ X → Obs (the projections from X into that codomain). Thus an observation of X is precisely an element (in PFunctor.Idx terms) of this polynomial: a chosen codomain Obs together with a projection X → Obs. The Σ-form Σ Obs : Type u, X → Obs is recovered definitionally because PFunctor.Idx P unfolds to Σ a, P.B a. The polynomial substrate is the truth; the Observation name is an ergonomic re-skin in the spirit of OracleSpec / OracleComp and Spec.done / Spec.node.

Information lattice

The intended order on Observation X is informativeness, ordered low ≤ high:

• Observation.bot X = ⟨PUnit, fun _ => PUnit.unit⟩ is the bottom of the lattice: zero information, the coarsest (one-class) partition.
• Observation.top X = ⟨X, id⟩ is the top: full information, the finest (all-singleton) partition.
• Observation.Refines k₁ k₂ (k₁ ⊑ k₂) means "k₁ reveals no more than k₂": the projection of k₁ factors through that of k₂.
• Observation.combine k₁ k₂ is the join in the information lattice: the Σ-product of both kernels, i.e. the universal kernel that records what is learned by jointly observing through k₁ and k₂.
• Observation.postcomp k f post-composes the projection of k with f, yielding a kernel that is automatically refined by k (a downgrade).

The dual meet (greatest common reduction, the coarsest kernel that both refine) requires quotienting X by the joint indistinguishability relation and is deferred until a use case requires it.

Mathlib lattice notation

The named operations above are also exposed via Mathlib's order typeclasses so that standard notation works on Observation X:

• (⊤ : Observation X) = Observation.top X via Top;
• (⊥ : Observation X) = Observation.bot X via Bot;
• k₁ ≤ k₂ denotes k₁.Refines k₂ via LE and Preorder;
• bot_le and le_top come from the OrderBot and OrderTop instances;
• k₁ ⊔ k₂ = Observation.combine k₁ k₂ via Max.

Note that Refines is only a preorder, not a partial order: two observations may mutually refine each other through different bijections of their codomains (e.g. ⟨X × Y, _⟩ and ⟨Y × X, _⟩). For that reason we do not declare SemilatticeSup (which would require antisymmetry); the join-style theorems for combine are stated as named lemmas instead.

A practical payoff is that Pi-instance lifting in Mathlib then transfers all of this notation pointwise to per-party observation profiles Party → Observation X (see Multiparty/ObservationProfile.lean) for free.

Action shape

Observation.Action k m Cont is the maximally general local node type associated to a kernel: it asks the participant to commit to a uniform continuation family conditioned on the observation o : k.1. The four-mode operational refinement and its rfl-friendly action shapes live in Multiparty/Core.lean (ViewMode); this file only knows the universal form.

@[reducible]

def Interaction.Multiparty.Observation.basePFunctor (X : Type u) : PFunctor.{u + 1, u}

The polynomial functor whose index type is Multiparty.Observation X: positions are observation codomains Type u, and the child family at a position Obs : Type u is the type of projections X → Obs.

Following the convention established by Interaction.Spec.basePFunctor, this exposes Observation X as the index type PFunctor.Idx (basePFunctor X) = Σ Obs : Type u, X → Obs of a specific polynomial functor: the universal "observations of X" container. An element of the polynomial is precisely a chosen codomain together with a projection from X into it.

@[reducible, inline]

abbrev Interaction.Multiparty.Observation (X : Type u) : Type (u + 1)

Observation X is the polynomial-element form of a local view at a node whose move space is X: a single quotient morphism toObs : X → Obs packaged with its codomain Obs.

It is definitionally the index type of Observation.basePFunctor X: Observation X = PFunctor.Idx (basePFunctor X) = Σ Obs : Type u, X → Obs, mirroring the pattern by which Interaction.Spec is defined as PFunctor.FreeM Spec.basePFunctor PUnit. The Σ-pair literal ⟨Obs, π⟩ works directly as a constructor, and the projections k.1 / k.2 recover the codomain and projection.

This is the maximally general "what does a participant see" primitive. It is the carrier of the information lattice (see Observation.top, Observation.bot, Observation.Refines, Observation.combine).

Operationally specialized observations with simpler Action shapes live in Multiparty/Core.lean as the four-constructor ViewMode type; every ViewMode collapses to an Observation via ViewMode.toObservation, and every Observation lifts back into ViewMode via Observation.toViewMode (equivalently, the universal ViewMode.react constructor).

def Interaction.Multiparty.Observation.top (X : Type u) : Observation X

Observation.top X = ⟨X, id⟩ is the top of the information lattice on X: the identity projection, recording the entire move.

Every Observation X refines Observation.top X.

def Interaction.Multiparty.Observation.bot (X : Type u) : Observation X

Observation.bot X = ⟨PUnit, fun _ => PUnit.unit⟩ is the bottom of the information lattice on X: the constant projection to a singleton, recording nothing about the move.

Observation.bot X refines every Observation X.

def Interaction.Multiparty.Observation.Refines {X : Type u} (k₁ k₂ : Observation X) : Prop

Observation.Refines k₁ k₂ (read "k₁ refines k₂") holds when k₁ is no more revealing than k₂: the projection of k₁ factors through that of k₂.

Equivalently, every k₂-indistinguishability class is a union of k₁-indistinguishability classes, so observers using k₁ learn at most what observers using k₂ learn. This is the natural ordering in which Observation.bot is least and Observation.top is greatest.

theorem Interaction.Multiparty.Observation.Refines.refl {X : Type u} (k : Observation X) : k.Refines k

theorem Interaction.Multiparty.Observation.Refines.trans {X : Type u} {k₁ k₂ k₃ : Observation X} (h₁₂ : k₁.Refines k₂) (h₂₃ : k₂.Refines k₃) : k₁.Refines k₃

theorem Interaction.Multiparty.Observation.bot_refines {X : Type u} (k : Observation X) : (Observation.bot X).Refines k

The bottom kernel refines every kernel: zero information is no more revealing than any kernel.

theorem Interaction.Multiparty.Observation.refines_top {X : Type u} (k : Observation X) : k.Refines (Observation.top X)

Every kernel refines the top kernel: any kernel is no more revealing than the identity projection.

def Interaction.Multiparty.Observation.combine {X : Type u} (k₁ k₂ : Observation X) : Observation X

Observation.combine k₁ k₂ is the join in the information lattice: the Σ-product of both kernels' observations.

It is the canonical way to combine two parties' views into a coalition view, and the universal kernel that records what is learned by jointly observing through k₁ and k₂. Since Refines orders by informativeness, combine k₁ k₂ carries strictly more information than either factor.

theorem Interaction.Multiparty.Observation.refines_combine_left {X : Type u} (k₁ k₂ : Observation X) : k₁.Refines (k₁.combine k₂)

theorem Interaction.Multiparty.Observation.refines_combine_right {X : Type u} (k₁ k₂ : Observation X) : k₂.Refines (k₁.combine k₂)

theorem Interaction.Multiparty.Observation.combine_refines_of {X : Type u} {k k₁ k₂ : Observation X} (h₁ : k₁.Refines k) (h₂ : k₂.Refines k) : (k₁.combine k₂).Refines k

combine is the least upper bound for Refines: any kernel k that is refined by both k₁ and k₂ is refined by combine k₁ k₂.

def Interaction.Multiparty.Observation.postcomp {X : Type u} (k : Observation X) {Y : Type u} (f : k.fst → Y) : Observation X

k.postcomp f post-composes the projection of k with f : k.1 → Y, yielding a kernel that is automatically refined by k.

This is the workhorse for "downgrading" an observation: if a corruption mode strips a field from the observation type, the new kernel is postcomp of the old one with the field-removal map.

theorem Interaction.Multiparty.Observation.postcomp_refines {X : Type u} (k : Observation X) {Y : Type u} (f : k.fst → Y) : (k.postcomp f).Refines k

def Interaction.Multiparty.Observation.Action {X : Type u} (k : Observation X) (m : Type u → Type u) (Cont : X → Type u) : Type u

Observation.Action k m Cont is the maximally general local node shape associated to a kernel k = ⟨Obs, toObs⟩.

It asks the participant to commit to an entire family of continuations indexed by the observation o : Obs: for each observed value o, an effectful map sending each move x : X whose observation is o to its continuation Cont x.

Operationally specialized shapes (the simpler Σ-of-X, function-from-X, and function-into-Cont patterns) live in Multiparty/Core.lean as ViewMode.Action; this is the universal shape that they all collapse to.

Mathlib lattice typeclass instances

The instances below expose the information-lattice algebra of Observation X through Mathlib's standard order classes. They are non-defining: each one is a thin wrapper over the named operations above (Observation.top, Observation.bot, Refines, combine).

A SemilatticeSup instance would require antisymmetry of Refines, which fails in general (mutually refining kernels related by codomain bijections), so we expose only Max for the ⊔ notation; the join-style lemmas live as named theorems above.

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instTop {X : Type u} : Top (Observation X)

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instBot {X : Type u} : Bot (Observation X)

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instLE {X : Type u} : LE (Observation X)

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instPreorder {X : Type u} : Preorder (Observation X)

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instOrderTop {X : Type u} : OrderTop (Observation X)

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instOrderBot {X : Type u} : OrderBot (Observation X)

@[implicit_reducible]

instance Interaction.Multiparty.Observation.instMax {X : Type u} : Max (Observation X)

@[simp]

theorem Interaction.Multiparty.Observation.top_def {X : Type u} : ⊤ = Observation.top X

@[simp]

theorem Interaction.Multiparty.Observation.bot_def {X : Type u} : ⊥ = Observation.bot X

@[simp]

theorem Interaction.Multiparty.Observation.le_def {X : Type u} {k₁ k₂ : Observation X} : k₁ ≤ k₂ ↔ k₁.Refines k₂

@[simp]

theorem Interaction.Multiparty.Observation.sup_def {X : Type u} (k₁ k₂ : Observation X) : k₁ ⊔ k₂ = k₁.combine k₂