From ab152a8134e17d396eecc35fe5015c77e28f39bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Enrique=20Gonz=C3=A1lez=20Paredes?= <enriqueg@cscs.ch>
Date: Tue, 22 Sep 2026 07:21:34 +0200
Subject: [PATCH 1/4] =?UTF-8?q?personal/egparedes:=20connectivities=20as?=
 =?UTF-8?q?=20types=20=E2=80=94=20update=20to=20the=20implementation?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The design as implemented in the GridTools/gt4py stack #2898, #2899,
#2907-#2912 (ADRs 0028, 0029): corrected concepts and sketch, binding model,
shared local dimensions, answered open questions, the PR stack, and where the
implementation departs from the original proposal.
---
 content/index.md                              |   2 +-
 .../connectivities-as-types.md                | 538 +++++++++---------
 .../connectivities-as-types_research.md       |   2 +-
 3 files changed, 285 insertions(+), 257 deletions(-)

diff --git a/content/index.md b/content/index.md
index 5e7a122..7d7d5e4 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, 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..d711404 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, metaclass, serialization, fingerprint, staggering, migration, adr, tech-debt, shared-local-dimensions, implemented]
 created: 2026-09-17
+updated: 2026-09-22
 status: draft
 ---
 
@@ -23,10 +24,18 @@ status: draft
 > program(a, out=out, offset_provider={V2E: v2e_table})
 > ```
 >
-> `FieldOffset`, `ts.OffsetType`, the string-keyed `OffsetProvider` 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.
+> `FieldOffset`, the string-keyed provider *API* 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.
+
+> **Implementation status (2026-09-22).** Implemented as the stacked
+> GridTools/gt4py PRs listed in [Implementation](#implementation), with
+> ADR 0028 (dimensions as nominal types) and ADR 0029 (connectivities as
+> types). The sections below describe the design **as implemented**; 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. Derived from a full audit of the gt4py tree
 > at `b3c53fa7e` (v1.2.2, 2026-09-03); every `file:line` reference was
@@ -139,97 +148,106 @@ 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** with a fixed `size`; carries `max_neighbors` / `min_neighbors` when declared | `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 | untyped position dicts keyed by name strings |
+
+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
+    max_neighbors: ClassVar[int | None]
+    min_neighbors: ClassVar[int | None]        # min == max  <=>  no skip values
+    def __init_subclass__(cls, *, size: int | None = None): ...
 
 
-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"
+    def __call__(cls, *a, **kw) -> NoReturn: ...        # no instances
+    def __getitem__(cls, item): ...            # V2E[1] in embedded; NC[V, E] forwarded
+    def __gt_type__(cls) -> ts.OffsetType: ...  # Codomain -> (Origin, Local), tag=offset_tag
 
 
 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): ...
+
 
-    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 = 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
@@ -251,98 +269,82 @@ 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 compile runner detects a job that
+   references such a class and **compiles it in the calling process** 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; a connectivity declaration additionally by its dimensions 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` — with inverse
+   `from_codegen_name`, used by gtfn, DaCe and the roundtrip backend. The first
+   draft's "escape `__` then replace `.`" was **not** injective (`".."` and
+   `"_"` collide); the prefix escape was verified exhaustively.
+6. **Staggering came into scope, and earlier than planned.**
+   `Staggered[D]` is an interning metaclass subscription producing a real
+   class (a PEP 695 generic would give a `typing` alias, which fails
+   `issubclass` and eve's `type[...]` validation). 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.
 
 ### 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`,
