class Lean.Order.PreservesSup {α : Type u} [CompleteLattice α] (f : α → α) : Prop

f : α → α preserves Sup if it distributes over arbitrary joins: f (sup s) = sup { f x | x ∈ s }. Equivalently f is a lower adjoint, so it has an upper adjoint PreservesSup.upperAdjoint f.

A frame operator acts by a Sup-preserving map for each resource r: the lattice meet (a ⊓ ·), or a cost combinator (costConj r) for a counter resource. The upper adjoint is the corresponding implication: Heyting ⇨ for the meet, a magic wand for separating conjunction.

• map_sup (s : α → Prop) : f (CompleteLattice.sup s) = CompleteLattice.sup fun (y : α) => ∃ (x : α), s x ∧ y = f x

  f preserves joins.

noncomputable def Lean.Order.PreservesSup.upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) (b : α) : α

The upper adjoint of f: the join of all x with f x ⊑ b. For f = (a ⊓ ·) this is Heyting implication a ⇨ ·.

Equations

• Lean.Order.PreservesSup.upperAdjoint f b = Lean.Order.CompleteLattice.sup fun (x : α) => Lean.Order.PartialOrder.rel (f x) b

theorem Lean.Order.PreservesSup.upperAdjoint_spec {α : Type u} [CompleteLattice α] (f : α → α) (b : α) : is_sup (fun (x : α) => PartialOrder.rel (f x) b) (upperAdjoint f b)

upperAdjoint f b is the least upper bound of {x | f x ⊑ b} by definition.

theorem Lean.Order.PreservesSup.le_upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) {b x : α} (h : PartialOrder.rel (f x) b) : PartialOrder.rel x (upperAdjoint f b)

Unit, free from the definition of upperAdjoint: f x ⊑ b → x ⊑ upperAdjoint f b. Needs only CompleteLattice.

theorem Lean.Order.PreservesSup.upperAdjoint_le {α : Type u} [CompleteLattice α] (f : α → α) [PreservesSup f] (b : α) : PartialOrder.rel (f (upperAdjoint f b)) b

Counit (modus ponens), from join preservation: f (upperAdjoint f b) ⊑ b.

theorem Lean.Order.PreservesSup.map_mono {α : Type u} [CompleteLattice α] (f : α → α) [PreservesSup f] {b b' : α} (h : PartialOrder.rel b b') : PartialOrder.rel (f b) (f b')

Monotonicity of a Sup-preserving f, derived from join preservation.

noncomputable def Lean.Order.PreservesSup.frameClosure {α : Type u} [CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α) (k : (β → α) → α) (Q : β → α) : α

The frame closure of a post-transformer k with respect to a family of Sup-preserving operators op r: the meet over all resources r of the r-upper-adjoint of k framed by r. It internalizes the frame rule into any k (see frameClosure_frames), with no assumption on k. A weakest precondition built as frameClosure op (fun Q => bwp x Q E) satisfies the op-frame rule by construction.

Equations

• Lean.Order.PreservesSup.frameClosure op k Q = Lean.Order.iInf fun (r : R) => Lean.Order.PreservesSup.upperAdjoint (op r) (k fun (a : β) => op r (Q a))

theorem Lean.Order.PreservesSup.frameClosure_frames {α : Type u} [CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α) [∀ (r : R), PreservesSup (op r)] (comp : R → R → R) (hact : ∀ (r r' : R) (a : α), op (comp r r') a = op r (op r' a)) (k : (β → α) → α) (Q : β → α) (F : R) : PartialOrder.rel (op F (frameClosure op k Q)) (frameClosure op k fun (a : β) => op F (Q a))

The frame rule, internalized: for a family of Sup-preserving operators op r whose resources compose by comp with the action law op (comp r r') = op r ∘ op r', and any post-transformer k, op F (frameClosure op k Q) ⊑ frameClosure op k (fun a => op F (Q a)).

theorem Lean.Order.PreservesSup.le_frameClosure_iff {α : Type u} [CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α) [∀ (r : R), PreservesSup (op r)] (k : (β → α) → α) {Q : β → α} {pre : α} : PartialOrder.rel pre (frameClosure op k Q) ↔ ∀ (r : R), PartialOrder.rel (op r pre) (k fun (a : β) => op r (Q a))

Landing below the frame closure, transposed across the Galois connection: pre ⊑ frameClosure op k Q holds exactly when op r pre ⊑ k (fun a => op r (Q a)) for every resource r. At a unit resource (op e = id) the r = e conjunct is pre ⊑ k Q; the remaining conjuncts are the frame conditions on pre, so a pre that cannot frame is forced down to the trivial ⊥.

theorem Lean.Order.PreservesSup.le_frameClosure {α : Type u} [CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α) [∀ (r : R), PreservesSup (op r)] (k : (β → α) → α) {Q : β → α} {pre : α} (hframe : ∀ (r : R) (Q' : β → α), PartialOrder.rel (op r (k Q')) (k fun (a : β) => op r (Q' a))) (hpre : PartialOrder.rel pre (k Q)) : PartialOrder.rel pre (frameClosure op k Q)

Landing below the frame closure reduces to landing below the base transformer together with framing: if pre ⊑ k Q and k frames every op r (op r (k Q') ⊑ k (fun a => op r (Q' a))), then pre ⊑ frameClosure op k Q.

theorem Lean.Order.PreservesSup.upperAdjoint_mono {α : Type u} [CompleteLattice α] (f : α → α) [PreservesSup f] {b b' : α} (h : PartialOrder.rel b b') : PartialOrder.rel (upperAdjoint f b) (upperAdjoint f b')

A right adjoint is monotone.

theorem Lean.Order.PreservesSup.frameClosure_le {α : Type u} [CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α) [∀ (r : R), PreservesSup (op r)] (e : R) (hunit : ∀ (a : α), op e a = a) (k : (β → α) → α) (Q : β → α) : PartialOrder.rel (frameClosure op k Q) (k Q)

The frame closure lies below the base transformer, witnessed at a unit resource e with op e = id.

theorem Lean.Order.le_apply_of_point_meet_le {σ : Type v} {β : Type w} [CompleteLattice β] (s : σ) (pre : β) (Q : σ → β) (h : PartialOrder.rel (fun (u : σ) => meet (CompleteLattice.ofProp (u = s)) pre) Q) : PartialOrder.rel pre (Q s)

Frame a single state coordinate: from the function-order premise (fun u => ⌜u = s⌝ ⊓ pre) ⊑ Q conclude the point entailment pre ⊑ Q s. Instantiating the premise at u := s collapses ⌜s = s⌝ ⊓ pre to pre. Iterating it over a state chain point-frames pre ⊑ Q s₁ … sₙ to the function-order goal (fun u⃗ => ⌜u⃗ = s⃗⌝ ⊓ pre) ⊑ Q.