Level-annotated relatedness

This refines the Related kernel (Bridges/Transfer/Related) with the relatedness levels of Bridges/Transfer/Levels. A RelatedAt lvl enc a b carries the same underlying equation enc a = b and additionally records the strongest encoding strength (RelLevel) available along this transfer.

The level is metadata rather than a proof obligation: the equation is identical at every level. The level provides reflection at the embedding level — transferIffAt turns a one-way encoding equality into the two-way ↔ of ReprEmbeddingClass.eq_iff, which the bare map level cannot supply.

Composition follows Levels.meet: an op-tree assembled from sub-transfers is only as strong as its weakest part, so composeBinOpAt sits at the meet of the component levels — and since RelLevel.meet is the view of the MapClass lattice meet, the composite's level index is computed in the Trocq lattice (composeBinOpAt_level_toMapClass).

The Param-hierarchy foundation

The primary, lattice-indexed semantics of a level-annotated transfer is membership in the graph Param at the image level: RelLevel.graphParam lvl enc : Param lvl.toMapClass .map0 packages the graph of enc with the exact MapHas structure the image level carries (map1 a bare map, map3 both inclusions, map4 + the proof-irrelevance coherence), and relatedAt_iff_graphParam identifies RelatedAt lvl enc a b with (graphParam lvl enc).R a b. At the class-registered points the graph Param is the committed hierarchy witness (graphParam_map_eq_paramOfMap, graphParam_embedding_eq_paramOfEmbedding), and the embedding-level reflection transferIffAt is derived from its Param-side form (transferIffParam). The RelatedAt class is kept as the resolution-facing wrapper over this semantics.

Bridges to the unlevelled kernel

• RelatedAt.toRelated — forget the level (always sound: same equation).
• Related.toRelatedAtMap — every transfer is at least map-level.

class Transfer.RelatedAt (lvl : RelLevel) {A α : Type u} (enc : A → α) (a : A) (b : α) : Prop

RelatedAt lvl enc a b: like Related enc a b (the value b is the encoding enc a of a), but indexed by the relatedness lvl recording the strongest encoding strength available along this transfer. The underlying equation is the same at every level.

• rel : enc a = b

  b is exactly the encoding of a.

class Transfer.RelatedBinOpAt (lvl : RelLevel) {A α : Type u} (enc : A → α) (op : A → A → A) (bop : α → α → α) : Prop

A level-annotated registered realization of a binary operation: the commuting square enc (op x y) = bop (enc x) (enc y), tagged with the level lvl at which the operation's encoding is realized.

• comm (x y : A) : enc (op x y) = bop (enc x) (enc y)

  The commuting square for this operation.

instance Transfer.composeBinOpAt {lop la lb : RelLevel} {A α : Type u} (enc : A → α) (op : A → A → A) (bop : α → α → α) (a b : A) (a' b' : α) [hop : RelatedBinOpAt lop enc op bop] [ha : RelatedAt la enc a a'] [hb : RelatedAt lb enc b b'] : RelatedAt (lop.meet (la.meet lb)) enc (op a b) (bop a' b')

Composition. A composite transfer is only as strong as its weakest part. A realized operation at level lop and operands at levels la, lb give the composite at meet lop (meet la lb). The equation proof mirrors composeBinOp.

@[instance 100]

instance Transfer.leafAt {lvl : RelLevel} {A α : Type u} (enc : A → α) (a : A) : RelatedAt lvl enc a (enc a)

Leaf (generic encoding) at an explicit level. The encoding of a value is related to it. Low priority so composeBinOpAt is preferred and resolution terminates at leaves. The level must be pinned by the goal.

@[instance 100]

instance Transfer.leafIdAt {lvl : RelLevel} {α : Type u} (a : α) : RelatedAt lvl id a a

Leaf for the identity encoding at an explicit level. Gives the head RelatedAt lvl id a a directly (resolution will not reduce id a to a).

theorem Transfer.RelatedAt.toRelated {lvl : RelLevel} {A α : Type u} {enc : A → α} {a : A} {b : α} (h : RelatedAt lvl enc a b) : Related enc a b

Forget the level. A level-annotated transfer is always a plain transfer: same equation.

theorem Transfer.Related.toRelatedAtMap {A α : Type u} {enc : A → α} {a : A} {b : α} (h : Related enc a b) : RelatedAt RelLevel.map enc a b

Every transfer is at least map-level. A plain transfer lifts to a map-annotated one (the weakest level).

theorem Transfer.transferRelAt {lvl : RelLevel} {A α : Type u} {enc : A → α} {a : A} {b : α} (h : RelatedAt lvl enc a b) : enc a = b

Transfer corollary. Extracts the underlying equation from a level-annotated transfer.