+- The class `V2E` is a **declaration**. 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.
+  is what compilation sees. Declared counts are a constraint on the table;
+  undeclared ones are simply taken from the table (its
+  `NeighborConnectivityType`, which is part of the compile-cache key as
+  before). Nothing is written 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.** Every program entry point
+  (`Program.__call__`, `FieldOperator.__call__`, `compile`,
+  `CompilationOptions.connectivities`, `embedded.context.update`, the
+  iterator `fendef`, DaCe `get_sdfg_conn_args`) rewrites the provider to the
+  form the IR uses, keyed by `offset_tag`. Lowering, the backends and the
+  compiled-program cache keep seeing tag-keyed providers — like hand-written
+  IR — so the ~19 direct provider accesses in the backends did not change. A
+  bare string key such as `"V2E"` is rejected as the removed spelling.
+- **Validated once per compiled variant** (and on embedded calls):
+  `check_neighbor_table` checks the domain `(Origin, Local)`, the codomain,
+  an integral dtype, the declared counts, and that skip values are present
+  iff `min_neighbors < max_neighbors`. Tables over one shared local dimension
+  must also have the same neighbor structure (skip values at the same
+  positions). Not on every call: building a table's type is too slow for the
+  call path.
+- The class never holds data; the table crosses process boundaries as it did.
 
 ### The local dimension
 
@@ -362,8 +364,25 @@ 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`. The base declares `Local: ClassVar[type[LocalDimensionIndex]]` as an
+  *annotation only* (a real nested class on the base is an incompatible
+  override for pyright), and `__init_subclass__` reads `cls.Local` after the
+  class body. The annotation gives library code `conn.Local` as a *value* of
+  type `type[LocalDimensionIndex]`; it does not make `conn.Local` usable as an
+  *annotation* for a generic `conn`, which no checker allows — generic code
+  names the local dimension through a `TypeVar` bound to
+  `LocalDimensionIndex`.
+- A declaration can instead **adopt** a module-level local dimension
+  (`Local = V2EDim`); it keeps its own tag. This is also how the migration
+  script rewrites existing `FieldOffset`s without renaming anything.
+- A connectivity can **share** another one's local dimension
+  (`class C2CE(NeighborConnectivity[C, CE]): Local = 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 `C2E`; the sharer must have the same origin, its counts are 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 if bound,
+  else the sharer with the smallest tag).
 - `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
@@ -377,68 +396,66 @@ tables assign different neighbors to the same origin element. The model:
   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 the owner-less `common.ConstList(LocalDimensionIndex, size=1)`,
+  one class used by iterator embedded and the DaCe lowering with identity
+  checks.
 - `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.
 
 ### `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]`).
+- `*Ls` is unconstrained because `TypeVarTuple` cannot carry a bound; the
+  constructor checks the shape at runtime.
+- 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__`), carrying `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` | `codegen_name(tag)`; lookups through `connectivity_key_over` |
+| DaCe | ~10 `offset_type.value` lookups; `Dimension(offset, LOCAL)` synthesized | `codegen_name` for array/symbol names; `connectivity_key_over`; no synthesis |
+| roundtrip backend | emits `gtx.Dimension("<name>")` / `offset("<tag>")` as source text | emits `gtx.resolve("<tag>")` bound to mangled identifiers |
+| Provider | `Mapping[str, NeighborTable]` | public: `{V2E: table}`; 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
+`FieldOffset` (both forms) and its export; the string-keyed provider *API*
+(bare names are rejected); `dimension(tag, kind)`, the interning registry and
+the `copyreg` hook of #2844 (only a narrow one for `Staggered[D]` remains); the
+`_Staggered` prefix and its string sniffing; `_CONST_DIM` as a magic name;
+the stored `AxisLiteral.kind`; `SparseTag`; `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", ...)`.
 
