We now introduce the last (g) of our abstract characterisations of local compactness in the Introduction. Recall from Section 2 that any continuous distributive lattice carries a binary relation (written ≪ and called “waybelow”) such that
⊥≪γ 
Notation 11.1
We define a new relation n≺≺ m as A_{n}β^{m}.
This is an open binary relation (term of type Σ with two free variables) on the overt discrete object N of indices of a basis, not on the lattice Σ^{X}. It is an “imposed” structure on N in the sense of Remark 4.5.
For most of the results of this section, we shall require (β^{n},A_{n}) to be an ∨basis for X.
Examples 11.2 (Not all of these are ∨bases.)
L≺≺ R ≡ A_{L} B^{R} ⇔ R⊂^{♯}L ≡ ∀ℓ∈ L.∃ℓ′∈ R.(ℓ′⊂ℓ), 
(ℓ≺≺_{Σ2 X}ℓ′) ⇔ (ℓ≺≺_{X}^{♯}ℓ′). 
Our first result just restates the assumption of an ∨basis, cf. Lemmas 1.9 and 2.6:
Lemma 11.3 0≺≺ p, whilst
n+m≺≺ p iff both n≺≺ p and m≺≺ p.
Proof A_{0}β^{p}⇔⊤ and A_{n+m}β^{p}⇔ A_{n}β^{p}∧ A_{m}β^{p}. ▫
In a continuous lattice, α≪β implies α≤β, but we have no similar property relating ≺≺ to ≼. We shall see the reasons for this in Section 13. But we do have two properties that carry most of the force of α≪β⇒α≤β. We call them roundedness. The second also incorporates many of the uses of directed joins and Scott continuity into a notation that will become increasingly more like discrete mathematics than it resembles the technology of traditional topology.
Lemma 11.4 β^{n}=∃ m.(m≺≺ n)∧β^{m} and
A_{m}=∃ n.A_{n}∧(m≺≺ n).
Proof The first is simply the basis expansion of β^{n}. For the second, we apply A_{m} to the basis expansion of φ, so
A_{m}φ ⇔ ∃ n.A_{n}φ∧ A_{m}β^{n} ⇔ (∃ n.A_{n}∧ A_{m}β^{n})φ, 
since A_{n} preserves directed joins (Theorem 9.6). ▫
Corollary 11.5
If m≺≺ n then β^{m}≤β^{n} and A_{m}≥ A_{n}. ▫
Corollary 11.6
If m≺≺ n, A_{m′}≥ A_{m} and β^{n}≤β^{n′},
then m′≺≺ n′.
Proof (m≺≺ n)≡ A_{m}β^{n}⇒ A_{m′}β^{n′}≡(m′≺≺ n′). ▫
Corollary 11.7 The relation ≺≺ satisfies
transitivity and the interpolation lemma:
(m≺≺ n) ⇔ (∃ k. m≺≺ k≺≺ n). 
Proof A_{m}β^{n} ⇔ (∃ k.A_{k}∧ m≺≺ k)β^{n} ⇔ ∃ k.A_{k}β^{n}∧ m≺≺ k. ▫
Now we consider the interaction between ≺≺ and the lattice structures (⊤,⊥,∧,∨) and (1,0,+,⋆). Of course, for this we need a lattice basis.
φ∧ψ = ∃ p q.β^{p⋆ q}∧ A_{p}φ∧ A_{q}ψ and φ∨ψ = ∃ p q.β^{p+q}∧ A_{p}φ∧ A_{q}ψ. 
Proof The first is the Frobenius law, since β^{p⋆ q}=β^{p}∧β^{q}.
The second uses Lemma 4.17: we obtain the expression
φ∨ψ = ∃ p.A_{p}φ∧(β^{p}∨ψ) 
from the basis expansion φ=∃ p.A_{p}φ∧β^{p} by adding ψ to the 0th term (since A_{0}φ⇔⊤ and β^{0}=⊥) and, harmlessly, A_{p}φ∧ψ to the other terms. Similarly,
β^{p}∨ψ = ∃ q.A_{q}ψ∧(β^{p}∨β^{q}) = ∃ q.A_{q}ψ∧β^{p+q}. 
The joins are directed because because A_{0}φ∧ A_{0}ψ⇔⊤ and
(A_{p1}φ ∧ A_{q1}ψ) ∧ (A_{p2}φ∧ A_{q2}ψ) ⇔ (A_{p1+p2}φ∧ A_{q1+q2}ψ). ▫ 
Lemma 11.9 For a lattice basis,
A_{n}⊤⇔(n≺≺1), A_{n}⊥⇔(n≺≺0) and

