diff --git a/content/index.md b/content/index.md
index 5e7a122..081b944 100644
--- a/content/index.md
+++ b/content/index.md
@@ -44,7 +44,7 @@ Work-in-progress proposals, organized by contributor.
 
 - [[personal/egparedes/layered-architecture|A layered architecture for gt4py with enforced public/internal decoupling]] — keywords: architecture, layering, tach, modularity, public-api, semi-public, internal, packaging, dependencies, refactoring, infrastructure, over-engineering, otf, workflow, dsl, config, allocators, caching, fingerprint, compiled-program, process-pool, factory-boy, instrumentation, adr, jax, decoupling, migration, tech-debt
 - [[personal/egparedes/otf-toolchain-split|Dissolving gt4py.next.otf into a toolchain core and DSL-agnostic build infrastructure]] — keywords: otf, toolchain, workflow, pipeline, refactoring, architecture, layering, modularity, backend, bindings, build-system, caching, runners, compiled-program, factory-boy, naming, observability, stage-inspection, adr, tach, tech-debt
-- [[personal/egparedes/connectivities-as-types/connectivities-as-types|Connectivities as types: one declaration for offset, local dimension and provider key]] — keywords: type-system, type-checking, dimensions, local-dimensions, connectivities, offset-provider, unstructured, neighbor-sum, reduction, frontend, foast, gtir, embedded, gtfn, dace, nominal-types, metaclass, serialization, fingerprint, staggering, migration, adr, tech-debt
+- [[personal/egparedes/connectivities-as-types/connectivities-as-types|Connectivities as types: one declaration for offset, local dimension and provider key]] — keywords: type-system, type-checking, dimensions, local-dimensions, connectivities, offset-provider, unstructured, neighbor-sum, reduction, frontend, foast, gtir, embedded, gtfn, dace, nominal-types, dependent-types, metaclass, serialization, fingerprint, staggering, migration, adr, tech-debt, shared-local-dimensions, implemented
 - [[personal/egparedes/discretization-independent-fd-syntax|A discretization-independent surface syntax for finite-difference computations]] — keywords: finite-difference, finite-volume, mesh-invariant, structured, unstructured, exterior-calculus, dec, mimetic, de-rham, location-typing, stencil, weight-generation, rbf-fd, gfdm, moment-matching, conservation, field-operators, icon, pace, pmap, fv3, ifs-fvm, arakawa-staggering, c-grid, d-grid, a-grid, dynamical-core, hevi, vertical-solve, elliptic-solve, mpdata, semi-implicit, miura, atlas, prior-art, dsl-design
 
 <!-- Entry format (index only the main proposal; link appendices/implementations
diff --git a/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md b/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
index 8be895d..3d8ae53 100644
--- a/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
@@ -1,8 +1,9 @@
 ---
 title: "Connectivities as types: one declaration for offset, local dimension and provider key"
 author: egparedes
-tags: [type-system, type-checking, dimensions, local-dimensions, connectivities, offset-provider, unstructured, neighbor-sum, reduction, frontend, foast, gtir, embedded, gtfn, dace, nominal-types, metaclass, serialization, fingerprint, staggering, migration, adr, tech-debt]
+tags: [type-system, type-checking, dimensions, local-dimensions, connectivities, offset-provider, unstructured, neighbor-sum, reduction, frontend, foast, gtir, embedded, gtfn, dace, nominal-types, dependent-types, metaclass, serialization, fingerprint, staggering, migration, adr, tech-debt, shared-local-dimensions, implemented]
 created: 2026-09-17
+updated: 2026-09-23
 status: draft
 ---
 
@@ -13,7 +14,8 @@ status: draft
 > Make the connectivity a **class** that *contains* its local dimension, is its
 > own provider key, and whose identity — like every dimension after
 > [[shared/dimensions-as-types|dimensions as types]] — is its qualified Python
-> name, which is also its IR tag:
+> name. In the IR it is named by its local dimension's tag, so shifts,
+> reductions and sparse arguments all find the table under one string:
 >
 > ```python
 > class V2E(NeighborConnectivity[V, E]):
@@ -23,20 +25,36 @@ status: draft
 > program(a, out=out, offset_provider={V2E: v2e_table})
 > ```
 >
-> `FieldOffset`, `ts.OffsetType`, the string-keyed `OffsetProvider` and the
+> `FieldOffset`, bare-name provider keys (`{"V2E": ...}`) and the
 > `V2EDim`-next-to-`V2E` naming convention disappear. Of the ten cross-object
 > identity constraints in the current tree, five (A1–A5) dissolve by
 > construction and three (A6–A8) collapse into a single bind-time check.
 
-> **Status**: draft, AI-assisted. Derived from a full audit of the gt4py tree
-> at `b3c53fa7e` (v1.2.2, 2026-09-03); every `file:line` reference was
-> re-derived from that tree, and the two behaviours the proposal leans on
-> hardest were confirmed by *running* them, not by reading. The complete
-> constraint catalogue and concept inventory are in the appendix
+> **Implementation status (2026-09-23).** Implemented as the stacked
+> GridTools/gt4py PRs listed in [Implementation](#implementation), with
+> ADR 0028 (dimensions as nominal types) and ADR 0029 (connectivities as
+> types). PR 1 is ready for review; PRs 2–8 are drafts. The sections below
+> describe the design **as implemented** on the top branch
+> (`connectivities-as-types-8-typed-positions`), including the review-fix
+> commits on PRs 2–8 that followed a check of this note against the code at
+> `65fa529b6` (2026-09-23); where the implementation had to depart from the
+> original proposal, the text was corrected and the departure is listed in
+> [Where the implementation departs](#where-the-implementation-departs-from-the-original-proposal).
+
+> **Status**: draft, AI-assisted. The *Problem* section and the appendix are
+> derived from a full audit of the gt4py tree at `b3c53fa7e` (v1.2.2,
+> 2026-09-03), i.e. *before* the implementation; their `file:line` references
+> point to that tree, and the two behaviours the proposal leans on hardest were
+> confirmed by *running* them, not by reading. The complete constraint
+> catalogue and concept inventory are in the appendix
 > [[personal/egparedes/connectivities-as-types/connectivities-as-types_research|Tag and name constraints — full catalogue]].
+> For the type-theoretic background — why the local dimension is owned by the
+> connectivity, and what a Python type can and cannot say about a neighbor
+> table — see
+> [[personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing|Background: dependent typing for mesh connectivities]].
 
 > **Relation to existing proposals.** This is the *single-hop base* that
-> [[personal/havogt/dependent-local-dimensions|Dependent local dimensions and
+> [[personal/havogt/dependent-local-dimensions/dependent-local-dimensions|Dependent local dimensions and
 > connectivity chains]] §6 calls "the shared core" and §9 stages as U0/U1: one
 > typed connectivity declaration, derived local dimension, derived offset tag.
 > It takes no position on chains, reduction order or the path-vs-forest
@@ -44,11 +62,11 @@ status: draft
 > (`min_neighbors` instead of `has_skip_values`; a nested `V2E.Local` instead
 > of a generic `Local[C]`) — see [Open questions / conflicts](#open-questions--conflicts).
 > The remap typing it needs is the `Connectivity[NewD, D0]` rule of
-> [[personal/havogt/dimension-generic-fields|Generic dimensions and statically
+> [[personal/havogt/dimension-generic-fields/dimension-generic-fields|Generic dimensions and statically
 > typed staggering]]. It builds on [[shared/dimensions-as-types|Dimensions as
 > types]] and its implementation in GridTools/gt4py#2844, and **conflicts with
 > one of that proposal's decisions** (identity semantics). It also overlaps
-> with [[personal/havogt/mesh-and-first-class-halos|A mesh concept with
+> with [[personal/havogt/mesh-and-first-class-halos/mesh-and-first-class-halos|A mesh concept with
 > first-class halos]], which proposes replacing the same `offset_provider`
 > dict with a Mesh object; this note re-types the dict and should be read as
 > the typed substrate that proposal can bind through.
@@ -139,109 +157,124 @@ what is one idea — *a mapping between two index spaces, plus a name for it*.
 
 ## Proposal
 
-### Five concepts
+### Four concepts
 
 | Concept | Role | Replaces |
 | --- | --- | --- |
-| `DimensionBaseIndex` | root of all dimension types; `value` is the index position | the `DimensionBase` root [[shared/dimensions-as-types|dimensions as types]] deferred |
-| `DimensionIndex` | user-declarable primary dimension (as in #2844) | `Dimension` instances |
-| `LocalDimensionIndex` | a local dimension: either **owned**, declared nested in its connectivity, or **owner-less** with a fixed `size`; carries `max_neighbors` / `min_neighbors` when they are known statically | `Dimension(..., kind=LOCAL)`, `_CONST_DIM`, and `NeighborConnectivityType.max_neighbors` / `skip_value` |
-| `NeighborConnectivity[Origin, Codomain]` | the connectivity **class**: type, shift handle and provider key in one object; contains its `Local` | `FieldOffset`, `runtime.Offset`, `ts.OffsetType`, the `V2EDim` convention |
-| `MultiDimensionIndex[D, *Ls]` | position in the product of a primary and one or more local dimensions | untyped position dicts keyed by name strings |
-
-`Connectivity` (the runtime protocol), `CartesianConnectivity`,
-`NeighborTable` / `NdArrayConnectivityField` (the data) and
-`NeighborConnectivityType` (the compile-time record) all **stay**. What
-changes is that the compile-time record is *produced by* the class instead
-of being authored in parallel with it.
-
-### Sketch
+| `DimensionIndex` | a dimension is a subclass, an index along it an instance (ADR 0028) | `Dimension` instances |
+| `LocalDimensionIndex(DimensionIndex)` | a local dimension: **owned** (declared nested in, or adopted by, its connectivity), or **owner-less** (optionally with `size=n`, which sets `max_neighbors = min_neighbors = n`); carries the neighbor counts | `Dimension(..., kind=LOCAL)`, `_CONST_DIM` (now `ConstList`) |
+| `NeighborConnectivity[Origin, Codomain]` | the connectivity **declaration**: shift handle in DSL code and provider key; contains its `Local`; never instantiated, and **not** a `Connectivity` | `FieldOffset`, the `V2EDim` convention |
+| `MultiDimensionIndex[D, *Ls]` | a position in the product of a primary and local dimensions, a tuple of indices; user-facing, nothing in the toolchain requires it | — (new; the iterator-embedded position dicts separately switched from name strings to dimension-class keys) |
+
+The originally proposed `DimensionBaseIndex` root was dropped: `Dimension` is
+`type[DimensionIndex]` and eve validates `type[X]` by `issubclass`, so a sibling
+root would have forced every `type[DimensionIndex]` annotation in the tree to
+widen and then admit local dimensions everywhere anyway. The tree already tells
+local dimensions apart by a runtime `kind` check, and keeps doing so.
+
+`Connectivity` (the runtime data protocol), `CartesianConnectivity`,
+`NeighborTable` / `NdArrayConnectivityField` (the data),
+`NeighborConnectivityType` (the compile-time record) and `ts.OffsetType` (the
+DSL type of a declaration) all **stay**. What changes is that they are
+*produced by* or *checked against* the class instead of being authored in
+parallel with it.
+
+### Sketch (as implemented)
 
 ```python
-# ── dimensions ─────────────────────────────────────────────────────────────
+# ── dimensions (ADR 0028) ─────────────────────────────────────────────────
 class DimensionMeta(type):
     @property
     def tag(cls) -> Tag:                       # identity, and the IR spelling
         return f"{cls.__module__}.{cls.__qualname__}"
     kind: DimensionKind
-    # __eq__/__hash__: default type identity. No registry, no copyreg.
-
-
-class DimensionBaseIndex[T](metaclass=DimensionMeta):
-    value: T
+    __hash__ = type.__hash__                   # __eq__ stays for `I == 5` -> Domain
 
 
-class DimensionIndex(DimensionBaseIndex[int]): ...                  # user-declarable
+class DimensionIndex(metaclass=DimensionMeta):
+    value: int                                 # an index along the dimension
 
+type Dimension = type[DimensionIndex]          # PEP 695: `Dimension("I")` is not callable
 
-class LocalDimensionIndex(DimensionBaseIndex[int]):
-    kind = DimensionKind.LOCAL
-    owner: ClassVar[type[NeighborConnectivity] | None]   # None: owner-less, fixed extent
-    max_neighbors: ClassVar[int | None]    # None: completed at bind time
-    min_neighbors: ClassVar[int | None]    # min == max  <=>  no skip values
 
-    def __init_subclass__(cls, *, size: int | None = None): ...   # owner-less form
+class LocalDimensionIndex(DimensionIndex):     # kind is LOCAL; `kind=LOCAL` elsewhere is an error
+    owner: ClassVar[type[NeighborConnectivity] | None]   # None: owner-less; set by the owner
+    max_neighbors: ClassVar[int | None]        # the counts live here, not on the connectivity
+    min_neighbors: ClassVar[int | None]        # min == max  <=>  no skip values
+    def __init_subclass__(cls, *, size: int | None = None): ...   # size: max = min = size
 
 
-class MultiDimensionIndex[D: DimensionIndex, *Ls](DimensionBaseIndex[tuple[D, *Ls]]):
-    """Position in the product of a primary dimension and its local dimensions."""
-    value: tuple[D, *Ls]                   # *Ls checked at runtime to be LocalDimensionIndex
+class MultiDimensionIndex[D: DimensionIndex, *Ls](tuple[D, *Ls]): ...   # shape checked at runtime
 
+Staggered[KDim]                                # an interned, real dimension class (ADR 0026)
 
-class Staggered[D: DimensionIndex](DimensionBaseIndex[int]): ...    # replaces the _Staggered prefix
 
-
-# ── connectivities ─────────────────────────────────────────────────────────
-class Connectivity[Src, Dst]: ...   # Protocol; parametrization changes, see Open Q6
-
-class CartesianConnectivity[D: DimensionIndex](Connectivity[D, D]): ...   # semantics unchanged
+# ── connectivities (ADR 0029) ─────────────────────────────────────────────
+class ConnectivityMeta(type):
+    tag: Tag                                   # the declaration's qualified name
+    offset_tag: Tag                            # how the IR names it, see "Identity"
+    origin: Dimension; codomain: Dimension     # read from the base subscription
+    def __call__(cls, *a, **kw) -> NoReturn: ...        # no instances
+    def __getitem__(cls, item): ...            # V2E[1] = bound_table()[Local(1)] in embedded;
+                                               # NC[V, E] forwarded to __class_getitem__
+    def __gt_type__(cls) -> ts.OffsetType: ...  # Codomain -> (Origin, Local), tag=offset_tag
+    def bound_table(cls) -> NeighborTable: ... # the table bound in the current embedded run
 
 
 class NeighborConnectivity[Origin: DimensionIndex, Codomain: DimensionIndex](
-    Connectivity[MultiDimensionIndex[Origin, LocalDimensionIndex], Codomain],
-    metaclass=ConnectivityMeta,
+    metaclass=ConnectivityMeta
 ):
-    Local: type[LocalDimensionIndex]   # MUST be declared nested by every subclass (see below)
+    Local: ClassVar[type[LocalDimensionIndex]]   # annotation only; every subclass declares it
+    def __init_subclass__(cls, *, max_neighbors=None, min_neighbors=None): ...
+    # writes Local.owner and the counts onto Local; subclassing a declaration is an error
+
 
-    def __init_subclass__(
-        cls, *, max_neighbors: int | None = None, min_neighbors: int | None = None
-    ): ...   # verifies `cls.Local` exists and is a LocalDimensionIndex; sets Local.owner = cls
-    # ConnectivityMeta provides: tag (qualified name), __gt_type__() -> NeighborConnectivityType
-    # (complete only once the counts are known), __getitem__ so that V2E[1] is a
-    # single-neighbor Connectivity, default type identity.
+def check_neighbor_table(connectivity, table_or_type) -> None: ...   # A6–A8 as one check
 
 
 # ── user code ──────────────────────────────────────────────────────────────
 class V(DimensionIndex): ...
 class E(DimensionIndex): ...
+class C(DimensionIndex): ...
+class CE(DimensionIndex): ...                  # flattened (cell, edge-of-cell) pairs
 
 
 class V2E(NeighborConnectivity[V, E], max_neighbors=6, min_neighbors=5):   # counts optional
     class Local(LocalDimensionIndex): ...                            # explicit, always
 
 
+class C2E(NeighborConnectivity[C, E]):
+    class Local(LocalDimensionIndex): ...
+
+
+class C2CE(NeighborConnectivity[C, CE]):       # a flattened sparse pattern:
+    Local: typing.TypeAlias = C2E.Local        # shares C2E's neighbor axis
+
+
 class LsqUnk(LocalDimensionIndex, size=3): ...                       # owner-less local axis
-class ConstList(LocalDimensionIndex, size=1): ...                    # replaces _CONST_DIM
 
 
 @field_operator
 def op(a: Field[Dims[E], float]) -> Field[Dims[V], float]:
-    return neighbor_sum(a(V2E), axis=V2E.Local)                      # local axis stays explicit
+    return neighbor_sum(a(V2E), axis=V2E.Local) + a(V2E[0])
 
 
 program(a, out=out, offset_provider={V2E: v2e_table})
+a(as_offset(KDim, k_offsets))                 # was as_offset(Koff, ...)
 ```
 
 Vocabulary: `Origin` is the dimension the remapped field lives on
 (`conn.domain[0]`), `Codomain` is what the table entries point into
 (`conn.codomain`) — the terms of ADR 0019 and of
-[[personal/havogt/dependent-local-dimensions|dependent local dimensions]] §3,
+[[personal/havogt/dependent-local-dimensions/dependent-local-dimensions|dependent local dimensions]] §3,
 chosen precisely because `FieldOffset.source`/`target` obscure direction.
 
 ### Identity is the qualified Python name
 
 A dimension's or connectivity's identity is the Python type; its tag is
-`f"{cls.__module__}.{cls.__qualname__}"`. The static view (checkers see
+`f"{cls.__module__}.{cls.__qualname__}"` (except `Staggered[D]`, whose tag
+embeds its base's full tag, rule 1; a connectivity is *named in the IR* by its
+`offset_tag`, rule 7). The static view (checkers see
 nominal types) and the runtime view (equality is `is`) agree by
 construction, and the tag is a valid, unique IR string. This is a deliberate
 departure from [[shared/dimensions-as-types|dimensions as types]] and #2844,
@@ -251,109 +284,139 @@ The position taken here: *existing tests that redeclare dummy dimensions can
 be fixed in other ways; they should not constrain the design of the
 concepts.* The consequences, stated as rules:
 
-1. **Reconstruction from the IR is an import.** `dimension(tag, kind)` is
-   replaced by `resolve(tag)`: `importlib.import_module(module)` then walk
-   the `qualname` (nested classes like `V2E.Local` resolve naturally). The
-   IR references a Python type exactly the way `pickle` references a class.
-   `AxisLiteral.kind` becomes redundant, which the `TODO` at
-   `iterator/ir.py:93` has wanted since the beginning. Parametrized types
-   (`Staggered[D]`, rule 6) have no importable `qualname`; their tag needs a
-   small grammar (`<qualname>[<tag>]`) and `resolve` must parse it and
-   materialize the class — the one place where "resolution is an import"
-   is not literally true.
-2. **Types reaching the IR must be importable.** An early heuristic at class
-   creation catches the common mistake:
-
-   ```python
-   def __init_subclass__(cls, **kw):
-       if "<locals>" in cls.__qualname__:
-           raise TypeError(f"'{cls.__qualname__}' must be declared at module level.")
-   ```
-
-   It is neither necessary nor sufficient — `type("Dyn", ...)` inside a
-   function passes, a class `del`'d after creation passes — so the
-   authoritative check remains pickle's own `save_global` at pickle time,
-   exactly as for any class. The `spawn`-based compile workers of
-   `otf/runners.py` re-execute the main script as `__mp_main__`, so classes
-   declared in a *file's* `__main__` resolve there (provided the script has
-   an `if __name__ == "__main__":` guard, which the pool already requires).
-   What does not resolve is *interactive* `__main__`: the REPL, notebooks,
-   `python -c`. Documented limitation, not fixed.
-3. **No registry, no `copyreg`.** Classes pickle by reference, which is
-   correct for module-level types; #2844's `copyreg.pickle(DimensionMeta, ...)`
-   and `_DIMENSION_REGISTRY` are removed again. Nothing equivalent creeps
-   back in, because string-keyed providers are not accepted at all (there is
-   no deprecation window), so no name→class table is ever needed.
-4. **Cache fingerprints depend on module paths.** #2844 adds a
-   `fingerprinting.py` deconstructor keyed on `(tag, kind)` (recorded in
-   ADR 0028) *specifically so that* a dimension is not fingerprinted by
-   qualified name. Under type identity it is, by definition; renaming a
-   module invalidates compiled artifacts (ADR 0023's cache). Correct for
-   this model; a consequence to record, not a reversal of ADR 0023 itself.
-5. **Codegen names need injective mangling.** `generated::<tag>_t` (gtfn) and
-   DaCe symbols cannot contain dots. One shared `codegen_name(tag)`, injective
-   (escape existing `__` before replacing `.`), used by both backends; gtfn's
-   existing `TagDefinition.alias` mechanism can shorten where needed.
-6. **Staggering comes into scope.** `flip_staggered` builds
-   `Dimension(f"_Staggered{name}")` from a string (`common.py:1452-1457`).
-   There is no such type to import, so ADR 0026's prefix cannot survive
-   type identity; `Staggered[D]` becomes a real parametrized dimension type.
-   This is the `DimensionBase` extension point named in
-   [[shared/dimensions-as-types|dimensions as types]], now with a concrete
-   requirement.
+1. **Reconstruction from the IR is an import.** `resolve(tag)` imports the
+   longest importable module prefix and walks the rest as attributes (nested
+   classes like `V2E.Local` resolve naturally), the way `pickle` references a
+   class. Only where the module path ends is memoized: the attribute walk is
+   repeated, so a declaration redefined under the same name (a re-run
+   notebook cell) resolves to the new class. `AxisLiteral` stores only the tag
+   and derives `kind` and `dim` from it (the `TODO` at `iterator/ir.py:93`);
+   printing IR never imports (`resolve_loaded`). `Staggered[D]` tags use the
+   small grammar `<owner tag>[<base tag>]`, resolved by subscripting the owner.
+2. **Types reaching the IR must be importable.** `<locals>` in a qualname is
+   rejected at class creation (for dimensions and connectivities); pickle's
+   own `save_global` stays the authoritative check. Interactive `__main__`
+   (REPL, notebooks, `python -c`) turned out to matter — every notebook
+   declares its dimensions there — so the process-pool runner
+   (`BUILD_JOBS_MODE=process`) detects a job that references such a class
+   and, with a warning, **compiles it in the calling thread** instead of
+   failing in a spawn worker.
+3. **No registry.** Classes pickle by reference. One narrow `copyreg` hook
+   remains, for `Staggered[D]`, whose bracketed qualname `save_global` cannot
+   look up; it reduces to the base dimension and re-interns.
+4. **Fingerprints depend on qualified names.** Dimensions are fingerprinted by
+   reference (`Staggered[D]` through its base); a connectivity declaration
+   additionally by its origin, codomain, `Local` and counts, so a redefinition
+   under the same name does not reuse artifacts.
+5. **Codegen names need injective mangling.** `codegen_name(tag)` is a prefix
+   escape — `_`→`_u`, `.`→`_d`, `[`→`_l`, `]`→`_r` — used by gtfn, DaCe, the
+   roundtrip backend and the nanobind bindings; its inverse
+   `from_codegen_name` is used by DaCe to parse names back. The first
+   draft's "escape `__` then replace `.`" was **not** injective (`".."` and
+   `"_"` collide); the prefix escape is tested exhaustively over its alphabet
+   up to length 4.
+6. **Staggering came into scope, and earlier than planned.**
+   `Staggered[D]` is an interning metaclass subscription producing a real
+   class at runtime (a PEP 695 generic would give a `typing` alias, which
+   fails `issubclass` and eve's `type[...]` validation); under
+   `TYPE_CHECKING` it *is* declared as a PEP 695 generic, so checkers accept
+   `Staggered[K]` in annotations. It had to land with the
+   dimension change itself, since the old `_Staggered` name prefix needs a
+   name→class registry.
+7. **The IR names a connectivity by its `offset_tag`.** That is its local
+   dimension's tag when it declares the local dimension: shifts, reductions
+   and sparse arguments then all find the table under **one** string, which
+   made the backends' A3/A4 lookups correct without touching them. A
+   connectivity *sharing* another one's local dimension is named by its own
+   tag, since the local tag already names the owner's table; for that case
+   the backends needed a fallback lookup, `connectivity_key_over` (see *The
+   local dimension*).
 
 ### Binding model
 
 The connectivity *type* conceptually depends on the *table*: two different
 tables assign different neighbors to the same origin element. The model:
 
-- The class `V2E` is a **type constructor**. Its static part — `Origin`,
-  `Codomain`, `Local`, and *optionally* `max_neighbors` / `min_neighbors` —
-  is what compilation sees. When the counts are declared, they are a
-  constraint the table must satisfy. When they are not, they are **completed
-  at bind time**: from the table's shape and skip value in the JIT flow, or
-  from a `NeighborConnectivityType` supplied through `connectivities=` in the
-  AOT flow (`ffront/decorator.py:188-208`), which already passes exactly that
-  record without any data. `NeighborConnectivityType` is derived from class
-  plus binding, and is complete only once both are known.
+- The class `V2E` is a **declaration**. Its static part — `V2E.origin`,
+  `V2E.codomain`, `V2E.Local`, and *optionally* the counts
+  `V2E.Local.max_neighbors` / `V2E.Local.min_neighbors` (they are stored on
+  the local dimension; `V2E.max_neighbors` does not exist) — is what
+  compilation sees. Declared counts are a constraint on the table; undeclared
+  ones are simply taken from the bound table's `NeighborConnectivityType` when
+  a variant is compiled. Binding never writes anything back to the class.
 - Why the counts are not static-only. Two in-tree and in-ICON facts: the
-  arity of the same connectivity varies per mesh (`fvm_nabla_setup.py:99`
-  sizes `V2E` from `edges_per_node`, computed from the atlas mesh), so a
-  static count binds the DSL source to one mesh family and makes
-  `Field[Dims[Vertex, V2E.Local]]` signatures unshareable across meshes; and
-  skip-value presence is *configuration*-dependent in ICON (`icon.py:130`:
-  pentagon offsets have skip values on the icosahedron but not on the torus;
-  boundary offsets only on limited-area or distributed grids), so a static
-  `min_neighbors` would force ICON4Py to either declare two classes per
-  boundary offset or always compile skip-mask handling, defeating its
-  `keep_skip_values=False` table rewrite (`base.py:180`). Declared counts
-  remain the right choice for fixed-arity meshes, and the compile cache is
-  unaffected either way: `NeighborConnectivityType` is part of the key today
-  and stays so.
-- A **bound connectivity** is the class plus a table. Within one program
-  invocation there is exactly one table per class, so every occurrence of
-  `V2E` in that invocation denotes the same mapping. The provider
+  arity of the same connectivity varies per mesh (`fvm_nabla_setup.py` sizes
+  `V2E` from the atlas mesh), and skip-value presence is
+  *configuration*-dependent in ICON (`icon.py:130`: pentagon offsets have skip
+  values on the icosahedron but not on the torus), so a static `min_neighbors`
+  would force duplicate classes or always-on skip handling.
+- A **bound connectivity** is the class plus a table; the provider
   `{V2E: table}` *is* the binding, and a dict makes one-table-per-class
   structural.
-- The table is validated against the static part **once, at bind time**:
-  shape `(n, max_neighbors)`, integral dtype, skip values present iff
-  `min_neighbors < max_neighbors`. This one runtime check replaces the whole
-  declaration-vs-provider family of constraints (A6–A8 in the appendix); they
-  do not vanish, they become a single validated invariant.
-- The class never holds data. `_ConnectivityFileRef` and the compile cache
-  (ADR 0023) keep working unchanged: the type part is fingerprinted by
-  qualified name, the table crosses process boundaries as it does today.
+- **Normalized at the entry points.** `as_tag_keyed_offset_provider`
+  rewrites the provider to the form the IR uses, keyed by `offset_tag`. It is
+  called *strictly* by `Program.__call__`, `FieldOperator.__call__`,
+  `FieldOperatorFromFoast.__call__`, `compile` and
+  `CompilationOptions.connectivities`, and *non-strictly* by
+  `embedded.context.update`, the iterator `fendef` and DaCe
+  `get_sdfg_conn_args`.
+  Strict means that a key which is neither a declaration nor a dotted tag
+  string — e.g. `"V2E"`, the removed `FieldOffset` spelling — raises
+  `TypeError`; the iterator-level hooks accept any string, since hand-written
+  IR names offsets freely. A dotted string is accepted as an
+  already-normalized tag everywhere, and class and string keys can be mixed
+  (binding one tag twice is an error). Lowering, the backends and the
+  compiled-program cache keep seeing tag-keyed providers — like hand-written
+  IR — so the backends' accesses *by connectivity tag* did not change; those
+  keyed by a *local dimension* (reductions, sparse and list arguments) now
+  find the table through `connectivity_key_over`.
+- **Validated at the boundary.** `check_offset_provider` runs at *every* entry
+  point, including the iterator `fendef`, `FieldOperatorFromFoast` and the DaCe
+  orchestration's `CompilationOptions.connectivities`. Its result is remembered
+  per set of bound tables (hashed by their `id`, as the compiled-program cache
+  keys its variants), so a repeated call with the same tables costs one hash;
+  like that cache, the memo can in principle skip a check when a freed table is
+  replaced at the same address. Reading the tables — comparing skip positions,
+  below — happens only where a program is compiled, not on the call path. It
+  calls `check_neighbor_table` per declaration, which checks the domain
+  `(Origin, Local)` and the codomain by class identity (with a hint when a
+  declaration looks redefined), an integral dtype, `max_neighbors` equal to
+  the table's width and `min_neighbors` not above it if declared, and — only
+  when `min_neighbors` is declared — that the table has a skip value iff
+  `min_neighbors <` its width. Skip values are judged on the table's *type*:
+  the number of valid neighbors per row is never counted. `check_offset_provider`
+  additionally requires all tables over one local dimension to agree on width
+  and skip-value presence and — where a program is compiled — on the skip
+  positions of the concrete tables, compared on the device the tables live on.
+  A key that names the *connectivity* instead of the declaration (`{V2E.tag:
+  table}`, which is the IR name only of a connectivity that shares a local
+  dimension) is rejected with a pointer to `{V2E: table}`. A string key that is
+  not a qualified name at all is remembered as such, so it costs one import
+  attempt in total rather than one per call.
+- The class never holds data; the table crosses process boundaries as it did.
+
+In dependent-typing terms, the "true" type of a local index is
+`Fin<degree(table, v)>`: it depends on the table *value* and on the origin
+element. Python types cannot mention values, so the design keeps the part a
+checker can see — *which* neighbor relation the index belongs to, as the
+nominal type `V2E.Local` — and turns the value-dependent part into a
+validate-at-the-boundary check whose result is reused downstream. The
+[[personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing|dependent-typing appendix]]
+develops this with a worked example and lists what is kept, checked and given
+up.
 
 ### The local dimension
 
-- `V2E.Local` **must be declared explicitly** as a nested
-  `class Local(LocalDimensionIndex): ...`; `__init_subclass__` verifies it
-  and sets `Local.owner`. There is no generated form. This is settled by
-  running both checkers on
-  [`typing_probe.py`](connectivities-as-types/typing_probe.py): an explicitly
+- `V2E.Local` **must be given explicitly** in the class body — a nested
+  `class Local(LocalDimensionIndex): ...`, or an existing local dimension to
+  adopt or share (below); `__init_subclass__` verifies it (a missing `Local`
+  is a `TypeError`) and sets `Local.owner`. There is no generated form. This
+  is settled by running both checkers on
+  [`typing_probe.py`](typing_probe.py): an explicitly
   declared nested `Local` is a real, distinct type under mypy `--strict` and
-  pyright (`Field[V, V_E2E.Local]` vs `Field[E, E_V2V.Local]` is an
-  `arg-type` error), while a `Local` generated in `__init_subclass__` and
+  pyright (`Field[V, V_E2E.Local]` vs `Field[V, E_V2V.Local]`, differing only
+  in the local dimension, is an `arg-type` error, probe P1b), while a `Local`
+  generated in `__init_subclass__` and
   annotated `ClassVar[type[LocalDimensionIndex]]` on the base is rejected by
   both as *not valid as a type* — the very error class
   [[shared/dimensions-as-types|dimensions as types]] exists to remove. Two
@@ -362,92 +425,147 @@ tables assign different neighbors to the same origin element. The model:
 - `Local` is **not** passed through the base subscription
   (`NeighborConnectivity[V, "V2E.Local", E]`): mypy accepts that string
   forward reference, pyright reports `Class definition for "V2E" depends on
-  itself`. The metaclass reads `cls.Local` after the class body has run; on
-  Python 3.13 a PEP 696 default type parameter is the typed alternative.
+  itself`. `__init_subclass__` reads it from the class body instead.
+- **`Local` is annotated nowhere**, and that is load-bearing. An annotation on
+  the base (`Local: ClassVar[type[LocalDimensionIndex]]`) or on the metaclass
+  makes a declaration's `Local` a *variable* for the checkers, so
+  `Field[Dims[V, V2E.Local], float]` is rejected — by pyright for a nested
+  `Local` ("Variable not allowed in type expression"), by mypy for an adopted
+  or shared one ("not valid as a type"). A real nested `Local` on the base is
+  not an option either: pyright reports an incompatible override in every
+  declaration. With no annotation anywhere, all three spellings are types for
+  both checkers.
+  The cost is that `conn.Local` is not an attribute the checkers know for a
+  *generic* `conn`: library code reads it through
+  `common.local_dimension_of(conn)`, and code that must name a local dimension
+  generically uses a `TypeVar` bound to `LocalDimensionIndex`. This is checked
+  for both checkers in CI: the mypy cases in `typing_tests/test_next.yaml`, and
+  a pyright run over `typing_tests/pyright_probes.py` in the same nox session
+  (pyright is what catches the annotation regression; mypy accepts it).
+- A declaration can instead **adopt** a module-level local dimension, written
+  `Local: typing.TypeAlias = V2EDim`; the local keeps its own tag, which is then
+  the connectivity's `offset_tag`. This is also how the migration script
+  rewrites existing `FieldOffset`s without renaming anything. Adopting is *not*
+  side-effect free: the adopter becomes the local's `owner` and writes its
+  counts onto the module-level class, and ownership is first-come — the first
+  connectivity declared over a local dimension owns it, later ones share it. A
+  declaration *redefined* under the same tag (a re-run notebook cell) takes
+  ownership over again rather than becoming a sharer, and the counts it repeats
+  are then checked against the local dimension's own `size=`, not against what
+  the stale owner wrote. `ConstList` cannot be adopted: it belongs to no
+  connectivity.
+- A connectivity can **share** another one's local dimension
+  (`class C2CE(NeighborConnectivity[C, CE]): Local: typing.TypeAlias =
+  C2E.Local`). ICON4Py's flattened sparse offsets (`C2CE`, `E2ECV`, `E2EC`,
+  `C2CEC`) need exactly this, because their results must combine with
+  `C2E`-shaped sparse fields. The
+  owner stays the first declaration over the local (here `C2E`); the sharer
+  must have the same origin (its codomain is free), any counts it repeats must
+  equal the owner's, and reductions over the shared axis take the neighbor
+  structure from any bound table over it (`connectivity_key_over`: the owner's
+  key if bound, else the smallest bound key over that local, which raises
+  `KeyError` if there is none).
+- **Write an adopted or shared `Local` as a `TypeAlias`.** `Local: TypeAlias =
+  C2E.Local` is what keeps mypy treating `C2CE.Local` as a type; with a plain
+  assignment it is "not valid as a type" there (pyright accepts either, but
+  widens the plain form to `LocalDimensionIndex`). With the alias, annotations
+  may name the local dimension through any of its spellings — `C2CE.Local`,
+  `C2E.Local`, `V2EDim` — and they are one type.
 - `max_neighbors` / `min_neighbors` are class keywords, exactly as #2844 does
   `kind`, and optional (see Binding model). They are *not* type parameters:
   Python has no integer-valued type parameters, and nothing static needs the
   count — what must be in the type is *which* local dimension.
 - **Owner-less local dimensions** exist: `class LsqUnk(LocalDimensionIndex, size=3)`
   has `owner = None`, `min == max == size`, no skip values, and never appears
-  in the provider. ICON4Py needs this today: `LsqUnkDim` (`dimension.py:18`,
+  in the provider — unless a connectivity later adopts it, which makes it
+  owned. `size` is optional; an owner-less local without it has no counts. ICON4Py needs this today: `LsqUnkDim` (`dimension.py:18`,
   LOCAL kind, "number of least-squares unknowns") is the middle axis of a
   coefficient field over `(CellDim, LsqUnkDim, C2E2CDim)` and indexes no
   table; `RBFDimension` is an enum of stencil sizes that plays the same role.
   Such axes want the *storage and layout* treatment of a sparse dimension,
   not a connectivity; declaring them non-LOCAL instead would make them domain
   dimensions requiring a range in every program domain and would change
-  ICON4Py's memory layout for those fields. Backends handle the owner-less
-  form exactly as they handle `_CONST_DIM` today, generalized from size 1 to
-  size *n*.
-- `_CONST_DIM` (`iterator/embedded.py:220`) is therefore the owner-less
-  `ConstList(LocalDimensionIndex, size=1)`, replacing a magic name that is
-  special-cased at twelve use sites today (six in `iterator/embedded.py`,
-  six in the DaCe lowering).
+  ICON4Py's memory layout for those fields. (Backend support for sparse fields
+  over an owner-less axis *other than* `ConstList` is not part of the stack:
+  such a field still needs some bound table over its axis.)
+- `_CONST_DIM` is replaced by the owner-less
+  `common.ConstList(LocalDimensionIndex, size=1)`, one class used by iterator
+  embedded and the DaCe lowering with identity checks, and refused as an
+  adopted `Local`. (Type inference still
+  represents a constant list as `ListType(offset_type=None)`.)
 - `neighbor_sum(..., axis=V2E.Local)` — the local axis stays **explicit**.
   `axis=V2E` as sugar is deliberately not offered; it would blur the two
-  concepts the design separates.
+  concepts the design separates. Passing it is a type error in DSL code.
 
 ### `MultiDimensionIndex`
 
-Included so the final picture is complete, even though it is the last piece
-to implement and nothing else depends on it:
-
-- It is the **index type of a sparse-field position**. `V2E.Local(2)` alone
-  cannot address an element; `(V(3), V2E.Local(2))` can. Today that pair is a
-  dict keyed by dimension-name strings (`iterator/embedded.py:597-616`).
-- It is the **domain index of a `NeighborConnectivity`**, which is what makes
-  `Connectivity[MultiDimensionIndex[Origin, Local], Codomain]` a real
-  index-to-index function type.
-- `*Ls` is unconstrained because `TypeVarTuple` cannot carry a bound; a
-  runtime check in `__init_subclass__` covers what the checker cannot.
+- `MultiDimensionIndex(Vertex(3), V2E.Local(2))` is a position in the product
+  of a primary and local dimensions. It is a `tuple` subclass, so it indexes a
+  field or a table directly (`v2e_table[position]`, a 0-d field), and compares
+  and hashes like the plain tuple; `pickle` and `copy` keep it a
+  `MultiDimensionIndex`, tuple operations such as slicing do not. It is a
+  user-facing typed index; nothing in the toolchain requires it.
+- `*Ls` is unconstrained because `TypeVarTuple` cannot carry a bound, so the
+  constructor checks the shape at runtime: one non-local index, then *at least
+  one* local index, and an owned local dimension must index the neighbors of the
+  primary index's dimension — `MultiDimensionIndex(Edge(1), V2E.Local(1))` is a
+  `TypeError`, since `V2E` indexes the neighbors of a vertex. An owner-less
+  local axis (`LsqCoeff`) is accepted next to any primary dimension.
+- The original note also made it "the domain index of a
+  `NeighborConnectivity`", i.e. `Connectivity[MultiDimensionIndex[Origin,
+  Local], Codomain]`. That was dropped with the decision that a declaration is
+  not a `Connectivity` (see Open question 6).
+- The iterator-level embedded execution keys its positions by dimension
+  classes instead of tag strings and steps along a local dimension with an
+  explicit `SparseAxis(dim)`; `SparseTag` is gone.
 
 ### Effect per layer
 
-| Layer | Today | Under the proposal |
+| Layer | Before | As implemented |
 | --- | --- | --- |
 | Frontend declaration | `Dimension(LOCAL)` + `FieldOffset` + provider key | one class |
-| Frontend types | `ts.OffsetType(source, target)`, tag dropped | `ConnectivityType`, produced by the class (`TODO` at `type_specifications.py:74`) |
-| FOAST → GTIR | shift tag = **Python variable name** (`foast_to_gtir.py:305, 331`) | tag = `cls.tag`; the variable name is irrelevant |
-| ITIR | `OffsetLiteral(str)` + dict lookup | node carries the local dim's tag, resolved by import — the `CartesianOffset` pattern |
+| Frontend types | `ts.OffsetType(source, target)`, tag dropped | `ts.OffsetType` produced by the class (`__gt_type__`), its `tag` field (added in PR 1) set to `offset_tag`; `V2E.Local` in DSL code types as the local dimension |
+| FOAST → GTIR | shift tag = **Python variable name** | tag = `offset_tag`; the variable name is irrelevant (fixed first, as PR 1) |
+| ITIR | `OffsetLiteral(str)` + dict lookup; `AxisLiteral(value, kind)` | `OffsetLiteral(offset_tag)`, unchanged node; `AxisLiteral(value)` with `kind` derived |
 | ITIR types | `ListType.offset_type: Dimension` | unchanged (already the local dim) |
-| Embedded field | `get_offset(provider, axis.value)` | `axis.owner`, bound table from context |
-| Embedded iterator | positions keyed by name strings; `SparseTag` | `MultiDimensionIndex` positions (last step) |
-| gtfn | `dim.value` lookups for sparse args; `TagDefinition` per tag and per `neighbor_dim` | `local_dim.owner`; `codegen_name(tag)` |
-| DaCe | ~10 `offset_type.value` lookups; `Dimension(offset, LOCAL)` synthesized at `gtir_to_sdfg_lambda.py:1155` | `local_dim.owner`; no synthesis |
-| roundtrip backend | emits `gtx.Dimension("<name>", kind=...)` / `offset("<tag>")` as *source text* (`runners/roundtrip.py:175-179`) | emits imports of the qualified names, via `codegen_name` for the Python identifier |
-| Provider | `Mapping[str, NeighborTable]` | `Mapping[type[NeighborConnectivity], NeighborTable]`; **no string keys** and no deprecation window (a scripted migration for ICON4Py instead) |
+| Embedded field | `get_offset(provider, axis.value)` | table over the local dimension (`connectivity_key_over`); `V2E.bound_table()` |
+| Embedded iterator | positions keyed by name strings; `SparseTag` | positions keyed by dimension classes; `SparseAxis(dim)` |
+| gtfn | `dim.value` lookups; `TagDefinition` per tag and per `neighbor_dim` | still a `TagDefinition` per offset tag (and per differing `neighbor_dim`, i.e. for sharers), named by `codegen_name(tag)`; sparse-argument lookups through `connectivity_key_over` |
+| DaCe | ~10 `offset_type.value` lookups; `Dimension(offset, LOCAL)` synthesized | `codegen_name` for array/symbol names; `connectivity_key_over`; a local dimension sized from its own table (`local_dimension_size`); no synthesis |
+| roundtrip backend | emits `gtx.Dimension("<name>")` / `offset("<tag>")` as source text | emits `<mangled> = gtx.resolve("<tag>")` for axes and `<mangled> = offset("<tag>")` for offsets |
+| Provider | `Mapping[str, NeighborTable]` | public: `{V2E: table}` (a dotted tag string is also accepted; the type stays `Mapping[Any, …]`); internal: keyed by `offset_tag`, normalized at the entry points; no deprecation window (a migration script for ICON4Py instead) |
 
 ### What it deletes
 
-`FieldOffset` as the unstructured declaration; `runtime.Offset` as its base
-(the `TODO` at `fbuiltins.py:467-470`); `ts.OffsetType`; the four
-`OffsetProvider*` aliases in their
-string-keyed form; `dimension(tag, kind)`, the interning registry and the
-`copyreg` hook from #2844; the `_Staggered` prefix and its string sniffing;
-`_CONST_DIM` as a magic name; and the convention that
-`V2EDim = Dimension("V2E", LOCAL)` must sit next to `V2E = FieldOffset("V2E", ...)`.
-
-**Deleted only together with its replacement:** the single-target
-(Cartesian) `FieldOffset` form. Cartesian *shifts* already use
-`Dimension + int` (GridTools/gt4py#2411), but `as_offset(offset, field)`
-(`ffront/experimental.py:17`) requires a Cartesian `FieldOffset`
-(`type_deduction.py:956-967`, S6 in the appendix), is used in 5 test modules
-plus the `Ioff`/`Koff`/`EdgeOffset` fixtures in `cases_utils.py:163-169`, and
-ICON4Py calls it in diffusion and the dycore (`as_offset(Koff, ...)`, with
-`offset_provider={"Koff": KDim}`). Since there is no deprecation window, a
-dimension-based signature — `as_offset(KDim, field)` is the obvious
-candidate — must land in the **same release** that removes `FieldOffset`,
-and the migration script must rewrite these call sites too.
+`FieldOffset` (both forms) and its export; bare-name provider keys (rejected
+at the strict entry points); the `_Staggered` prefix and its string sniffing
+(replaced by the `Staggered[D]` class and a small `<owner>[<base>]` tag
+grammar); `_CONST_DIM` as a magic name; the stored `AxisLiteral.kind`;
+`SparseTag`; `NamedIndex` and the dimension half of the mypy plugin;
+`DimensionIndex(kind=LOCAL)` as a way to declare a local dimension; and the
+convention that `V2EDim = Dimension("V2E", LOCAL)` must sit next to
+`V2E = FieldOffset("V2E", ...)`. **Not adopted** from #2844 (they were never
+on `main`): `dimension(tag, kind)`, the interning registry and the general
+`copyreg` hook (only a narrow one for `Staggered[D]` exists).
+
+**Kept**, contrary to the original note: `ts.OffsetType` (it types
+declarations, `V2E[i]`, Cartesian `Dim ± i` and `as_offset`; renaming it to
+`ConnectivityType` would be churn without a user-visible gain), `iterator.runtime.offset("...")` (the
+iterator-level API names offsets by string, like the IR), and string-keyed
+providers *below* the entry points.
+
+The Cartesian `FieldOffset` went in the same PR as the unstructured one:
+Cartesian shifts were already `Dim + i`, and `as_offset` now takes the
+dimension, `as_offset(KDim, field)`.
 
 ### Relation to `Local[V2E]`
 
-[[personal/havogt/dependent-local-dimensions|Dependent local dimensions]]
+[[personal/havogt/dependent-local-dimensions/dependent-local-dimensions|Dependent local dimensions]]
 spells the local dimension `Local[V2E]` (a generic parametrized by the
 connectivity); this proposal spells it `V2E.Local` (a class nested in the
 connectivity). They **cannot be reconciled for a type checker**: making
 `Local.__class_getitem__` return `V2E.Local` unifies them at runtime only.
-[`typing_probe.py`](connectivities-as-types/typing_probe.py) shows both mypy
+[`typing_probe.py`](typing_probe.py) shows both mypy
 and pyright treating `Field[V, V2E.Local]` and `Field[V, Local[V2E]]` as
 incompatible in both directions. One spelling has to win, and this proposal
 picks `V2E.Local`: the nested form is what makes the tag unique with no
@@ -504,7 +622,7 @@ Declared counts stay available as a constraint; see Binding model.
 **A generated `Local` as the default, explicit declaration optional.**
 Rejected after running the checkers: a `ClassVar`-typed generated `Local` is
 not usable in an annotation under mypy or pyright
-([`typing_probe.py`](connectivities-as-types/typing_probe.py), probe P2).
+([`typing_probe.py`](typing_probe.py), probe P2).
 
 **`Local[C]` as the spelling, with `V2E.Local` an alias.** Rejected: the two
 are distinct types for every checker (probe P3); see Relation to `Local[V2E]`.
@@ -540,7 +658,7 @@ sparse storage treatment, changing ICON4Py's layout for `LsqUnkDim` fields.
   `(tag, kind)` fingerprint deconstructor; under type identity dimensions are
   fingerprinted by qualified name instead, and ADR 0023's cache invalidates
   on module renames. A consequence to record in the new ADR.
-- **[[personal/havogt/mesh-and-first-class-halos|A mesh concept with
+- **[[personal/havogt/mesh-and-first-class-halos/mesh-and-first-class-halos|A mesh concept with
   first-class halos]].** Proposes replacing the `offset_provider` dict with a
   Mesh object and keeps `Koff`/`LsqUnkDim` outside it. This note re-types the
   same dict. The two are compatible if the Mesh binds typed connectivity
@@ -548,88 +666,127 @@ sparse storage treatment, changing ICON4Py's layout for `LsqUnkDim` fields.
   and the multi-table case (halo variants, rewritten `keep_skip_values`
   tables, several meshes in one process) is addressed by neither yet.
 - **ADR 0026 (Staggered dimensions).** The `_Staggered` name prefix cannot
-  survive type identity; `Staggered[D]` is required, not optional.
+  survive type identity; `Staggered[D]` is required, not optional
+  (implemented in PR 2).
 - **ADR 0019 (Connectivities).** The part naming `FieldOffset` as the
-  frontend identifier is superseded; the `Connectivity` / `NeighborTable` /
-  `ConnectivityType` vocabulary is kept and strengthened.
+  frontend identifier is superseded (by ADR 0029); the `Connectivity` /
+  `NeighborTable` / `ConnectivityType` vocabulary is kept.
 - **[[personal/havogt/closure-variable-resolution|Closure variable
   resolution]].** The N2 leak (Python variable name becoming the IR tag) is a
   closure-variable-resolution bug in `foast_to_gtir`; that proposal's
   resolution mechanism should be the vehicle for the fix.
 
-**Open:**
-
-1. **Naming.** `NeighborConnectivity[Origin, Codomain]` vs the sketch's
-   `StaticMultiConnectivity[F, L, T]` vs the existing
-   `NeighborConnectivityType.source_dim`/`neighbor_dim` (a third vocabulary
-   this note would otherwise add to the two it criticizes); `Local` vs `Dim`;
-   `min_neighbors` vs `has_skip_values`. Converge with
-   [[personal/havogt/dependent-local-dimensions|dependent local dimensions]]
-   before either lands.
-2. **How `Local` reaches the base's parametrization.** Discovered by the
-   metaclass after the class body (works on 3.12, untyped in the base), or a
-   PEP 696 default type parameter (3.13, typed)? AGENTS.md invites 3.13
-   features where they improve a design; this is a candidate.
-3. **`__main__` in spawn workers.** Document, or detect and fall back to
-   in-process compilation with a warning?
-4. **ICON4Py migration.** `gtx.FieldOffset`, `Dimension(..., LOCAL)`,
-   `as_offset(Koff, ...)` and string-keyed providers (`{"V2E": ..., "Koff": KDim}`)
-   are all public and all change in **one release, with no deprecation
-   window**. ICON4Py's keys are bare names, so no import-based shim could
-   have resolved them anyway; the migration is a script over
-   `dimension.py` (16 offsets, 15 local dims), the `offset_provider`
-   construction in `grid/base.py`, and the `as_offset` call sites. `LsqUnkDim`
-   becomes an owner-less `LocalDimensionIndex` with `size=`. What the script
-   cannot decide is whether each connectivity declares its counts or leaves
-   them to bind time; the ICON skip-value rules (`icon.py:130`) suggest
-   leaving `min_neighbors` open for the boundary offsets.
-5. **Duplicate declarations.** With type identity, two modules declaring
-   `class V2E(...)` are two connectivities. Is a warning on same-`__name__`
-   collisions in one program useful, or noise?
-6. **What is an instance of `V2E`?** Today `Connectivity` is
-   `Field[DimsT, IntegralScalar]` parametrized by `Dims` plus a codomain
-   (`common.py:990`), and `CartesianConnectivity` is a dataclass with
-   instances. The sketch's `Connectivity[Src, Dst]` is a different
-   parametrization, and `V2E` is a data-less type constructor subclassing a
-   runtime protocol. Either instances of `V2E` are the bound tables (so
-   `{V2E: table}` becomes `V2E(table)`), or `NeighborConnectivity` is not a
-   `Connectivity` subclass at all and only *produces* one at bind time. The
-   sketch leaves this open and should not.
-
-## Staging
-
-Each step is landable separately and leaves the tree green.
-
-0. **Fix the N2 leak now, independently.** `foast_to_gtir.py:305, 331` emit
-   the offset's own tag; extend `test_offset_dimensions_names.py` to
-   `neighbor_sum`, embedded and DaCe so A3 is *visible*. This is a bug today.
-1. **#2844 lands**, then the `DimensionBaseIndex` root and type identity
-   (registry and `copyreg` removed, importability rule added,
-   `resolve(tag)` by import). Revision of `shared/dimensions-as-types.md`.
-2. **`NeighborConnectivity` + `LocalDimensionIndex`** (owned and owner-less)
-   in `common`; object-keyed provider; `FieldOffset` and string keys removed
-   outright; bind-time completion and validation of the counts.
-3. **`ts.OffsetType` → `ConnectivityType`**; `as_offset` gets its
-   dimension-based signature in the same step, so the Cartesian `FieldOffset`
-   form can go with the rest.
-4. **Backends** switch from `local_dim.value` lookups to `local_dim.owner`,
-   one file at a time (`gtfn_module.py`, `unroll_reduce.py`, `gtir_to_sdfg*.py`,
-   `nd_array_field.py`, `iterator/embedded.py`, and the source-emitting
-   `runners/roundtrip.py`). `codegen_name` introduced.
-5. **`Staggered[D]`**, superseding ADR 0026; `_CONST_DIM` becomes the
-   owner-less `ConstList` local dimension.
-6. **`MultiDimensionIndex`** and typed embedded positions.
-7. **Typing tests** (`typing_tests/test_next.yaml`, pyright): `Field[Dims[V, V2E.Local], float]`,
-   a `TypeVar` bound to `LocalDimensionIndex`, a negative case mixing two
-   connectivities' locals — the probes in
-   [`typing_probe.py`](connectivities-as-types/typing_probe.py) are the
-   starting set.
-8. **Test-tree migration** as its own PR (`toy_connectivity.py`,
-   `cases_utils.py`, `fvm_nabla_setup.py` are the fixture modules everything
-   imports).
-
-An ADR in gt4py (next in sequence after 0028) should record steps 1–2, since
-they reverse two recorded decisions and change a public-API shape.
+**Open questions, and how the implementation answered them:**
+
+1. **Naming.** Implemented with `NeighborConnectivity[Origin, Codomain]`,
+   `Local`, `max_neighbors` / `min_neighbors`, and `offset_tag` for the IR
+   name. Convergence with
+   [[personal/havogt/dependent-local-dimensions/dependent-local-dimensions|dependent local dimensions]]
+   (`Dim`, `has_skip_values`, `source_dim`/`neighbor_dim`) is still to be
+   discussed on the PRs; the names are public from PR 3 on.
+2. **How `Local` reaches the base.** `NeighborConnectivity.__init_subclass__`
+   reads `cls.__dict__["Local"]` after the class body, with a `ClassVar`
+   annotation on the base (3.12-compatible). A PEP 696 default type parameter
+   was not needed.
+3. **`__main__` in spawn workers.** Detected: under the process-pool runner,
+   jobs referencing a class of an interactive `__main__` are compiled in the
+   calling thread, with a warning.
+4. **ICON4Py migration.** `scripts/python/migrate_connectivities.py` rewrites
+   `Dimension(...)` and `FieldOffset(...)` declarations (connectivities adopt
+   their existing local dimensions, so `C2EDim` etc. keep working and `C2CE`
+   becomes a sharer), removes Cartesian offsets and rewrites their uses
+   (`Koff[1]` → `KDim + 1`, `as_offset(KDim, ...)`, imports), and reports
+   what it cannot decide from the source. The counts depend on the ICON4Py
+   revision, so GridTools/gt4py#2910 quotes a pinned one: at ICON4Py
+   `89b4967` (2026-09-21), after ICON4Py had already dropped `Koff[1]`, the
+   script rewrites 4 files (`dimension.py` and 3 stencil modules) and reports
+   46 connectivity provider keys, 2 removable Cartesian provider entries and 10
+   `isinstance(..., Dimension)` sites in 5 modules. Declaring counts is left to
+   ICON4Py.
+5. **Duplicate declarations** (two same-named declarations from different
+   modules, or a redefinition). No warning was added; being different
+   classes, they are simply different connectivities, and
+   `check_neighbor_table` hints "was the declaration redefined?" when a table
+   built for one is bound to the other.
+6. **What is an instance of `V2E`?** Nothing: `NeighborConnectivity` is **not**
+   a `Connectivity`, and instantiating a declaration raises. The table stays a
+   `Connectivity` implementation and is *checked against* the declaration.
+   `Field.premap`/`__call__` accept either a table or a declaration, as they
+   accepted a `FieldOffset` (which was not a `Connectivity` either).
+7. **New: connectivities sharing a local dimension** (raised by the review of
+   the test-tree migration): needed for ICON4Py's flattened sparse offsets;
+   answered by adopting an owned `Local` and naming the sharer by its own tag.
+
+## Implementation
+
+A stack of GridTools/gt4py PRs, each green in CI on its own. It is an
+alternative to #2844 (which implemented `(name, kind)` value identity) that
+takes over the parts of #2844 compatible with type identity. The one
+substantive review so far (on #2899) prefers this approach over #2844 but
+raises the churn and the long qualified names.
+
+| # | PR | What |
+| --- | --- | --- |
+| 1 | GridTools/gt4py#2898 | `fix[next]`: lower unstructured shifts with the offset's own tag (the N2 leak); adds `ts.OffsetType.tag` and makes shift lowering type-driven, so module-qualified offsets (`a(mod.V2E)`) work (supersedes #2730); regression matrix {shift, `neighbor_sum`} × {tag ≠ variable name, tag ≠ local-dimension name}. A later review commit (`25f7a32c4`, 2026-09-23) reports invalid shift arguments as located `DSLError`s; it is not yet in PRs 2–8, and #2899 currently conflicts |
+| 2 | GridTools/gt4py#2899 | `feat[next]`: a concrete dimension is a class identified by its qualified name (ADR 0028); `codegen_name`; `Staggered[D]`; interactive-`__main__` fallback; `NamedIndex` and the dimension half of the mypy plugin removed; the one-string invariant pulled forward (`FieldOffset(V2EDim.tag, ...)`, `{V2EDim.tag: table}`) |
+| 3 | GridTools/gt4py#2907 | `feat[next]`: `NeighborConnectivity`, `LocalDimensionIndex`, `check_neighbor_table`, declaration fingerprinting; usable in the DSL; shared local dimensions; ADR 0029 |
+| 4 | GridTools/gt4py#2908 | `feat[next]`: the test tree and docs declare connectivities as classes; iterator-embedded `shift`/`neighbors` accept them; `DimensionIndex(kind=LOCAL)` rejected; two-target `FieldOffset` deprecated |
+| 5 | GridTools/gt4py#2909 | `feat[next]`: backends support connectivities sharing a local dimension (`connectivity_key_over`, DaCe `local_dimension_size`); lifts PR 1's xfails |
+| 6 | GridTools/gt4py#2910 | `feat[next]!`: class-keyed offset providers; `FieldOffset` removed; `as_offset(dim, field)`; migration script |
+| 7 | GridTools/gt4py#2911 | `refactor[next]`: the `ConstListDim` class (from PR 2) becomes `ConstList` with `size=1`, replacing the `_CONST_DIM` aliases by identity checks; `AxisLiteral` drops `kind`; printing IR never imports (`resolve_loaded`) |
+| 8 | GridTools/gt4py#2912 | `refactor[next]`: `MultiDimensionIndex` and typed embedded positions |
+
+Each of PRs 2–8 carries a follow-up commit applying an independent review of
+this note against the code (the "review fixes" commits). The behaviour they
+changed is described above; in outline: `Local` is annotated nowhere, so it
+stays a type for pyright as well as mypy, and `common.local_dimension_of` is
+the accessor for library code (PR 3); adoption and sharing are written
+`Local: TypeAlias = ...`, and the `make_const_list` dimension cannot be adopted
+(PRs 3, 4, 6); a redefined declaration re-owns an adopted local dimension
+(PR 3); `check_offset_provider` runs at every entry point, is memoized per set
+of bound tables and reads the tables only where a program is compiled, and a
+key naming the connectivity rather than the declaration is rejected (PR 6);
+`MultiDimensionIndex` requires a local index and checks it against the primary
+dimension (PR 8); a dimension cannot be staggered twice and staggered classes
+are interned thread-safely (PR 2); pyright runs in the typing nox session
+(PR 3).
+
+### Where the implementation departs from the original proposal
+
+- **No `DimensionBaseIndex`**; `LocalDimensionIndex` subclasses
+  `DimensionIndex`. Generic constructors whose parameter must be a primary
+  dimension (`NeighborConnectivity[Origin, Codomain]`, `Staggered[D]`,
+  `MultiDimensionIndex`) check at runtime that it is not local.
+- **`NeighborConnectivity` is not a `Connectivity`** (Open question 6), so
+  `MultiDimensionIndex` is not the domain index of a declaration.
+- **The IR names a connectivity by its local dimension's tag** (its
+  `offset_tag`), not by the connectivity's own tag, and **internal providers
+  stay keyed by that string**; the public API takes classes (and still
+  accepts dotted tag strings). This made
+  the originally planned "backends resolve through `Local.owner`" step
+  unnecessary — with one string per connectivity, going through `owner`
+  changes nothing.
+- **Shared local dimensions** were not in the proposal and turned out to be
+  needed (ICON4Py's flattened offsets). They reintroduce an offset tag that
+  differs from its local dimension's tag, for which the backends got
+  `connectivity_key_over`.
+- **`Staggered[D]` had to land with the dimension change**, not later, and it
+  is an interning metaclass subscription, not a PEP 695 generic; a narrow
+  `copyreg` hook remains for it.
+- **Codegen mangling** is a prefix escape (`_u`, `_d`, `_l`, `_r`); the
+  proposed "escape `__` then replace `.`" is not injective.
+- **Interactive `__main__`** is handled (in-process compilation), not merely
+  documented.
+- **`ts.OffsetType` and `iterator.runtime.offset` are kept**; providers stay
+  string-keyed below the entry points.
+- **The one-string invariant** (offset tag = local dimension tag = provider
+  key) was pulled forward into the dimension PR: once tags became qualified
+  names, most test-tree local dimensions stopped matching their offsets' tags.
+- **Staging**: the proposal's step 2 bundled the declaration migration, the
+  provider key change and the removals; they had to be separate to stay green
+  (declarations first, class keys last).
+- **Adopting a module-level local dimension** mutates it (owner and counts);
+  the proposal treated adoption as a pure renaming aid.
 
 ## Appendices
 
@@ -639,6 +796,13 @@ they reverse two recorded decisions and change a public-API shape.
   each with `file:line`; per-context tables for embedded, IR, gtfn and DaCe;
   the complete concept inventory (L0–L9); class-hierarchy and name-flow
   diagrams; the two executed experiments.
-- [`typing_probe.py`](connectivities-as-types/typing_probe.py): the mypy /
-  pyright probes behind the `Local` decisions (explicit nested class works;
-  generated `ClassVar` form and `Local[C]` reconciliation do not).
+- [[personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing|Background: dependent typing for mesh connectivities]]:
+  a primer on value-dependent types (Π and Σ types, refinements, evidence,
+  local slots vs. incidences) on a small mesh, and a mapping of each concept
+  onto this design — what is kept statically, what moves to the bind-time
+  check, and what is given up.
+- [`typing_probe.py`](typing_probe.py): the mypy /
+  pyright probes behind the `Local` decisions (explicit nested class works,
+  also when only the local dimension differs; generated `ClassVar` form and
+  `Local[C]` reconciliation do not). Last run with mypy 2.3.1 and pyright
+  1.1.414.
diff --git a/content/personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing.md b/content/personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing.md
new file mode 100644
index 0000000..4cc3f76
--- /dev/null
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing.md
@@ -0,0 +1,318 @@
+---
+title: "Connectivities as types — background: dependent typing for mesh connectivities"
+author: egparedes
+tags: [type-system, type-checking, dependent-types, connectivities, local-dimensions, unstructured, offset-provider, nominal-types, prior-art]
+created: 2026-09-23
+status: draft
+---
+
+> **Appendix** to [[personal/egparedes/connectivities-as-types/connectivities-as-types|Connectivities as types]].
+> Background for reviewers: what a connectivity *would* look like in a
+> language with dependent types, and which parts of that picture the
+> Python-level design keeps statically, which it moves to a bind-time check,
+> and which it gives up. Part 1 is a condensed primer, adapted from the note
+> *Dependent typing for imperative programmers — from graph connectivity to
+> checked sparse computations*; part 2 maps it onto gt4py.
+
+## Why this appendix
+
+The main note makes several choices that look arbitrary in isolation: the
+local dimension is *owned* by a connectivity (`V2E.Local`) rather than being a
+free-standing name; the class `V2E` is a *declaration* that never holds data;
+neighbor counts are optional and taken from the table; a table is checked at
+the program boundary and then trusted. All of them are the Python
+approximation of one idea from type theory: **the type of a local index
+depends on a value** — the mesh, and the element whose neighbors are being
+visited. Python's type system cannot mention values, so the design has to
+decide what to keep of that dependency and where to check the rest.
+
+[[personal/havogt/dependent-local-dimensions/dependent-local-dimensions|Dependent local dimensions]]
+starts from the same observation ("`V2EDim` is a *dependent* dimension", §1)
+and cites Dex's dependent index sets as prior art (§10). This appendix spells
+out the vocabulary both notes lean on.
+
+## Part 1 — A primer
+
+The primer uses C-like pseudocode in which angle brackets accept types *or
+values*, and later arguments may mention earlier ones. Graphs are immutable
+values throughout.
+
+### Running example
+
+A mesh fragment `G` with four vertices and three edges, as a Boolean
+vertex × edge incidence matrix:
+
+```text
+             edge 0  edge 1  edge 2
+vertex 0       true   false   false
+vertex 1       true   true    true
+vertex 2       false  true    false
+vertex 3       false  false   true
+```
+
+Its neighbor lists are `[0]`, `[0, 1, 2]`, `[1]`, `[2]`. The ordinary API
+leaves every interesting condition unstated:
+
+```text
+List<int> neighbors(Graph g, int v);
+double    weight(Graph g, int v, int e);
+```
+
+IDs must be in range, the list must be exact, and `weight` needs an incident
+pair — `(0, 1)` has valid IDs but is not an incidence.
+
+### 1. Put values in types
+
+A **type family** selects a type from a parameter, which may be a value:
+
+```text
+Vector<T, n>    // exactly n elements
+Fin<n>          // a natural number i with 0 <= i < n
+
+type Vert<Graph g> = Fin<g.nV>;
+type Edge<Graph g> = Fin<g.nE>;
+
+double get(Nat n, Vector<double, n> a, Fin<n> i);   // the type of i is the bounds check
+```
+
+The checker reasons symbolically about `n`; it need not know its numeral.
+
+### 2. Let arguments determine types (Π and Σ)
+
+A **dependent function type** (Π type) lets an argument determine later
+argument or result types:
+
+```text
+auto   row(Graph g, Vert<g> v) -> Vector<double, degree(g, v)>;
+double at (Graph g, Vert<g> v, Fin<degree(g, v)> k);
+```
+
+`k` is a **local slot** in `v`'s row, not an edge ID, and its legal range
+changes with `v`. A **dependent pair** (Σ type) packages a value with data
+whose type mentions it:
+
+```text
+struct Row { Nat length; Vector<double, length> data; };
+```
+
+### 3. Refinements: say *exactly* the neighbors
+
+A length-correct `Vector<Edge<g>, degree(g, v)>` still admits `[2]` for vertex
+0. A **refinement** restricts a type by a predicate:
+
+```text
+type NeighborList<Graph g, Vert<g> v> =
+    List<Edge<g>> es where
+        noDuplicates(es) &&
+        forall (Edge<g> e) (contains(es, e) == g.incident(v, e));
+```
+
+— soundness, completeness, uniqueness. Order is extra information: without
+sorting, a row of degree `d` has `d!` valid orderings.
+
+### 4. Proofs are evidence, and can be erased
+
+`Proof<P>` is checked evidence for `P`, not a Boolean. A loop that scans the
+incidence matrix establishes `NeighborList` by an invariant ("the result holds
+exactly the incident edges examined so far"). Evidence is usually erased
+during compilation; computational data that happens to appear in types —
+lengths, offsets, indices — is not.
+
+### 5. Restrict a field to valid incidences
+
+```text
+type IncidentEdge<Graph g, Vert<g> v> = Edge<g> e where g.incident(v, e);
+
+struct Incidence<Graph g> {             // a Σ type: edge's type mentions vertex
+    Vert<g> vertex;
+    IncidentEdge<g, vertex> edge;
+};
+
+type IncidenceField<Graph g> = function(Incidence<g>) -> double;
+```
+
+The field assigns one value per *incidence*: `(0, 0)` and `(1, 0)` may carry
+different weights although both name edge 0. The dependency restricts the
+**domain**; the output is an ordinary `double`.
+
+### 6. Edge IDs vs. local slots: the enumeration
+
+The edges above one vertex (its **fiber**) can be addressed by edge ID or by
+local slot. An exact neighbor list is a **bijection** between the two:
+
+```text
+type NeighborOrder<Graph g> =
+    function(Vert<g> v) -> Bijection<Fin<degree(g, v)>, IncidentEdge<g, v>>;
+```
+
+Once an enumeration is chosen, a field has two equivalent addressings:
+
+| Addressing | Type for a fixed graph `g` | Storage analogy |
+| --- | --- | --- |
+| vertex–edge incidence | `Incidence<g> -> double` | coordinate-based, like COO |
+| vertex–local slot | `(v : Vert<g>) -> Fin<degree(g, v)> -> double` | row-and-slot, like CSR |
+
+Degrees alone define the legal slots but not *which* edge sits in each;
+**reordering the neighbors requires reordering every slot-addressed value
+consistently.** A uniform degree reduces the ragged shape to a rectangular
+array — the edge correspondence still matters. With `nbr : NeighborOrder<g>`
+and `field : IncidenceField<g>`, a neighbor reduction is:
+
+```text
+double sumAtVertex(Vert<g> v) {
+    double total = 0.0;
+    for (Fin<degree(g, v)> k : range(degree(g, v)))
+        total += field(Incidence<g>{v, nbr(v).forward(k)});
+    return total;
+}
+```
+
+### 7. Types indexed by a graph do not identify the graph
+
+Indexing a type by `g` does **not** prove "same type ⇒ same graph": an alias
+may ignore its index, and `Fin<g.nV>` distinguishes bounds, not two meshes
+with the same vertex count. Preventing cross-mesh ID mixing needs an
+**identity-preserving wrapper, or brand**.
+
+### 8. Validate at boundaries, then reuse the evidence
+
+Runtime input acquires a dependent type through a checked decision
+(`makeIncidence(g, v, e) -> Option<Incidence<g>>`). A graph loaded at run time
+travels with its checked operations:
+
+```text
+type NeighborsFor<Graph g> = function(Vert<g> v) -> NeighborList<g, v>;
+
+struct GraphPackage {
+    Graph graph;
+    NeighborsFor<graph> neighbors;
+    IncidenceField<graph> field;
+};
+```
+
+The loader proves the contracts once; consumers reuse them. Evidence is valid
+only for the graph it describes — a mutated or different graph needs a new
+check. The trade-off is proof work at construction points in exchange for
+guarantees everywhere downstream; validated constructors and branded ID
+wrappers offer part of this discipline in ordinary languages.
+
+## Part 2 — What gt4py can keep of it
+
+### The dictionary
+
+| Dependent-typing concept | gt4py today (v1.2.2) | This design |
+| --- | --- | --- |
+| `Vert<g>` — index type of a mesh entity | `Dimension("Vertex")`, identity by `(value, kind)` | the class `V(DimensionIndex)`; identity is the class (a **brand**, §7) |
+| `Fin<degree(g, v)>` — local slot, depends on `g` *and* `v` | `V2EDim = Dimension("V2E", LOCAL)`, a free name | `V2E.Local`: depends on the **declaration** `V2E` (nominally, by nesting), not on `g` or `v` |
+| `degree(g, v)` bounded by the padded row length | `max_neighbors` on the table's type | `max_neighbors` / `min_neighbors`: optional class keywords stored on `V2E.Local`, else taken from the table |
+| `Option`-valued slots of a padded ragged row | `skip_value` (−1) in the table | same; if `min_neighbors` is declared, skip values must be present iff `min_neighbors < max_neighbors` |
+| `NeighborOrder<g>` — the enumeration | a `NeighborTable` / `NdArrayConnectivityField` | unchanged: the table *is* the enumeration |
+| `(v : Vert<g>) -> Fin<degree(g, v)> -> double` — slot-addressed field | `Field[Dims[V, V2EDim], float]` | `Field[Dims[V, V2E.Local], float]` |
+| `Incidence<g>` — a Σ-typed position | an untyped `{"Vertex": 3, "V2E": 2}` dict | `MultiDimensionIndex(V(3), V2E.Local(2))`; checked at run time that `V2E.Local` indexes the neighbors of a `V` (the dependency of the second component on the first, but not on the value `3`) |
+| the graph value `g` in the signature | a string-keyed `offset_provider` | a bound connectivity: `{V2E: table}` binds the class to one table per call |
+| `GraphPackage` — graph plus checked operations | — | the provider after `check_offset_provider` (and, in [[personal/havogt/mesh-and-first-class-halos/mesh-and-first-class-halos\|the mesh proposal]], a Mesh object) |
+| validate at the boundary, reuse evidence | no check; errors surface as `KeyError` or wrong results | `check_offset_provider` at every entry point, remembered per set of bound tables, then trusted by lowering and backends |
+
+### What is kept statically
+
+- **Which index space a local slot belongs to.** The essential dependency of
+  §2 is that `k` in `at(g, v, k)` is not an arbitrary integer but a slot of
+  *this* neighbor relation. `V2E.Local` keeps that part: a field over
+  `(V, V2E.Local)` and one over `(V, V2V.Local)` are different types for mypy
+  and pyright, and `neighbor_sum(..., axis=V2E.Local)` names the relation it
+  reduces over. This is why the design insists on a *nested, explicitly
+  declared* `Local` — it is the only spelling that is a real, distinct type for
+  both checkers (probes P1b and P2 in
+  [`typing_probe.py`](typing_probe.py)). A connectivity that *shares* or
+  *adopts* a local dimension spells it `Local: TypeAlias = C2E.Local`, so
+  `C2CE.Local` and `C2E.Local` are the same type — one slot type, two
+  relations enumerating it.
+- **A brand per mesh entity (§7).** Nominal identity makes two independently
+  declared `Vertex` classes distinct types, statically and at run time. The
+  `(name, kind)` equality of [[shared/dimensions-as-types|dimensions as types]]
+  is the unbranded `Fin<g.nV>` of §7: equal names, interchangeable indices.
+  Nominal identity is not sufficient to separate two *meshes* that share the
+  same declarations, though — see below.
+
+### What moves to a bind-time check
+
+Python has no value-indexed types, so the dependency on the table value `g`
+cannot be expressed. The design splits the connectivity type the way §4
+splits data from evidence:
+
+- The **class** `V2E` is the static, erasable part: `Origin`, `Codomain`,
+  `Local` and, optionally, the declared counts. It is what the frontend and the
+  type checker see.
+- The **table** is the value `g`. Binding happens per call through the
+  provider (`{V2E: table}`), and `check_neighbor_table` is the "checked
+  decision" of §8: it establishes that the table's domain is `(Origin, Local)`,
+  its codomain `Codomain`, its dtype integral, its width equal to a declared
+  `max_neighbors` and not below a declared `min_neighbors`, and — if
+  `min_neighbors` is declared — its skip values consistent with it.
+- **Undeclared counts are taken from the table** when a variant is compiled.
+  In §4's terms the counts are computational data that appear in types and
+  are *not* erased; they are specialised on per compiled variant rather than
+  fixed in the source. The main note's *Binding model* explains why a
+  static-only count would bind DSL source to one mesh family.
+
+### What is given up (and why that is acceptable)
+
+- **Soundness and completeness of the table (§3).** Nothing checks that a
+  table lists *exactly* the incident entities, without duplicates. That is a
+  property of the mesh generator, and gt4py never has the incidence relation
+  independently of the table to check it against.
+- **Per-element ragged degree.** `Fin<degree(g, v)>` becomes
+  `Fin<max_neighbors>` plus skip values, i.e. the padded, rectangular
+  representation of §6. `min_neighbors == max_neighbors` is exactly the
+  uniform-degree case, which is why it is equivalent to "no skip values".
+- **Same type ⇒ same table (§7).** `V2E` does not identify a mesh. Two
+  different tables bound to `V2E` in two calls give two different, both
+  well-typed, programs. This is deliberate — it is what lets one DSL source run
+  on several meshes — and the one-table-per-class-per-call dict keeps it from
+  becoming ambiguous *within* a call. Guarding against mixing meshes across
+  calls (e.g. a field computed on mesh A consumed on mesh B) is out of scope;
+  it would need a mesh-level brand, which is where
+  [[personal/havogt/mesh-and-first-class-halos/mesh-and-first-class-halos|a mesh concept]]
+  could take over.
+
+### The enumeration consequence: shared local dimensions
+
+§6's warning — slot-addressed values are only meaningful relative to one
+enumeration — is the reason for the one genuinely new rule the implementation
+added. `C2CE` (cell → flattened (cell, edge-of-cell) pairs) *shares*
+`C2E.Local` so that its results combine with `C2E`-shaped sparse fields.
+Sharing a slot type across two connectivities is only sound if both tables
+enumerate each cell's fiber in the same order and pad it in the same places.
+The type checker cannot see this; the bind-time check (`check_offset_provider`)
+requires tables over one shared local dimension to have the same width and
+skip-value presence and — where a program is compiled — skip values at the
+same positions, and reductions over the shared axis take that structure from any
+bound table over it. Note what this does *not* check: that the two tables list
+each cell's neighbors in the same *order* — §6's bijection — which is again a
+property of the mesh generator.
+
+### Evidence lifetime
+
+§8's caveat — evidence is valid only for the graph it describes — applies to
+the check's placement. `check_offset_provider` runs at every entry point, and
+its result is remembered per set of bound tables, keyed by their *identity*:
+binding a different table re-runs the check, re-binding the same object reuses
+the evidence for the cost of one hash. The data-dependent part (comparing skip
+positions of tables over a shared local dimension) runs only where a program
+is compiled, not on the call path. Two gaps remain, both the kind §8 names for
+mutable data: a table modified in place after the check keeps its old
+evidence, and — as with the compiled-program cache, which is keyed the same
+way — a freed table replaced by a new one at the same address could in
+principle reuse the old evidence.
+
+## Further reading
+
+- [[personal/havogt/dependent-local-dimensions/dependent-local-dimensions|Dependent local dimensions and connectivity chains]]
+  — the chain/forest generalisation and its prior-art section (Dex).
+- A. Paszke et al., *Getting to the Point: Index Sets and
+  Parallelism-Preserving Autodiff for Pointful Array Programming*, ICFP 2021 —
+  Dex's typed index sets, the closest array-language analogue of `Fin<n>`
+  dimensions.
+- M. Noonan, *Ghosts of Departed Proofs (Functional Pearl)*, Haskell
+  Symposium 2018 — carrying checked facts as phantom/brand types in a language
+  without full dependent types, the technique `V2E.Local` is an instance of.
diff --git a/content/personal/egparedes/connectivities-as-types/connectivities-as-types_research.md b/content/personal/egparedes/connectivities-as-types/connectivities-as-types_research.md
index 8f3ce11..0d6179f 100644
--- a/content/personal/egparedes/connectivities-as-types/connectivities-as-types_research.md
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types_research.md
@@ -12,8 +12,10 @@ status: draft
 > `gt4py.next`, across the embedded, IR and backend contexts. It documents the
 > implementation as it is; the proposal it supports is in the main note.
 
-Line references are against gt4py `main` at `b3c53fa7e` (v1.2.2, 2026-09-03);
-paths are relative to `src/gt4py/next/` unless they start with `tests/`.
+Line references are against gt4py `main` at `b3c53fa7e` (v1.2.2, 2026-09-03),
+i.e. the tree *before* the implementation (see the main note's Implementation
+section), so this catalogue is a historical record. Paths
+are relative to `src/gt4py/next/` unless they start with `tests/`.
 
 Related gt4py records:
 [ADR 0019 Connectivities](https://github.com/GridTools/gt4py/blob/main/docs/development/ADRs/next/0019-Connectivities.md),
diff --git a/content/personal/egparedes/connectivities-as-types/typing_probe.py b/content/personal/egparedes/connectivities-as-types/typing_probe.py
index 379be6b..1bf5ff1 100644
--- a/content/personal/egparedes/connectivities-as-types/typing_probe.py
+++ b/content/personal/egparedes/connectivities-as-types/typing_probe.py
@@ -2,11 +2,17 @@
 
 Run with `mypy --strict --python-version 3.12` and `pyright --pythonversion 3.12`.
 Expected: P1 accepts the explicit nested `Local` and rejects the cross-connectivity
-mismatch on line `p1(Field[E, E_V2V.Local]())`; P2 rejects the generated `ClassVar` form
+mismatch on line `p1(Field[E, E_V2V.Local]())`; P1b rejects a mismatch in the local
+dimension alone (`Field[V, E_V2V.Local]`), so the nested classes are distinct types
+in their own right; P2 rejects the generated `ClassVar` form
 as "not valid as a type"; P3 rejects each spelling where the other is expected.
 pyright additionally reports "Class definition for V_E2E depends on itself" on the
 string forward reference in the base subscription, which is why the proposal does
 not pass `Local` through the bases.
+
+`StaticMultiLevelMapping` is scaffolding from an early draft that stored the table
+on the class (rejected, see "Data on the class" in the main note); only the probes
+at the end matter. Last run: mypy 2.3.1 and pyright 1.1.414 (2026-09-23).
 """
 
 from __future__ import annotations
@@ -96,6 +102,7 @@ class Field[*Ds]: ...
 def p1(a: Field[V, V_E2E.Local]) -> None: ...
 p1(Field[V, V_E2E.Local]())
 p1(Field[E, E_V2V.Local]())   # expected error: distinct locals
+p1(Field[V, E_V2V.Local]())   # P1b, expected error: only the local dimension differs
 
 # P2: generated Local (ClassVar on the base), as the proposal's default form
 class Base2:
@@ -113,3 +120,4 @@ def p3a(a: Field[V, V_E2E.Local]) -> None: ...
 def p3b(a: Field[V, Local[V_E2E]]) -> None: ...
 p3a(Field[V, Local[V_E2E]]())    # same type for the checker?
 p3b(Field[V, V_E2E.Local]())
+