-**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.
+**Kept**, contrary to the original note: `ts.OffsetType` (it now types only
+declarations 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]`
 
@@ -548,88 +565,99 @@ 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:**
+**Open questions, and how the implementation answered them:**
 
-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
+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]]
-   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.
+   (`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.** Metaclass discovery 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: jobs referencing a class of an
+   interactive `__main__` are compiled in the calling process.
+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. A dry run over ICON4Py `main`
+   rewrites `dimension.py` and ~50 stencil modules and leaves 79 string
+   provider keys, 30 removable Cartesian provider entries and 14
+   `isinstance(..., Dimension)` checks to do by hand. Declaring counts is left
+   to ICON4Py.
+5. **Duplicate declarations.** No warning was added.
+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 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.
+
+| # | PR | What |
+| --- | --- | --- |
+| 1 | GridTools/gt4py#2898 | `fix[next]`: lower unstructured shifts with the offset's own tag (the N2 leak), regression matrix for the four names |
+| 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; the one-string invariant pulled forward (`FieldOffset(V2EDim.tag, ...)`, `{V2EDim.tag: table}`) |
+| 3 | GridTools/gt4py#2907 | `feat[next]`: `NeighborConnectivity`, `LocalDimensionIndex`, `check_neighbor_table`; usable in the DSL; shared local dimensions; ADR 0029 |
+| 4 | GridTools/gt4py#2908 | `feat[next]`: the test tree and docs declare connectivities as classes; `DimensionIndex(kind=LOCAL)` rejected; two-target `FieldOffset` deprecated |
+| 5 | GridTools/gt4py#2909 | `feat[next]`: backends support connectivities sharing a local dimension (`connectivity_key_over`) |
+| 6 | GridTools/gt4py#2910 | `feat[next]!`: class-keyed offset providers; `FieldOffset` removed; `as_offset(dim, field)`; migration script |
+| 7 | GridTools/gt4py#2911 | `refactor[next]`: `ConstList` replaces `_CONST_DIM`; `AxisLiteral` drops `kind` |
+| 8 | GridTools/gt4py#2912 | `refactor[next]`: `MultiDimensionIndex` and typed embedded positions |
+
+### 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 it at runtime.
+- **`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**; only the public API takes classes. 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).
 
 ## Appendices
 
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..68315b7 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,7 +12,7 @@ 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);
+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); this catalogue is a historical record;
 paths are relative to `src/gt4py/next/` unless they start with `tests/`.
 
 Related gt4py records:

From 29ff81d6b05da0782208f3a8104d1a4395a48976 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Enrique=20Gonz=C3=A1lez=20Paredes?= <enriqueg@cscs.ch>
Date: Wed, 23 Sep 2026 15:33:57 +0200
Subject: [PATCH 2/4] =?UTF-8?q?personal/egparedes:=20connectivities=20as?=
 =?UTF-8?q?=20types=20=E2=80=94=20align=20with=20the=20implementation,=20a?=
 =?UTF-8?q?dd=20dependent-typing=20background?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Checked the note against the top of the implementation stack
(connectivities-as-types-8-typed-positions at 65fa529b6) and corrected it:
the IR names a connectivity by its local dimension's tag; only bare-name
provider keys are rejected (dotted tags are accepted, and the iterator hooks
normalize non-strictly); the exact normalizing entry points and when the
table check runs (per compiled variant, keyed by table identity, and on
embedded calls); what check_neighbor_table checks; counts live on V2E.Local;
adoption makes the adopter the owner (first-come); the MultiDimensionIndex
runtime check; per-layer, deletion and PR-table details; migration dry-run
counts against current ICON4Py.

Add a background appendix on dependent typing for mesh connectivities: a
condensed primer (Pi/Sigma types, refinements, evidence, local slots vs
incidences) and a mapping of what the design keeps statically, checks at
bind time, and gives up.

typing_probe.py gains probe P1b, which isolates the claim that nested Locals
are distinct types. Fix wikilinks to havogt's notes and the typing_probe
links, and add dependent-types to the index keywords.
---
 content/index.md                              |   2 +-
 .../connectivities-as-types.md                | 341 +++++++++++-------
 ...onnectivities-as-types_dependent-typing.md | 316 ++++++++++++++++
 .../connectivities-as-types_research.md       |   6 +-
 .../connectivities-as-types/typing_probe.py   |  10 +-
 5 files changed, 547 insertions(+), 128 deletions(-)
 create mode 100644 content/personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing.md

diff --git a/content/index.md b/content/index.md
index 7d7d5e4..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, shared-local-dimensions, implemented
+- [[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 d711404..15e2506 100644
--- a/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
@@ -1,9 +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, shared-local-dimensions, implemented]
+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-22
+updated: 2026-09-23
 status: draft
 ---
 
@@ -14,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]):
@@ -24,28 +25,35 @@ status: draft
 > program(a, out=out, offset_provider={V2E: v2e_table})
 > ```
 >
