Regular Propositions of a Compatibility Frame

[HM24]

The ◇-regular subsets of a compatibility frame F form an orthocomplemented lattice. Rather than re-derive it, this file identifies that lattice with the abstract concept lattice of the orthogonality relation ¬ compat: CompatFrame.Regular F := Orthoframe.Regular F.toOrthoframe (mathlib Order.Concept, via Core.Order.Orthoframe), so the OrthocomplementedLattice structure and Holliday–Mandelkern's Proposition 4.8 (compl_compl) come for free.

What this file contributes is the decidable construction interface: the IsRegular predicate (a bounded-quantifier Prop, hence decide-able on finite frames), its closure lemmas, the bridge isRegular_iff_isExtent, and the smart constructor CompatFrame.regOf building a Regular element from a regularity proof.

Main definitions

• CompatFrame.toOrthoframe, CompatFrame.Regular, CompatFrame.regOf.
• isRegular_iff_isExtent — IsRegular F is IsExtent of the orthogonality relation.

Closure-under-regularity helpers

theorem Orthologic.orthoNeg_isRegular {S : Type u_1} (F : CompatFrame S) (A : Set S) : IsRegular F (orthoNeg F A)

The orthocomplement of any set is regular (whether or not the original set is).

theorem Orthologic.inter_isRegular {S : Type u_1} {F : CompatFrame S} {A B : Set S} (hA : IsRegular F A) (hB : IsRegular F B) : IsRegular F (A ∩ B)

Regular sets are closed under intersection.

theorem Orthologic.disj_isRegular {S : Type u_1} (F : CompatFrame S) (A B : Set S) : IsRegular F (disj F A B)

The disjunction disj F A B = orthoNeg F (orthoNeg F A ∩ orthoNeg F B) is regular (immediate from orthoNeg_isRegular).

theorem Orthologic.empty_isRegular {S : Type u_1} (F : CompatFrame S) : IsRegular F ∅

The empty set is regular (vacuously: take y = x by reflexivity).

theorem Orthologic.univ_isRegular {S : Type u_1} (F : CompatFrame S) : IsRegular F Set.univ

The full set is regular (trivially).

theorem Orthologic.orthoNeg_orthoNeg_of_isRegular {S : Type u_1} (F : CompatFrame S) {A : Set S} (hA : IsRegular F A) : orthoNeg F (orthoNeg F A) = A

The load-bearing involutivity: orthoNeg² A = A for regular A. [HM24] Proposition 4.8.

Bridge to the abstract orthoframe construction

def Orthologic.CompatFrame.toOrthoframe {S : Type u_1} (F : CompatFrame S) : Orthoframe S

The orthogonality (incompatibility) orthoframe of a compatibility frame: x ⊥ y ↔ ¬ compat x y. Symmetry and irreflexivity come from symmetry and reflexivity of compat.

Equations

• F.toOrthoframe = { ortho := fun (x y : S) => ¬F.compat x y, ortho_symm := ⋯, ortho_irrefl := ⋯ }

theorem Orthologic.orthoNeg_eq_upperPolar {S : Type u_1} (F : CompatFrame S) (A : Set S) : orthoNeg F A = upperPolar F.toOrthoframe.ortho A

orthoNeg is the upperPolar of the orthogonality relation.

theorem Orthologic.isRegular_iff_orthoNeg_orthoNeg {S : Type u_1} (F : CompatFrame S) (A : Set S) : IsRegular F A ↔ orthoNeg F (orthoNeg F A) = A

IsRegular is the double-orthonegation fixed-point condition.

theorem Orthologic.isRegular_iff_isExtent {S : Type u_1} (F : CompatFrame S) (A : Set S) : IsRegular F A ↔ Order.IsExtent F.toOrthoframe.ortho A

The ◇-regular sets of F are exactly the concept extents of its orthogonality relation; Holliday–Mandelkern's Proposition 4.8 is mathlib's upperPolar_lowerPolar_upperPolar (see Core.Order.Orthoframe).

The ortholattice of regular propositions

@[reducible, inline]

abbrev Orthologic.CompatFrame.Regular {S : Type u_1} (F : CompatFrame S) : Type u_1

The regular propositions of F: the ortholattice Orthoframe.Regular of its orthogonality orthoframe (the concept extents of ¬ compat); Holliday–Mandelkern's Proposition 4.8 is mathlib's upperPolar_lowerPolar_upperPolar. The decidable IsRegular predicate is the construction interface — use regOf to build an element from a regularity proof (e.g. by decide on a finite frame).

Equations

• F.Regular = F.toOrthoframe.Regular

def Orthologic.CompatFrame.regOf {S : Type u_1} (F : CompatFrame S) (A : Set S) (h : IsRegular F A) : F.Regular

Build a regular proposition from a set and an IsRegular proof.

Equations

• F.regOf A h = Concept.ofIsExtent F.toOrthoframe.ortho A ⋯

@[simp]

theorem Orthologic.CompatFrame.coe_regOf {S : Type u_1} {F : CompatFrame S} (A : Set S) (h : IsRegular F A) : ↑(F.regOf A h) = A

@[simp]

theorem Orthologic.CompatFrame.mem_regOf {S : Type u_1} {F : CompatFrame S} (A : Set S) (h : IsRegular F A) (x : S) : x ∈ F.regOf A h ↔ x ∈ A

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_inf {S : Type u_1} {F : CompatFrame S} (A B : F.Regular) : ↑(A ⊓ B) = ↑A ∩ ↑B

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_top {S : Type u_1} {F : CompatFrame S} : ↑⊤ = Set.univ

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_bot {S : Type u_1} {F : CompatFrame S} : ↑⊥ = ∅

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_compl {S : Type u_1} {F : CompatFrame S} (A : F.Regular) : ↑Aᶜ = orthoNeg F ↑A