Proof The first two are A_{n}β^{1} and A_{n}β^{0}. The other two are ∃ p q.A_{n}(β^{p⋆ q})∧ A_{p}φ∧ A_{q}ψ and ∃ p q.A_{n}(β^{p+q})∧ A_{p}φ∧ A_{q}ψ, which are A_{n} applied to the directed joins in Lemma 11.8. ▫
Proposition 11.10
The lattice basis (β^{n},A_{n}) is a filter basis iff 1≺≺1 and
Proof (n≺≺1)⇔ A_{n}β^{1}⇔ A_{n}⊤, but recall that n≺≺1 for all n iff 1≺≺1.
The displayed rule is A_{m}β^{p}∧ A_{m}β^{q} ⇔ A_{m}β^{p⋆ q} ≡ A_{m}(β^{p}∧β^{q}). Given this, by the Frobenius law and Lemma 11.9,

If we don’t have a filter basis, we have to let n “slip” by n≺≺ m, cf. Lemma 2.8:
Lemma 11.11 For any lattice basis,
Proof Downwards, interpolate n≺≺ m≺≺ p⋆ q≼ p,q, then m≺≺ p,q by monotonicity. Conversely, using Corollary 11.5, if A_{n}β^{m}⇔⊤ and β^{m}≤β^{p⋆ q} then A_{n}β^{p⋆ q}⇔⊤. ▫
The corresponding result for ∨ is our version of the Wilker property, cf. Proposition 1.10 and Lemma 2.7.
Proof Lemma 11.9 with φ≡β^{p} and ψ≡β^{q}. ▫
We shall summarise these rules in Definition 14.1.
There are special results that we have in the cases of overt and compact objects. We already know that 1≺≺ 1 iff the object is compact (cf. Lemma 6.5), but the lattice dual characterisation of overtness cannot be 0≺≺ 0, as that always happens.
Lemma 11.13 If X is overt then
(n≺≺ m) ⇒ (n≺≺ 0) ∨ (∃ y.β^{m} y) but (n≺≺ 0)∧(∃ x.β^{n} x)⇔⊥. 
Proof φ x⇒ ∃ y.φ y so, using the Phoa principle (Axiom 3.6),
A_{n}φ ⇒ A_{n}(λ x.∃ y.φ y) ⇔ A_{n}⊥∨∃ y.φ y∧ A_{n}⊤ ⇒ (n≺≺ 0) ∨ ∃ y.φ y. 
Putting φ≡β^{m},
(n≺≺ m) ≡ A_{n}β^{m} ⇒ (n≺≺ 0)∨ ∃ y.β^{m} y, 
whilst (n≺≺ 0) ∧ ∃ x.β^{n} x ⇔ ∃ x.A_{n}β^{0}∧β^{n} x ⇒ ∃ x.∃ n.A_{n}⊥∧β^{n} x ⇔ ∃ x.⊥ x ⇔ ⊥. ▫
By a similar argument, we have Johnstone’s “Townsend–Thoresen Lemma” [Joh84],
(n≺≺ p+q) ⇒ (n≺≺ p) ∨ (∃ y.β^{q} y). 
Corollary 11.14 Given a compact overt object, it’s
decidable whether it’s empty or inhabited, cf. Corollary 5.8.
Proof As (1≺≺1)⇔⊤, the Lemma makes (1≺≺0) and ∃ x.β^{1} x≡∃ x.⊤ complementary. ▫
Compact overt subobjects are, in fact, particularly well behaved in discrete [E] and Hausdorff [J] objects.
Sections 13–16 are devoted to proving that the rules above for ≺≺ are complete, in the sense that from any abstract basis (N,0,1,+,⋆,≺≺) satisfying them we may recover an object of the category. This proof is very technical, so in the next section we consider a special case, in which the lattice structure plays a much lighter role.