-> `FieldOffset`, the string-keyed provider *API* 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.
+> `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.
 
-> **Implementation status (2026-09-22).** Implemented as the stacked
+> **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). The sections below describe the design **as implemented**; where
-> the implementation had to depart from the original proposal, the text was
-> corrected and the departure is listed in
+> 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` at `65fa529b6`, 2026-09-22);
+> 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. 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
+> **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
@@ -53,11 +61,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.
@@ -153,9 +161,9 @@ what is one idea — *a mapping between two index spaces, plus a name for it*.
 | Concept | Role | Replaces |
 | --- | --- | --- |
 | `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** with a fixed `size`; carries `max_neighbors` / `min_neighbors` when declared | `Dimension(..., kind=LOCAL)`, `_CONST_DIM` (now `ConstList`) |
+| `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 | untyped position dicts keyed by name strings |
+| `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
@@ -189,10 +197,10 @@ type Dimension = type[DimensionIndex]          # PEP 695: `Dimension("I")` is no
 
 
 class LocalDimensionIndex(DimensionIndex):     # kind is LOCAL; `kind=LOCAL` elsewhere is an error
-    owner: ClassVar[type[NeighborConnectivity] | None]   # None: owner-less
-    max_neighbors: ClassVar[int | None]
+    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): ...
+    def __init_subclass__(cls, *, size: int | None = None): ...   # size: max = min = size
 
 
 class MultiDimensionIndex[D: DimensionIndex, *Ls](tuple[D, *Ls]): ...   # shape checked at runtime
@@ -204,9 +212,12 @@ Staggered[KDim]                                # an interned, real dimension cla
 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] in embedded; NC[V, E] forwarded
+    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](
@@ -214,6 +225,7 @@ class NeighborConnectivity[Origin: DimensionIndex, Codomain: DimensionIndex](
 ):
     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 check_neighbor_table(connectivity, table_or_type) -> None: ...   # A6–A8 as one check
@@ -253,13 +265,15 @@ 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,
@@ -282,24 +296,30 @@ concepts.* The consequences, stated as rules:
    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 compile runner detects a job that
-   references such a class and **compiles it in the calling process** instead
-   of failing in a spawn worker.
+   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; a connectivity declaration additionally by its dimensions and
-   counts, so a redefinition under the same name does not reuse artifacts.
+   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` — with inverse
-   `from_codegen_name`, used by gtfn, DaCe and the roundtrip backend. The first
+   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 was verified exhaustively.
+   `"_"` 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 (a PEP 695 generic would give a `typing` alias, which fails
-   `issubclass` and eve's `type[...]` validation). It had to land with the
+   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
@@ -307,19 +327,22 @@ concepts.* The consequences, stated as rules:
    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.
+   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 **declaration**. Its static part — `Origin`,
-  `Codomain`, `Local`, and *optionally* `max_neighbors` / `min_neighbors` —
-  is what compilation sees. Declared counts are a constraint on the table;
-  undeclared ones are simply taken from the table (its
-  `NeighborConnectivityType`, which is part of the compile-cache key as
-  before). Nothing is written back to the class.
+- 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` sizes
   `V2E` from the atlas mesh), and skip-value presence is
@@ -329,33 +352,62 @@ tables assign different neighbors to the same origin element. The model:
 - 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.
-- **Normalized at the entry points.** Every program entry point
-  (`Program.__call__`, `FieldOperator.__call__`, `compile`,
-  `CompilationOptions.connectivities`, `embedded.context.update`, the
-  iterator `fendef`, DaCe `get_sdfg_conn_args`) rewrites the provider to the
-  form the IR uses, keyed by `offset_tag`. Lowering, the backends and the
+- **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`,
+  `CompilationOptions.connectivities` and DaCe `get_sdfg_conn_args`, and
+  *non-strictly* by `embedded.context.update` and the iterator `fendef`.
+  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 ~19 direct provider accesses in the backends did not change. A
-  bare string key such as `"V2E"` is rejected as the removed spelling.
-- **Validated once per compiled variant** (and on embedded calls):
-  `check_neighbor_table` checks the domain `(Origin, Local)`, the codomain,
-  an integral dtype, the declared counts, and that skip values are present
-  iff `min_neighbors < max_neighbors`. Tables over one shared local dimension
-  must also have the same neighbor structure (skip values at the same
-  positions). Not on every call: building a table's type is too slow for the
-  call path.
+  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 when a compiled
+  variant is created (variants are keyed by the *identity* of the bound
+  tables, so a new table object means a new variant and a new check) and on
+  every embedded `Program` / `FieldOperator` call; not on compiled calls,
+  because building a table's type is too slow for that 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, for concrete tables, on the skip positions.
+  The iterator `fendef`, `FieldOperatorFromFoast` and DaCe orchestration via
+  `CompilationOptions.connectivities` are not validated.
 - 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
@@ -373,23 +425,34 @@ tables assign different neighbors to the same origin element. The model:
   names the local dimension through a `TypeVar` bound to
   `LocalDimensionIndex`.
 - A declaration can instead **adopt** a module-level local dimension
-  (`Local = V2EDim`); it keeps its own tag. This is also how the migration
-  script rewrites existing `FieldOffset`s without renaming anything.
+  (`Local = 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 connectivity can **share** another one's local dimension
   (`class C2CE(NeighborConnectivity[C, CE]): Local = 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 `C2E`; the sharer must have the same origin, its counts are 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 if bound,
-  else the sharer with the smallest tag).
+  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).
+- **In annotations, name the local dimension by its declaring class.** An
+  adopted or shared `Local` is a plain class attribute assignment:
+  `C2CE.Local` works as a *value* (`axis=C2CE.Local`), but annotations should
+  write `Field[Dims[C, C2E.Local], ...]` or `Field[Dims[V, V2EDim], ...]`.
 - `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.
@@ -399,20 +462,25 @@ tables assign different neighbors to the same origin element. The model:
   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 the owner-less `common.ConstList(LocalDimensionIndex, size=1)`,
-  one class used by iterator embedded and the DaCe lowering with identity
-  checks.
+- `_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. (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`
 
 - `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]`).
+  field or a table directly (`v2e_table[position]`, a 0-d field), and compares,
+  hashes and pickles like the plain tuple. It is a user-facing typed index;
+  nothing in the toolchain requires it.
 - `*Ls` is unconstrained because `TypeVarTuple` cannot carry a bound; the
-  constructor checks the shape at runtime.
+  constructor checks the *kinds* of the components at runtime (one non-local
+  index, then local indices), not that the local dimensions belong to the
+  primary one: `MultiDimensionIndex(Edge(1), V2E.Local(1))` is accepted.
 - 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
@@ -426,30 +494,33 @@ tables assign different neighbors to the same origin element. The model:
 | Layer | Before | As implemented |
 | --- | --- | --- |
 | Frontend declaration | `Dimension(LOCAL)` + `FieldOffset` + provider key | one class |
-| Frontend types | `ts.OffsetType(source, target)`, tag dropped | `ts.OffsetType` produced by the class (`__gt_type__`), carrying `offset_tag`; `V2E.Local` in DSL code types as the local dimension |
+| 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)` | 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` | `codegen_name(tag)`; lookups through `connectivity_key_over` |
-| DaCe | ~10 `offset_type.value` lookups; `Dimension(offset, LOCAL)` synthesized | `codegen_name` for array/symbol names; `connectivity_key_over`; no synthesis |
-| roundtrip backend | emits `gtx.Dimension("<name>")` / `offset("<tag>")` as source text | emits `gtx.resolve("<tag>")` bound to mangled identifiers |
-| Provider | `Mapping[str, NeighborTable]` | public: `{V2E: table}`; internal: keyed by `offset_tag`, normalized at the entry points; no deprecation window (a migration script for ICON4Py instead) |
+| 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` (both forms) and its export; the string-keyed provider *API*
-(bare names are rejected); `dimension(tag, kind)`, the interning registry and
-the `copyreg` hook of #2844 (only a narrow one for `Staggered[D]` remains); the
-`_Staggered` prefix and its string sniffing; `_CONST_DIM` as a magic name;
-the stored `AxisLiteral.kind`; `SparseTag`; `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", ...)`.
-
-**Kept**, contrary to the original note: `ts.OffsetType` (it now types only
-declarations and `as_offset`; renaming it to `ConnectivityType` would be churn
-without a user-visible gain), `iterator.runtime.offset("...")` (the
+`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.
 
@@ -459,12 +530,12 @@ 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
@@ -521,7 +592,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]`.
@@ -557,7 +628,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
@@ -580,25 +651,35 @@ sparse storage treatment, changing ICON4Py's layout for `LsqUnkDim` fields.
 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]]