def Transfer.levelOf {lvl : RelLevel} {A α : Type u} {enc : A → α} {a : A} {b : α} : RelatedAt lvl enc a b → RelLevel

The level a transfer used, reportable as data.

Equations

• Transfer.levelOf x✝ = lvl

The Param-hierarchy foundation: graph Param at the image level

def Transfer.RelLevel.graphMapHas {A α : Type u} (enc : A → α) (lvl : RelLevel) : Param.MapHas lvl.toMapClass fun (a : A) (b : α) => enc a = b

The forward MapHas structure of the graph of enc at the image level lvl.toMapClass: a bare map at map1, both graph inclusions (identities) at map3, and the map4 coherence free by proof irrelevance on the Prop-valued graph.

Equations

• Transfer.RelLevel.graphMapHas enc Transfer.RelLevel.map = { map := enc }
• Transfer.RelLevel.graphMapHas enc Transfer.RelLevel.embedding = { map := enc, map_in_R := ⋯, R_in_map := ⋯ }
• Transfer.RelLevel.graphMapHas enc Transfer.RelLevel.equiv = { map := enc, map_in_R := ⋯, R_in_map := ⋯, R_in_mapK := ⋯ }

def Transfer.RelLevel.graphParam {A α : Type u} (lvl : RelLevel) (enc : A → α) : Param.Param lvl.toMapClass Param.MapClass.map0 A α

The graph of enc as an annotated relation at the image level: the primary, lattice-indexed semantics of a level-annotated transfer. Backward map0 — no decoder is packaged (an annotation records forward strength only; the backward directions live in the Param hierarchy's committed witnesses).

Equations

• lvl.graphParam enc = { R := fun (a : A) (b : α) => enc a = b, fwd := Transfer.RelLevel.graphMapHas enc lvl, bwd := { } }

theorem Transfer.relatedAt_iff_graphParam {lvl : RelLevel} {A α : Type u} {enc : A → α} {a : A} {b : α} : RelatedAt lvl enc a b ↔ (lvl.graphParam enc).R a b

Old = new: RelatedAt lvl enc a b is exactly membership in the graph Param's relation at the image level. The class is the resolution-facing wrapper over this Param-hierarchy semantics.

theorem Transfer.graphParam_map_eq_paramOfMap {A α : Type u} [ReprMapClass A α] : RelLevel.map.graphParam ReprMapClass.enc = Param.paramOfMap

At the map point the graph Param of a class-registered map is the committed hierarchy witness paramOfMap.

theorem Transfer.graphParam_embedding_eq_paramOfEmbedding {A α : Type u} [ReprEmbeddingClass A α] : RelLevel.embedding.graphParam ReprMapClass.enc = Param.paramOfEmbedding

At the embedding point the graph Param of a class-registered embedding is the committed hierarchy witness paramOfEmbedding.

theorem Transfer.composeBinOpAt_level_toMapClass (lop la lb : RelLevel) : (lop.meet (la.meet lb)).toMapClass = lop.toMapClass.meet (la.toMapClass.meet lb.toMapClass)

The composite level index of composeBinOpAt is computed in the MapClass lattice: its toMapClass is the lattice meet of the images (immediate from the lattice definition of RelLevel.meet).

Reflection at the embedding level

theorem Transfer.transferIffParam {A α : Type u} [ReprEmbeddingClass A α] {a a' : A} {b : α} (h : Param.paramOfEmbedding.R a b) : b = ReprMapClass.enc a' ↔ a = a'

Reflection stated on the Param side (the primary form): membership in the class-registered embedding's Param relation reflects equality — the one-way graph equation becomes the two-way ↔ via ReprEmbeddingClass.eq_iff.

theorem Transfer.transferIffAt {A α : Type u} [ReprEmbeddingClass A α] {a a' : A} {b : α} (h : RelatedAt RelLevel.embedding ReprMapClass.enc a b) : b = ReprMapClass.enc a' ↔ a = a'

Embedding-level reflection. At embedding level the encoding reflects equality, so the one-way transfer equation enc a = b becomes the two-way b = enc a' ↔ a = a'. This is what embedding provides over map: map transfers equality forward, while embedding (ReprEmbeddingClass.eq_iff) transfers it both ways. Derived from the Param-side primary form transferIffParam.

Demonstrations at explicit levels

A tiny self-contained registered operation over Nat keeps the file light while exercising leaf resolution, single-op composition, and the meet of a composite.

instance Transfer.LevelsDemo.natAddRelated : RelatedBinOpAt RelLevel.equiv id (fun (x1 x2 : ℕ) => x1 + x2) fun (x1 x2 : ℕ) => x1 + x2

A trivially-realized + on Nat under the identity encoding, registered at equiv level (Nat ↔ Nat is a bijection).