Relatedness levels — the 3-point view of the Trocq lattice

Trocq indexes each relation by a pair (m, n) of MapClass levels recording how much structure the relation carries in each direction; the full 6-point lattice (map0 ⊑ map1 ⊑ {map2a, map2b} ⊑ map3 ⊑ map4, with its order and meet) lives in Transfer.Hierarchy.ParamLevel. That lattice is the single source of truth for level arithmetic. This file supplies the coarse three-point view of it used by the crypto encodings (which are embeddings, never bijections):

map < embedding < equiv

• map — the encoding transfers an equality forward (a = a' → enc a = enc a'); the image point is map1 (a bare forward map).
• embedding — additionally reflects equality (injective), so equality transfers in both directions; the image point is map3 (the graph of the encoding, both inclusions).
• equiv — a bijection (the univalence/SIP level the crypto encodings never reach); the image point is the coherent top map4.

RelLevel.toMapClass embeds the view into the lattice and MapClass.view3 retracts it (view3_toMapClass). The order RelLevel.le and the composite level RelLevel.meet are defined as the images of the lattice order and lattice meet under this view; the original three-point tables are recovered as theorems (le_iff_toNat, meet_eq_min), so every consumer of the 3-point API keeps its statements while the arithmetic is computed in the lattice.

The central operation is meet: a composite transfer (an op-tree assembled from sub-transfers) supports only the weakest level of its parts, so the level of a composite is the meet (the lower) of the component levels — computed as the MapClass meet of the images (toMapClass_meet).

inductive Transfer.RelLevel : Type

The three relatedness levels — the univalence-free 3-point view of Trocq's MapClass lattice (see the module docstring; the embedding is RelLevel.toMapClass). Ordered map < embedding < equiv.

• map : RelLevel

  A representation map: transfers equality forward only.

• embedding : RelLevel

  An embedding (injective map): transfers equality both ways.

• equiv : RelLevel

  An equivalence (bijection): the univalence/SIP level.

@[instance_reducible]

instance Transfer.instDecidableEqRelLevel : DecidableEq RelLevel

Equations

• Transfer.instDecidableEqRelLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Transfer.instReprRelLevel : Repr RelLevel

Equations

• Transfer.instReprRelLevel = { reprPrec := Transfer.instReprRelLevel.repr }

def Transfer.instReprRelLevel.repr : RelLevel → Nat → Std.Format

Equations

• Transfer.instReprRelLevel.repr Transfer.RelLevel.map prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Transfer.RelLevel.map")).group prec✝
• Transfer.instReprRelLevel.repr Transfer.RelLevel.embedding prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Transfer.RelLevel.embedding")).group prec✝
• Transfer.instReprRelLevel.repr Transfer.RelLevel.equiv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Transfer.RelLevel.equiv")).group prec✝

def Transfer.RelLevel.toNat : RelLevel → Nat

Rank of a level, for the linear order (the 3-point compatibility form; the primary order is the MapClass lattice order via toMapClass).

Equations

• Transfer.RelLevel.map.toNat = 0
• Transfer.RelLevel.embedding.toNat = 1
• Transfer.RelLevel.equiv.toNat = 2

def Transfer.RelLevel.toMapClass : RelLevel → Param.MapClass

The reconciliation-table embedding of the 3-point view into the Trocq level lattice: a bare representation map carries a forward map (map1); an embedding's graph relation carries both inclusions (map3); the equivalence point is the coherent top (map4).

Equations

• Transfer.RelLevel.map.toMapClass = Transfer.Param.MapClass.map1
• Transfer.RelLevel.embedding.toMapClass = Transfer.Param.MapClass.map3
• Transfer.RelLevel.equiv.toMapClass = Transfer.Param.MapClass.map4

def Transfer.Param.MapClass.view3 : MapClass → RelLevel

The coarsening retraction: every MapClass seen as a 3-point RelLevel (map0/map1 are map-strength, map2a/map2b/map3 are embedding-strength, map4 is the equivalence level).

Equations

• Transfer.Param.MapClass.map0.view3 = Transfer.RelLevel.map
• Transfer.Param.MapClass.map1.view3 = Transfer.RelLevel.map
• Transfer.Param.MapClass.map2a.view3 = Transfer.RelLevel.embedding
• Transfer.Param.MapClass.map2b.view3 = Transfer.RelLevel.embedding
• Transfer.Param.MapClass.map3.view3 = Transfer.RelLevel.embedding
• Transfer.Param.MapClass.map4.view3 = Transfer.RelLevel.equiv

@[simp]

theorem Transfer.RelLevel.view3_toMapClass (l : RelLevel) : l.toMapClass.view3 = l

RelLevel is a 3-point view: view3 retracts toMapClass.

def Transfer.RelLevel.le (l₁ l₂ : RelLevel) : Prop

The order on levels: l₁ ≤ l₂ iff l₁ is no stronger than l₂ — defined as the MapClass lattice order on the images.

Equations

• l₁.le l₂ = (l₁.toMapClass.le l₂.toMapClass = true)

@[instance_reducible]

instance Transfer.RelLevel.instLE : LE RelLevel

Equations

• Transfer.RelLevel.instLE = { le := Transfer.RelLevel.le }

theorem Transfer.RelLevel.le_iff_toNat (l₁ l₂ : RelLevel) : l₁.le l₂ ↔ l₁.toNat ≤ l₂.toNat

Old = new: the lattice-order definition of le agrees with the original 3-point rank order.

theorem Transfer.RelLevel.toMapClass_mono {l₁ l₂ : RelLevel} (h : l₁ ≤ l₂) : l₁.toMapClass.le l₂.toMapClass = true

The view embedding is monotone — definitionally, since le is the lattice order on the images.

def Transfer.RelLevel.meet (l₁ l₂ : RelLevel) : RelLevel

The meet (weaker) of two levels — the level a composite supports, given that it is only as strong as its weakest part. Defined as the view of the MapClass lattice meet of the images.

Equations

• l₁.meet l₂ = (l₁.toMapClass.meet l₂.toMapClass).view3

theorem Transfer.RelLevel.meet_eq_min (l₁ l₂ : RelLevel) : l₁.meet l₂ = if l₁.toNat ≤ l₂.toNat then l₁ else l₂

Old = new: the lattice-computed meet agrees with the original 3-point table (the minimum in the rank order).

theorem Transfer.RelLevel.toMapClass_meet (l₁ l₂ : RelLevel) : (l₁.meet l₂).toMapClass = l₁.toMapClass.meet l₂.toMapClass

The view embedding is a meet-homomorphism: the 3-point meet computes the lattice meet on the image (the image {map1, map3, map4} is meet-closed, and view3 retracts it).

@[simp]

theorem Transfer.RelLevel.meet_comm (l₁ l₂ : RelLevel) : l₁.meet l₂ = l₂.meet l₁

@[simp]

theorem Transfer.RelLevel.meet_self (l : RelLevel) : l.meet l = l

theorem Transfer.RelLevel.meet_le_left (l₁ l₂ : RelLevel) : l₁.meet l₂ ≤ l₁

theorem Transfer.RelLevel.meet_le_right (l₁ l₂ : RelLevel) : l₁.meet l₂ ≤ l₂

@[simp]

theorem Transfer.RelLevel.meet_map_left (l : RelLevel) : map.meet l = map

@[simp]

theorem Transfer.RelLevel.meet_map_right (l : RelLevel) : l.meet map = map