+   [[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.** Metaclass discovery 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: jobs referencing a class of an
-   interactive `__main__` are compiled in the calling process.
+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. A dry run over ICON4Py `main`
-   rewrites `dimension.py` and ~50 stencil modules and leaves 79 string
-   provider keys, 30 removable Cartesian provider entries and 14
-   `isinstance(..., Dimension)` checks to do by hand. Declaring counts is left
-   to ICON4Py.
-5. **Duplicate declarations.** No warning was added.
+   what it cannot decide from the source. The GridTools/gt4py#2910
+   description reports a dry run that rewrites `dimension.py` and 52 stencil
+   modules and leaves 79 provider-key sites and 14
+   `isinstance(..., Dimension)` checks to do by hand. These counts depend on
+   the ICON4Py revision and do not reproduce on current `main`: a re-run on
+   ICON4Py `89b4967` (2026-09-21), after ICON4Py had already dropped
+   `Koff[1]`, rewrites 5 files and reports 46 connectivity provider keys, 2
+   Cartesian provider entries and 5 `isinstance` checks. 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.
@@ -610,19 +691,21 @@ sparse storage treatment, changing ICON4Py's layout for `LsqUnkDim` fields.
 
 ## Implementation
 
-A stack of GridTools/gt4py PRs, each green 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.
+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), regression matrix for the four names |
-| 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; the one-string invariant pulled forward (`FieldOffset(V2EDim.tag, ...)`, `{V2EDim.tag: table}`) |
-| 3 | GridTools/gt4py#2907 | `feat[next]`: `NeighborConnectivity`, `LocalDimensionIndex`, `check_neighbor_table`; usable in the DSL; shared local dimensions; ADR 0029 |
-| 4 | GridTools/gt4py#2908 | `feat[next]`: the test tree and docs declare connectivities as classes; `DimensionIndex(kind=LOCAL)` rejected; two-target `FieldOffset` deprecated |
-| 5 | GridTools/gt4py#2909 | `feat[next]`: backends support connectivities sharing a local dimension (`connectivity_key_over`) |
+| 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]`: `ConstList` replaces `_CONST_DIM`; `AxisLiteral` drops `kind` |
+| 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 |
 
 ### Where the implementation departs from the original proposal
@@ -630,12 +713,13 @@ parts of #2844 compatible with type identity.
 - **No `DimensionBaseIndex`**; `LocalDimensionIndex` subclasses
   `DimensionIndex`. Generic constructors whose parameter must be a primary
   dimension (`NeighborConnectivity[Origin, Codomain]`, `Staggered[D]`,
-  `MultiDimensionIndex`) check it at runtime.
+  `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**; only the public API takes classes. This made
+  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.
@@ -658,6 +742,8 @@ parts of #2844 compatible with type identity.
 - **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
 
@@ -667,6 +753,13 @@ parts of #2844 compatible with type identity.
   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..853705f
--- /dev/null
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types_dependent-typing.md
@@ -0,0 +1,316 @@
+---
+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))`; component kinds checked at run time, not that `V2E.Local` belongs to `V` |
+| 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` when a compiled variant is created and on embedded calls, 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 exposes it as a plain attribute, so annotations
+  name the declaring class (`C2E.Local`, not `C2CE.Local`).
+- **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, for concrete tables, 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. For compiled backends, `check_offset_provider` runs when
+a compiled variant is created, not on every call, because building a table's
+type is too slow for the call path; variants are keyed by the *identity* of
+the bound table objects, so binding a different table creates a new variant
+and re-runs the check, while re-binding the same object reuses the evidence.
+The remaining gap is the one §8 names for mutable data: a table modified in
+place after the check keeps its old evidence. Embedded calls re-check every
+time. Some entry points (the iterator-level `fendef`, DaCe orchestration) do
+not run the check at all — evidence that is never established.
+
+## 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 68315b7..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), i.e. the tree *before* the implementation (see the main note's Implementation section); this catalogue is a historical record;
-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]())
+

From cc9a83e883b00dd38f446e9817c4d7e4a4f77a58 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Enrique=20Gonz=C3=A1lez=20Paredes?= <enriqueg@cscs.ch>
Date: Wed, 23 Sep 2026 16:40:12 +0200
Subject: [PATCH 3/4] =?UTF-8?q?personal/egparedes:=20connectivities=20as?=
 =?UTF-8?q?=20types=20=E2=80=94=20fold=20in=20the=20review=20fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Aligns the note with the follow-up commits on PRs 2-8: `Local` annotated
nowhere and read through `local_dimension_of`, adoption and sharing spelled
`Local: TypeAlias = ...`, redefinition re-owning an adopted local dimension,
`ConstList` not adoptable, `check_offset_provider` at every entry point with
the DaCe hook non-strict, its memoization and own-tag key rejection, the new
`MultiDimensionIndex` checks, and the pinned migration-script numbers.
---
 .../connectivities-as-types.md                | 142 ++++++++++++------
 1 file changed, 92 insertions(+), 50 deletions(-)

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 15e2506..fafe002 100644
--- a/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
@@ -247,7 +247,7 @@ class C2E(NeighborConnectivity[C, E]):
 
 
 class C2CE(NeighborConnectivity[C, CE]):       # a flattened sparse pattern:
-    Local = C2E.Local                          # shares C2E's neighbor axis
+    Local: typing.TypeAlias = C2E.Local        # shares C2E's neighbor axis
 
 
 class LsqUnk(LocalDimensionIndex, size=3): ...                       # owner-less local axis
@@ -355,9 +355,10 @@ tables assign different neighbors to the same origin element. The model:
 - **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`,
-  `CompilationOptions.connectivities` and DaCe `get_sdfg_conn_args`, and
-  *non-strictly* by `embedded.context.update` and the iterator `fendef`.
+  `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
@@ -368,12 +369,15 @@ tables assign different neighbors to the same origin element. The model:
   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 when a compiled
-  variant is created (variants are keyed by the *identity* of the bound
-  tables, so a new table object means a new variant and a new check) and on
-  every embedded `Program` / `FieldOperator` call; not on compiled calls,
-  because building a table's type is too slow for that path. It calls
-  `check_neighbor_table` per declaration, which checks the domain
+- **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
@@ -381,9 +385,13 @@ tables assign different neighbors to the same origin element. The model:
   `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, for concrete tables, on the skip positions.
-  The iterator `fendef`, `FieldOperatorFromFoast` and DaCe orchestration via
-  `CompilationOptions.connectivities` are not validated.
+  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
@@ -416,35 +424,52 @@ up.
 - `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 base declares `Local: ClassVar[type[LocalDimensionIndex]]` as an
-  *annotation only* (a real nested class on the base is an incompatible
-  override for pyright), and `__init_subclass__` reads `cls.Local` after the
-  class body. The annotation gives library code `conn.Local` as a *value* of
-  type `type[LocalDimensionIndex]`; it does not make `conn.Local` usable as an
-  *annotation* for a generic `conn`, which no checker allows — generic code
-  names the local dimension through a `TypeVar` bound to
-  `LocalDimensionIndex`.
-- A declaration can instead **adopt** a module-level local dimension
-  (`Local = 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*
+  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.
+  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 = 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
+  (`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).
-- **In annotations, name the local dimension by its declaring class.** An
-  adopted or shared `Local` is a plain class attribute assignment:
-  `C2CE.Local` works as a *value* (`axis=C2CE.Local`), but annotations should
-  write `Field[Dims[C, C2E.Local], ...]` or `Field[Dims[V, V2EDim], ...]`.
+- **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
@@ -464,7 +489,8 @@ up.
   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. (Type inference still
+  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
@@ -474,13 +500,16 @@ up.
 
 - `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,
-  hashes and pickles like the plain tuple. It is a user-facing typed index;
-  nothing in the toolchain requires it.
-- `*Ls` is unconstrained because `TypeVarTuple` cannot carry a bound; the
-  constructor checks the *kinds* of the components at runtime (one non-local
-  index, then local indices), not that the local dimensions belong to the
-  primary one: `MultiDimensionIndex(Edge(1), V2E.Local(1))` is accepted.
+  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
@@ -666,15 +695,13 @@ sparse storage treatment, changing ICON4Py's layout for `LsqUnkDim` fields.
    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 GridTools/gt4py#2910
-   description reports a dry run that rewrites `dimension.py` and 52 stencil
-   modules and leaves 79 provider-key sites and 14
-   `isinstance(..., Dimension)` checks to do by hand. These counts depend on
-   the ICON4Py revision and do not reproduce on current `main`: a re-run on
-   ICON4Py `89b4967` (2026-09-21), after ICON4Py had already dropped
-   `Koff[1]`, rewrites 5 files and reports 46 connectivity provider keys, 2
-   Cartesian provider entries and 5 `isinstance` checks. Declaring counts is
-   left to ICON4Py.
+   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
@@ -708,6 +735,21 @@ raises the churn and the long qualified names.
 | 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

From 950aea54ed35eab793f6fc3a83072779ffface62 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Enrique=20Gonz=C3=A1lez=20Paredes?= <enriqueg@cscs.ch>
Date: Wed, 23 Sep 2026 16:51:36 +0200
Subject: [PATCH 4/4] =?UTF-8?q?personal/egparedes:=20connectivities=20as?=
 =?UTF-8?q?=20types=20=E2=80=94=20refresh=20status=20and=20dependent-typin?=
 =?UTF-8?q?g=20appendix=20for=20the=20review=20fixes?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The appendix still described the pre-fix stack: shared and adopted Locals as
plain attributes, the table check missing at some entry points, and
MultiDimensionIndex not relating its components. Align it with the review-fix
commits on PRs 2-8, and stop pinning the status block to a branch SHA that the
rebase will move.
---
 .../connectivities-as-types.md                |  7 ++--
 ...onnectivities-as-types_dependent-typing.md | 32 ++++++++++---------
 2 files changed, 21 insertions(+), 18 deletions(-)

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 fafe002..3d8ae53 100644
--- a/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
+++ b/content/personal/egparedes/connectivities-as-types/connectivities-as-types.md
@@ -35,9 +35,10 @@ status: draft
 > 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` at `65fa529b6`, 2026-09-22);
-> where the implementation had to depart from the original proposal, the text
-> was corrected and the departure is listed in
+> (`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
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
index 853705f..4cc3f76 100644
--- 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
@@ -208,10 +208,10 @@ wrappers offer part of this discipline in ordinary languages.
 | `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))`; component kinds checked at run time, not that `V2E.Local` belongs to `V` |
+| `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` when a compiled variant is created and on embedded calls, then trusted by lowering and backends |
+| 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
 
@@ -224,8 +224,9 @@ wrappers offer part of this discipline in ordinary languages.
   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 exposes it as a plain attribute, so annotations
-  name the declaring class (`C2E.Local`, not `C2CE.Local`).
+  *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]]
@@ -284,8 +285,8 @@ 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, for concrete tables, skip values at the same
-positions, and reductions over the shared axis take that structure from any
+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.
@@ -293,15 +294,16 @@ 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. For compiled backends, `check_offset_provider` runs when
-a compiled variant is created, not on every call, because building a table's
-type is too slow for the call path; variants are keyed by the *identity* of
-the bound table objects, so binding a different table creates a new variant
-and re-runs the check, while re-binding the same object reuses the evidence.
-The remaining gap is the one §8 names for mutable data: a table modified in
-place after the check keeps its old evidence. Embedded calls re-check every
-time. Some entry points (the iterator-level `fendef`, DaCe orchestration) do
-not run the check at all — evidence that is never established.
+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