diff --git a/README.md b/README.md
index 9a7111a..76f31b4 100644
--- a/README.md
+++ b/README.md
@@ -4,369 +4,106 @@
 > tests, and documentation were developed with generative-AI assistance and
 > remain subject to maintainer review.
 
-New users can run the complete [ten-minute CPU
-quickstart](docs/src/learn/localmath-quickstart.md) before reading the
-compiler and execution details below.
+LocalMath is a typed language and execution layer for bounded local scientific
+computation. It represents finite spaces, fields, topology, conflict laws, and
+ordered publication independently of any one scientific domain. One validated
+lowering targets KernelAbstractions on CPU and GPU.
 
-`LocalMath` is the typed spatial and publication layer beneath bounded
-local scientific computations. A program says:
-
-- which finite `Space` owns each item;
-- which typed `Field`s hold scientific values;
-- which bounded `Relation`s connect spaces;
-- which fields a `Stage` gathers;
-- which conflict law publishes each result; and
-- which finite sequence of stages forms the local calculation.
-
-The package validates that meaning once, lowers it to one typed execution
-plan, and launches only KernelAbstractions kernels on CPU and GPU. Domain
-packages retain physics, clocks, semantic RNG, transactions, solvers,
-checkpoints, and distributed policy.
-
-## One typed waist
-
-The central representation is `LocalLaw`, containing an ordered tuple of
-typed `Stage`s. There is no parallel topology object, route-symbol program,
-backend-specific program, or old/new execution selector.
+Domain packages retain their physics, clocks, random-number semantics, solvers,
+transactions, checkpoints, and distributed policy.
 
 ```text
-domain compiler or mathematical notation
+mathematical notation or a domain compiler
                     ↓
                  LocalLaw
                     ↓
-        plan → prepare → execute! → wait
+        bind → plan → prepare → execute!
                     ↓
           KernelAbstractions CPU/GPU
 ```
 
-The ordinary mathematical form translates field notation directly into typed
-`Stage` values. Domain compilers may construct `LocalLaw(stage)` explicitly;
-there is no separate macro escape hatch or execution path:
-
-```julia
-law = @localmath (i ∈ cells;
-        parameters = (dt::Float32,)) begin
-    neighborhood = density[neighbors(i)]
-    next_density[i] = update(neighborhood, dt)
-end
-```
-
-`field[i]` is a required identity read, `field[relation(i)]` is a required
-bounded gather, and `samples(field[relation(i)])` retains explicit presence,
-boundary, and endpoint facts. Assignment lowers to `Unique`; `+=` lowers to a
-canonical `Reduce`. `resolve_to`, `bounded_collect`, `@ordered`, and explicit
-`publish(...; route, key, law)` cover resolution, finite collection, ordered
-recurrence, and runtime routing. `bounded_collect(record; maximum, group,
-groups)` keeps an explicit dense runtime group key separate from the stored
-record. Authored resolution accepts `sense=:min` or `sense=:max`, an explicit bounded tie field, and an exact
-empty result, for example
-`resolve_to(; score=depth[i], tie=identity[i], payload=color[i],
-onempty=UInt32(0))`; the lowest tie wins among equal scores. Several equations become named publication
-ports, while nested `@stage` blocks become the existing finite stage tuple.
+## Installation
 
-The macro is syntax translation only. Its parser records are discarded during
-expansion, every descriptor is evaluated once, and no syntax object reaches
-planning or a kernel.
-
-## Spatial values
-
-`Space(shape)` defines an ordinary finite index set. Domain compilers may use
-`Space(Tag, shape)` when the domain kind itself carries durable scientific
-meaning. `Field(space, T)` defines a logical value of type `T` at every point
-in that space. These descriptors contain scientific structure, not arrays.
+LocalMath is currently a pre-release package. Develop it from its repository
+until it is registered:
 
 ```julia
-cells = Space((nx, ny))
-padded = Space(PaddedTag, (nx + 2, ny + 2))
-
-density = Field(cells, Float32)
-padded_density = Field(padded, Float32)
+using Pkg
+Pkg.develop(url="https://github.com/PraneethMerugu/LocalMath.jl")
 ```
 
-Relations carry bounded connectivity and endpoint provenance:
+## A complete local computation
 
 ```julia
-self = IdentityRelation(cells)
-neighbors = FixedRelation(cells => padded; degree = 5)
-stream = AffineRelation(cells => padded; offsets = ((0, 0), (1, 0)))
-path = compose(first_relation, second_relation)
-```
+using LocalMath
+using KernelAbstractions
 
-For structured grids, compact Cartesian notation is a front-end spelling for
-the same affine relations:
+backend = KernelAbstractions.CPU()
+cells = Space((6, 6))
+u = Field(cells, Float32)
+laplacian = Field(cells, Float32)
 
-```julia
 law = @localmath (i, j) ∈ interior(cells, 1) begin
-    laplacian[i, j] = u[i - 1, j] + u[i + 1, j] +
-                      u[i, j - 1] + u[i, j + 1] - 4u[i, j]
-end
-```
-
-`interior(space, halo)` and `periodic(space)` are explicit authoring bounds.
-Only static binder offsets are admitted; they lower to bounded affine
-relations with exact directional footprints. No Cartesian storage or stencil
-executor is introduced.
-
-Available structural families include identity, affine, fixed, runtime,
-masked, selected, inverse, product, composed, boundary, and packed relations.
-Composition validates every adjacent space and preserves the product degree
-bound. It does not precompute a hidden adjacency table.
-
-Physical endpoint arrays are attached later during preparation. Planning validates
-their schema and contents and mints package-owned `RelationProof`s. Execution
-uses concrete device views and generation-qualified receipts; it never
-reconstructs a host topology object on a warm path.
-
-Direct fixed-topology arrays without a generation/status declaration are
-immutable borrows on CPU and GPU: LocalMath validates them when binding and
-callers must not mutate their contents for the lifetime of the bound law.
-Relations whose contents change use
-`LocalMath.MutableRelationStorage(storage; generation, status,
-validated_generations, slot)` so the same validation contract remains
-device-resident on CPU and GPU. Status and validated-generation arrays may be
-omitted only when an explicit backend is available to allocate them cold.
-
-## Local reads and publication laws
-
-`Access(field, relation)` means a bounded gather from the current stage item.
-Each evaluator receives only its declared gathered views, its typed parameters,
-and the source item. An evaluator must be a concrete, structurally
-device-admissible callable; capturing arrays or opaque runtime graphs is
-rejected.
-
-A publication law states the mathematics of competing writes. The common
-waist supports:
-
-- `Unique`: exact or partial assignment with proved destination ownership;
-- `Reduce`: deterministic ordered folds or explicitly relaxed qualified folds;
-- `Resolve`: argmin/argmax with payload, total rank bounds, tie-breaking, and
-  explicit empty behavior;
-- `Collect`: bounded canonical materialization with grouping and provenance;
-- `OrderedFold`: exact canonical sequential recurrence over mutable state.
-
-These are general operators, not Potts-, LBM-, LSM-, or FEM-specific features.
-One evaluator may publish several ports under different laws. Ordered stage
-composition remains finite and typed.
-
-`Control` supplies bounded prefix, mask, subset, and device-gate selection.
-False participation never calls the evaluator and never publishes a value.
-
-## Collections
-
-`Collection(T, capacity)` represents one bounded dynamic result. Its only
-runtime authority is `CompactedStorage`, containing records, one device count,
-optional group starts, source item/lane provenance, and an optional inverse
-source-position projection.
-
-Downstream stages consume collections without host settlement:
-
-- `CollectionCount(collection)` reads the device-resident live prefix;
-- `CollectionAccess(collection, BoundedGroup(K))` reads one bounded group;
-- `SourcePositionAccess(collection, lane=1)` reads one selected producer-lane
-  position; planning resolves and validates the producer's full emission width.
-
-Ordinary notation spells these same reads as
-`bounded(collection[i]; maximum=K)` and
-`source_position(collection, i; lane=k)`. Bounds and lanes are static authoring
-facts; no dynamically typed collection view reaches a kernel.
-
-The planner requires the exact preceding producer and proves capacity,
-occupancy, and projection compatibility. CPU and GPU use the same packed
-storage and the same execution path.
-
-## Ordered state
-
-Ordered recurrence declares both its total order and exact initial state:
-
-```julia
-law = @localmath event ∈ events begin
-    first = first_site[event]
-    second = second_site[event]
-
-    @ordered (
-        by=(ordinal[event], identity[event]),
-        state=(occupancy => occupancy_initial,
-               accepted => accepted_initial),
-    ) begin
-        admitted = occupancy[first] == 0 && occupancy[second] == 0
-        if admitted
-            occupancy[(first, second)] = (label[event], label[event])
-        end
-        accepted[event] = Int32(admitted)
-    end
+    laplacian[i, j] =
+        u[i - 1, j] + u[i + 1, j] +
+        u[i, j - 1] + u[i, j + 1] - 4f0 * u[i, j]
 end
-```
 
-Declared state reads observe the accumulated ordered prefix. Scalar and tuple
-assignments lower to statically bounded writes, and conditional assignments
-produce zero writes when false. `target => target` means explicit in-place
-initialization, `by=:source` selects source order, and `halt_when(condition)`
-terminates later steps. The macro generates a concrete isbits transition for
-the existing `OrderedFold`; no transaction object or runtime AST is created.
-
-## Preparation and execution
-
-Ordinary authors prepare storage with one lexical assignment block. The left
-side is the existing descriptor; the right side is caller-owned storage or an
-explicit cold allocation:
-
-```julia
-prepared = @prepare (
-    law;
-    backend = KernelAbstractions.get_backend(source_array),
-    lease_capacity = 3,
-) begin
-    source_field = source_array
-    result_field = result_array
-    neighbors = (endpoints = endpoint_array, counts = count_array)
-end
-receipt = execute!(prepared; parameters = parameter_values)
-wait(receipt)
-```
-
-`@prepare` is syntax-only lowering to `prepare(law, descriptor_pairs...;
-backend, ...)`. Every expression is evaluated once in ordinary Julia order;
-no setup value survives macro expansion. The Pair form remains canonical for
-dynamically generated compiler bindings.
-
-Storage-free computed relations are derived from the law and need no binding.
-The explicit `bind` and `plan` operations remain available to domain
-compilers, inspection tooling, and code that intentionally controls those cold
-boundaries; they accept the same flat descriptor-pair sequence.
-
-Caller-owned arrays are used exactly as supplied. Cold, LocalMath-owned
-storage is explicit and backend-qualified:
-
-```julia
+host_u = reshape(Float32.(1:36), 6, 6)
 prepared = @prepare (law; backend) begin
-    source_field = allocate(host_source)
-    result_field = allocate(undef)
-    neighbors = allocate((
-        endpoints = host_endpoints,
-        counts = host_counts,
-    ))
-    records = allocate()
+    u = host_u
+    laplacian = allocate(0f0)
 end
 
-result_array = LocalMath.storage(prepared, result_field)
+wait(execute!(prepared))
+result = LocalMath.storage(prepared, laplacian)
 ```
 
-A fixed relation may use its endpoint array directly when no per-source count
-array is needed. Mutable topology keeps its receipt state explicit:
-
-```julia
-prepared = prepare(law,
-    neighbors => LocalMath.MutableRelationStorage(
-        LocalMath.Allocate((; endpoints = host_endpoints));
-        generation = LocalMath.Allocate(UInt64[1]),
-    ),
-    field_pairs...;
-    backend,
-)
-```
-
-`Allocate(value)` fills only when `value` has the exact field element type;
-an exact-shape, exact-element-type array is copied into independent storage.
-`Allocate()` derives the precise bounded `CompactedStorage` of a produced
-Collection. Allocation and copying finish during cold preparation; allocation
-declarations never reach planning, preparation, or execution. An uninitialized
-field is admitted only when stage order proves that a total unconditional
-identity `Unique` publication initializes it before every use.
-
-Record-valued Fields use ordinary concrete isbits structs. A direct
-`StructArray` is borrowed with object identity intact; `allocate(struct_array)`
-recursively copies its component arrays onto the explicit backend and returns
-an independent `StructArray` with the same logical shape and element type.
-
-The lifecycle has one authority:
-
-1. `prepare(law, descriptor_pairs...; backend)` composes the existing cold
-   binding, planning, and preparation operations without another object or
-   execution path.
-2. Binding either retains caller storage or explicitly materializes requested
-   scientific storage; planning validates descriptors, relations, aliasing,
-   laws, and lowering.
-3. Preparation allocates or binds the exact bounded workspace and seals
-   callable methods for the selected backend.
-4. `execute!` appends the typed kernel sequence without an intermediate host wait.
-5. `wait(receipt)` synchronizes and drains the cumulative submitted prefix.
-
-Use `waitall(receipts...)` to settle several prepared plans sharing the same
-backend/device/task scope with one provider synchronization. Use
-`submission_capacity(prepared)` to preflight the bounded lease ledger.
-
-## Inspection
-
-`LocalMath.inspect` is public but intentionally unexported. It reports the
-stage origins, laws, executor family, field dependencies, relation proofs,
-workspace requirements, stage-local compiler spine, parameter ABI, backend
-environment, callable admission, and receipt state.
-
-```julia
-facts = LocalMath.inspect(prepared)
-facts.stages                         # semantic stages plus planning projections
-facts.relations                      # validated topology and footprint facts
-facts.planning.stage_phases          # current physical implementation
-facts.realized.callback_methods      # concrete callable admission
-```
-
-Focused projections use the same canonical facts:
-
-```julia
-relations = LocalMath.inspect(prepared; level=:relations)
-numerics = LocalMath.inspect(prepared; level=:numerics)
-memory = LocalMath.inspect(prepared; level=:memory)
-kernels = LocalMath.inspect(prepared; level=:kernels)
-compiler = LocalMath.compilation_report(prepared)
-```
+The equation creates ordinary typed LocalMath values. `@prepare` is hygienic
+syntax for descriptor-to-storage pairs; it does not introduce a builder or a
+second execution path. Caller arrays are borrowed exactly as supplied, while
+`allocate(...)` requests explicit cold LocalMath-owned storage on the selected
+backend.
 
-`compilation_report` reports structural specialization and realized method
-facts. It never predicts wall time or participates in planning.
+## Mathematical scope
 
-Descriptors also have compact REPL displays. A `Field` shows its element type,
-space extent, and abbreviated semantic identity; a `Relation` shows its family,
-domain and codomain, degree, and whether physical storage is required.
-Displaying a law, plan, or prepared plan summarizes descriptors, stages,
-provenance, workspace, storage ownership, and physical segments without
-planning, submitting, or synchronizing work.
+LocalMath provides:
 
-If setup is incomplete, canonical binding reports all missing Fields, stored
-Relations, and Collections in scientific encounter order. Fixed-topology
-errors include the expected lane/domain layout and actual storage shape. The
-manual's “LocalMath relations and storage” page contains the topology
-selection table and complete binding examples.
+- required and presence-aware bounded gathers;
+- unique assignment and deterministic or explicitly relaxed reduction;
+- argmin/argmax resolution with payload and tie-breaking;
+- bounded grouped collection with source provenance;
+- finite ordered recurrence over explicit state;
+- multiple publication ports and ordered stage composition;
+- structured inspection of topology, storage, lowering, and physical launches.
 
-Inspection is a cold, read-only projection, not a second semantic
-representation. Production planning and execution never consume it. Semantic
-fields describe the law; planning and realized fields describe the current
-implementation. The `0.2` contract freezes their documented meaning, while
-later compatible releases may add descriptive fields.
+Relations include identity, affine, fixed, boundary, indexed, selected,
+inverse, product, composed, runtime, masked, and packed topology. Dynamic
+topology remains packed and generation-qualified during execution.
 
-## Backend contract
+## Execution guarantees
 
-All package-owned execution uses KernelAbstractions. Vendor packages supply
-array types and a backend, but LocalMath contains no raw Metal, CUDA, AMDGPU,
-or oneAPI launch/synchronization path. The same typed lowering is used on CPU
-and GPU. The release suite executes on CPU and Metal; other conforming
-KernelAbstractions providers remain architecturally admissible but are not
-qualified or claimed by this release.
+The current implementation has one packed KernelAbstractions execution path.
+Preparation validates descriptors, storage, topology, callable admission,
+aliasing, workspace, and backend requirements. Warm execution performs no
+scientific storage allocation, relation packing, symbolic interpretation, or
+host scalar round trip.
 
-Warm execution owns only prepared typed views, bounded workspace, and receipt
-state. Cold host descriptors and serialization values must be converted before
-planning or preparation; conversion is forbidden during queued execution.
+CPU and Metal are exercised by the current test suite. Other
+KernelAbstractions providers are not claimed until independently qualified.
 
-## Scientific ownership
+Inspection is a cold projection over the semantic law, validated plan, and
+prepared runtime. Planning and execution never consume inspection reports.
 
-LocalMath owns bounded gathering, local evaluation, routing, assignment,
-folding, resolution, collection, ordered recurrence, composition, validation,
-workspace, and execution lifetime. It does not absorb domain meaning.
+## Learn more
 
-For example, CorePotts retains Hamiltonian source order, before/after proposal
-semantics, semantic RNG, Metropolis acceptance, MCS scheduling, lifecycle
-transactions, checkpoint continuation, and CPM capability claims. LBM retains
-collision and boundary-model meaning; LSM retains constitutive and fracture
-meaning; FEM retains weak-form and solver meaning.
+- [Ten-minute quick start](docs/src/learn/localmath-quickstart.md)
+- [Relations and storage](docs/src/learn/localmath-relations.md)
+- [Scientific recipes](docs/src/learn/localmath-recipes.md)
+- [Troubleshooting](docs/src/learn/localmath-troubleshooting.md)
+- [Domain compiler guide](docs/src/learn/localmath-domain-compiler.md)
+- [API reference](docs/src/api/localmath.md)
+- [Contributing](CONTRIBUTING.md)
+- [Citation metadata](CITATION.cff)
 
-That boundary is intentional: many scientific languages can lower to one
-small local-computation waist without turning LocalMath into a universal
-simulation framework.
+LocalMath is MIT licensed.
diff --git a/docs/make.jl b/docs/make.jl
index a3aaa49..3d3db54 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -1,6 +1,41 @@
 using Documenter
 using LocalMath
 
+pages = [
+    "Home" => "index.md",
+    "Quick start" => "learn/localmath-quickstart.md",
+    "Relations and storage" => "learn/localmath-relations.md",
+    "Scientific recipes" => "learn/localmath-recipes.md",
+    "Troubleshooting" => "learn/localmath-troubleshooting.md",
+    "Domain compilers" => "learn/localmath-domain-compiler.md",
+    "API" => "api/localmath.md",
+]
+
+function documented_pages(items)
+    paths = String[]
+    for item in items
+        value = item isa Pair ? last(item) : item
+        if value isa AbstractString
+            push!(paths, String(value))
+        else
+            append!(paths, documented_pages(value))
+        end
+    end
+    return paths
+end
+
+source_root = joinpath(@__DIR__, "src")
+source_pages = sort!(String[
+    relpath(joinpath(root, file), source_root)
+    for (root, _, files) in walkdir(source_root)
+    for file in files if endswith(file, ".md")
+])
+navigation_pages = sort!(documented_pages(pages))
+source_pages == navigation_pages || error(
+    "Documenter navigation must own every Markdown page; source=$(source_pages), " *
+    "navigation=$(navigation_pages)",
+)
+
 makedocs(
     sitename = "LocalMath.jl",
     authors = "Praneeth Merugu",
@@ -10,13 +45,5 @@ makedocs(
     pagesonly = true,
     checkdocs = :exports,
     remotes = nothing,
-    pages = [
-        "Home" => "index.md",
-        "Quick start" => "learn/localmath-quickstart.md",
-        "Relations and storage" => "learn/localmath-relations.md",
-        "Scientific recipes" => "learn/localmath-recipes.md",
-        "Troubleshooting" => "learn/localmath-troubleshooting.md",
-        "Domain compilers" => "learn/localmath-domain-compiler.md",
-        "API" => "api/localmath.md",
-    ],
+    pages = pages,
 )
diff --git a/docs/src/learn/localmath.md b/docs/src/learn/localmath.md
deleted file mode 100644
index 030fb1e..0000000
--- a/docs/src/learn/localmath.md
+++ /dev/null
@@ -1,174 +0,0 @@
-# LocalMath across domains
-
-LocalMath is a typed language for bounded local reads and conflict-aware
-publication. A domain model owns its scientific equations; LocalMath describes
-where each local calculation reads and how its results become spatial state.
-
-```julia
-law = @localmath (cell ∈ cells; parameters=(dt::Float32,)) begin
-    local_population = population[neighbors(cell)]
-    next_population[cell] = collide(local_population, dt)
-end
-```
-
-The same authoring and execution path is exercised by dimension-parametric
-stencils, D2Q9 collision and streaming, lattice-spring mechanics, matrix-free
-finite-element application, CIC/TSC deposition, graph gather and scatter,
-bounded recurrence, deterministic routed resolution, and a focused Potts
-proposal calculation. These examples use independent numerical oracles; the
-oracle is not a second LocalMath executor.
-
-Ordinary spaces need no marker type. Structured notation keeps the boundary
-contract in the equation while lowering to existing affine relations:
-
-```julia
-cells = Space((nx, ny))
-laplacian = @localmath (i, j) ∈ interior(cells, 1) begin
-    Δu[i, j] = u[i - 1, j] + u[i + 1, j] +
-               u[i, j - 1] + u[i, j + 1] - 4u[i, j]
-end
-```
-
-Use `periodic(cells)` for periodic indexing. Offset indices must be static;
-LocalMath neither guesses boundary behavior nor creates adjacency storage.
-
-Resolution makes conflict semantics visible in the equation:
-
-```julia
-law = @localmath fragment ∈ fragments begin
-    color[pixel(fragment)] = resolve_to(;
-        score=depth[fragment],
-        tie=identity[fragment],
-        payload=rgba[fragment],
-        lower=-100,
-        upper=100,
-        onempty=UInt32(0),
-        when=covered[fragment],
-    )
-end
-```
-
-Equal scores select the lowest explicit tie. An exact `onempty` value is
-published when no fragment participates; `onempty=:preserve` retains the
-destination. Reduction order is likewise explicit: `order=:canonical` gives a
-deterministic fold and `order=:relaxed` selects the relaxed atomic law where
-the operation supports it.
-
-Scientific storage remains explicit. Descriptors carry mathematical identity
-and topology; the setup block associates those lexical descriptors with
-caller-owned arrays or explicit cold allocation. LocalMath never guesses
-initialization or silently allocates an omitted output.
-
-```julia
-prepared = @prepare (law; backend) begin
-    population = allocate(host_population)
-    next_population = allocate(undef)
-    neighbors = allocate(host_neighbors)
-end
-
-wait(execute!(prepared; parameters=(dt=0.1f0,)))
-next_values = LocalMath.storage(prepared, next_population)
-```
-
-Computed identity and affine relations require no placeholder binding. Stored
-relations remain explicit because their endpoint arrays are scientific input.
-Direct fixed-topology arrays are immutable borrows on CPU and GPU; LocalMath
-validates their bounds once during cold binding and does not attach mutable
-generation receipts or repeat that validation during execution.
-Domain compilers and inspection tooling can still use the same flat pairs with
-the explicit `bind` and `plan` operations when they need to observe
-the intermediate cold boundaries.
-
-The reserved top-level forms are `allocate()`, `allocate(undef)`, and
-`allocate(value_or_source)`. Other right-hand expressions pass through as
-ordinary storage values. Direct arrays, including `StructArray` record
-storage, are borrowed without adaptation. Allocating a `StructArray` copies
-its component arrays onto the explicit backend while preserving its element
-type, shape, and component structure.
-
-Bounded dynamic records stay on the device. A producer may request a persistent
-source-position projection, and a later stage consumes the same collection
-without host settlement:
-
-```julia
-law = @localmath begin
-    @stage produce(p ∈ particles) begin
-        records[p] = bounded_collect(record(p);
-            maximum=1, group=cell(p), groups=ncells,
-            projection=:source_position)
-    end
-
-    @stage consume(c ∈ cells) begin
-        local_record = bounded(records[c]; maximum=1)
-        mass[c] = length(local_record) == 0 ? 0f0 : local_record[1].mass
-    end
-
-    @stage project_source(p ∈ particles) begin
-        record_position[p] = source_position(records, p; lane=1)
-    end
-end
-```
-
-`count(records)` is the number of live records, not the extent of the grouping
-key domain, so grouped consumers iterate the complete `cells` space (or an
-explicit dense remapping of occupied keys). The projection is consumed by
-producer identity in the final stage. Its maximum and projection lane are
-static facts and lower to the existing typed collection access laws.
-
-Cartesian binder symbols currently appear only inside Field indices. Use
-Fields or explicit parameters for coordinate-dependent coefficients; this
-keeps coordinate meaning explicit until that grammar is extended.
-
-Ordered state uses the same equation vocabulary while making initialization
-and total order explicit:
-
-```julia
-law = @localmath event ∈ events begin
-    first = first_site[event]
-    second = second_site[event]
-
-    @ordered (
-        by=(ordinal[event], identity[event]),
-        state=(occupancy => occupancy_initial,
-               accepted => accepted_initial),
-    ) begin
-        admitted = occupancy[first] == 0 && occupancy[second] == 0
-        if admitted
-            occupancy[(first, second)] = (label[event], label[event])
-        end
-        accepted[event] = Int32(admitted)
-    end
-end
-```
-
-Reads from `occupancy` in this block observe the accumulated ordered state,
-not the stage-entry snapshot. Tuple assignment is a statically bounded write;
-the `if` produces zero occupancy writes when admission fails. Use
-`target => target` for explicit in-place initialization, `by=:source` for
-source order, and `halt_when(condition)` for an ordered terminal step. The
-macro produces the existing typed `OrderedFold`; it does not create a task
-graph, transaction object, or second runtime.
-
-Bounded neighborhood mathematics can be packaged as an ordinary concrete
-callable while retaining explicit invalid, empty, and order semantics:
-
-```julia
-positive_geometric_mean = LocalMath.bounded_fold(
-    log, +, 0.0, (sum, count) -> exp(sum / count);
-    domain=LocalMath.Where(>(0)),
-    oninvalid=LocalMath.RejectInvalid(),
-    onempty=LocalMath.RejectEmpty(),
-    order=LocalMath.CanonicalLeftFold(),
-)
-```
-
-The operator consumes only a bounded gathered view or bounded collection
-group. Its implementation is a concrete evaluator-side fold; no dynamic
-iterator, allocation, or symbolic expression reaches a device kernel.
-
-Advanced authors and domain compilers may construct qualified `Stage`,
-`Publication`, and publication-law values directly. Those constructors lower
-to the same `LocalLaw`, planner, packed storage, and KernelAbstractions path;
-they are not an alternate runtime. Collection and recurrence notation is kept
-only where the cross-domain witnesses proved that it preserves explicit bounds,
-ordering, initialization, and conflict semantics.
diff --git a/docs/src/localmath-0.2-release-candidate.md b/docs/src/localmath-0.2-release-candidate.md
deleted file mode 100644
index cba53ce..0000000
--- a/docs/src/localmath-0.2-release-candidate.md
+++ /dev/null
@@ -1,45 +0,0 @@
-# LocalMath 0.2 release candidate
-
-LocalMath `0.2.0-rc1` is the first release candidate for the typed, bounded,
-conflict-aware local-computation interface used by CorePotts and the scientific
-witness corpus.
-
-## Frozen contract
-
-The release candidate freezes:
-
-- `Space`, `Field`, `Relation`, `Collection`, and `LocalLaw`;
-- `@localmath` Cartesian, gathered, routed, collected, and ordered-state forms;
-- explicit descriptor-keyed preparation and storage ownership;
-- `Unique`, `Reduce`, `Resolve`, `Collect`, and `OrderedFold` semantics;
-- `IndexRelation`, bounded folds, and transparent scalar functions;
-- `Plan`, `PreparedPlan`, `ExecutionReceipt`, and dependency settlement;
-- canonical inspection, focused inspection levels, and compilation reports;
-- the qualified low-level constructors used by scientific domain compilers.
-
-LocalMath owns spatial access, validation, publication, ordering, workspace,
-and physical KernelAbstractions execution. Domain packages retain equations,
-solvers, scientific RNG, scheduling, transactions, checkpoints, and capability
-claims.
-
-## Backend statement
-
-The implementation contains one packed KernelAbstractions path and no vendor-
-specific launch or synchronization branch. The release suite exercises CPU and
-real Metal with the same laws and storage model. Other conforming
-KernelAbstractions providers remain possible inputs to cold preparation, but
-this release makes no scientific support claim without corresponding hardware
-evidence.
-
-## Deliberate limitations
-
-- Distributed partitioning and scheduling are outside LocalMath.
-- Halo inspection reports communication requirements but does not execute MPI.
-- Compilation reports expose structure and realized methods, not predicted
-  wall time.
-- Static bounds, boundary behavior, initialization, conflict semantics, and
-  backend choice remain explicit.
-- CUDA and ROCm qualification are deferred.
-
-This release candidate is not a registry submission. Publication and any later
-provider qualification are separate release activities.
diff --git a/src/execution/program_inspection.jl b/src/execution/program_inspection.jl
index 8d129a6..52c4bd1 100644
--- a/src/execution/program_inspection.jl
+++ b/src/execution/program_inspection.jl
@@ -4,6 +4,579 @@ This file projects facts from the semantic law, validated binding, physical
 lowering, and prepared runtime. Execution never consumes these projections.
 """
 
+@inline function _stage_parameter_slot_inspection(
+        slot::_StageParameterSlot{T}) where {T}
+    bounds = slot.bounds isa _ClosedParameterBounds ?
+        (lower = slot.bounds.lower, upper = slot.bounds.upper) : nothing
+    return (name = slot.name, type = T, bounds)
+end
+_stage_parameter_layout_inspection(layout::_StageParameterLayout) =
+    map(_stage_parameter_slot_inspection, layout.slots)
+
+_lowering_identity(::_StageProgramLowering) =
+    :stage_local_erased_kernelabstractions_v1
+
+_parameter_inspection(declaration::Parameter) = (
+    name = declaration.name,
+    type = _parameter_type(declaration),
+    bounds = declaration.bounds isa _ClosedParameterBounds ?
+        (lower = declaration.bounds.lower,
+            upper = declaration.bounds.upper) : nothing,
+)
+
+_space_kind_inspection(::Space{_IndexSpaceKind}) = :index
+_space_kind_inspection(::Space{_ProductSpaceKind}) = :product
+_space_kind_inspection(::Space{K}) where {K} = K
+_space_structure_inspection(::Space{K,N,_PlainSpaceStructure}) where {K,N} = nothing
+_space_structure_inspection(
+        space::Space{_ProductSpaceKind,N,S}) where {N,S<:_ProductSpaceStructure} =
+    (factors = map(_space_inspection, _space_factors(space)),)
+
+_space_inspection(space::Space) = (
+    identity = semantic_identity(space),
+    kind = _space_kind_inspection(space),
+    extent = size(space),
+    structure = _space_structure_inspection(space),
+)
+
+_relation_representation_inspection(::_IdentityRelation) = (family = :identity,)
+_relation_representation_inspection(value::_AffineRelation) =
+    (family = :affine, offsets = value.offsets, origin = value.origin)
+_relation_representation_inspection(value::_FixedRelation) =
+    (family = :fixed, degree = value.degree)
+_relation_representation_inspection(value::_ProductRelation) =
+    (family = :product, factors = map(semantic_identity, value.factors),
+        degree = value.degree)
+_relation_representation_inspection(value::_ComposedRelation) =
+    (family = :composed, factors = map(semantic_identity, value.factors),
+        degree = value.degree)
+_relation_representation_inspection(value::_BoundaryRelation) =
+    (family = :boundary, base = semantic_identity(value.base),
+        policy = _boundary_policy_facts(value.policy), degree = value.degree)
+_relation_representation_inspection(value::_RuntimeRelation) =
+    (family = :runtime, degree = value.degree, key_type = value.key_type,
+        ownership = value.ownership)
+_relation_representation_inspection(value::_FieldIndexRelation) =
+    (family = :field_index, keys = semantic_identity(value.keys),
+        degree = value.degree, optional = value.optional)
+_relation_representation_inspection(value::_MaskedRelation) =
+    (family = :masked, base = semantic_identity(value.base),
+        mask = semantic_identity(value.mask), degree = value.degree)
+_relation_representation_inspection(value::_SelectedRelation) =
+    (family = :selected, base = semantic_identity(value.base),
+        injection = semantic_identity(value.injection), degree = value.degree)
+_relation_representation_inspection(value::_InverseRelation) =
+    (family = :inverse, forward = semantic_identity(value.forward),
+        degree = value.degree)
+_relation_representation_inspection(value::_PackedRelation) =
+    (family = :packed, degree = value.degree, capacity = value.capacity,
+        layout = value.layout, ownership = value.ownership)
+
+_relation_footprint_inspection(relation::Relation{_IdentityRelation}) =
+    (strength = :exact, kind = :identity)
+_relation_footprint_inspection(relation::Relation{<:_AffineRelation}) =
+    merge((strength = :exact,), _relation_footprint(relation))
+function _relation_footprint_inspection(
+        relation::Relation{<:_BoundaryRelation})
+    relation.representation.base.representation isa _AffineRelation ||
+        return merge((strength = :bounded,), _relation_footprint(relation))
+    return merge((strength = :exact,), _relation_footprint(relation))
+end
+_relation_footprint_inspection(
+        relation::Relation{<:Union{_RuntimeRelation,_PackedRelation}}) =
+    (strength = :opaque, kind = :runtime_bounded,
+        degree = degree_bound(relation))
+_relation_footprint_inspection(relation::Relation{<:_FieldIndexRelation}) =
+    (strength = :opaque, kind = :bounded_indirect,
+        degree = degree_bound(relation),
+        keys = semantic_identity(relation.representation.keys))
+_relation_footprint_inspection(relation::Relation) =
+    merge((strength = :bounded,), _relation_footprint(relation))
+
+_ownership_inspection(::_ComputedOwnership) = :computed
+_ownership_inspection(::_LocalOwnership) = :local
+_ownership_inspection(::_SharedOwnership) = :shared
+_ownership_inspection(::_GhostOwnership) = :ghost
+_ownership_inspection(::_ExternalOwnership) = :external
+_ownership_inspection(::_TemporaryOwnership) = :temporary
+
+function _relation_inspection(relation::Relation, proof)
+    proof_value = proof === nothing ? nothing : (
+        ownership = _ownership_inspection(proof.binding_schema.ownership),
+        bounds = proof.evidence.bounds,
+        multiplicity = proof.evidence.multiplicity,
+        coverage = proof.evidence.coverage,
+        canonical_order = proof.evidence.canonical_order,
+        physical_representation = proof.binding_schema.representation,
+        physical_leaves = proof.binding_schema.physical_leaves,
+    )
+    return (
+        identity = semantic_identity(relation),
+        domain = semantic_identity(domain(relation)),
+        codomain = semantic_identity(codomain(relation)),
+        schema_epoch = schema_epoch(relation),
+        representation = _relation_representation_inspection(
+            relation.representation),
+        proof = proof_value,
+        footprint = _relation_footprint_inspection(relation),
+    )
+end
+
+_collection_access_law_inspection(::_BoundedGroup{K}) where {K} =
+    (kind = :bounded_group, maximum = K)
+_collection_access_law_inspection(::_SourcePositionsAccess{K,L}) where {K,L} =
+    (kind = :source_position, width = K, lane = L)
+
+_dependency_inspection(::Nothing) = nothing
+_dependency_inspection(value::_ExternalFieldDependency) =
+    (kind = :external, resource = :field, identity = value.field_id)
+_dependency_inspection(value::_PrecedingFieldDependency) =
+    (kind = :stage, resource = :field, identity = value.field_id,
+        stage = value.stage)
+_dependency_inspection(value::_PrecedingCollectionDependency) =
+    (kind = :stage, resource = :collection,
+        identity = value.collection_id, stage = value.stage,
+        role = value.role)
+_dependency_inspection(value::_RelationUse) =
+    (kind = :relation, identity = value.relation_id)
+
+function _read_inspection(role::Symbol, access::Access, dependency = nothing)
+    return (
+        role,
+        kind = :field,
+        identity = semantic_identity(access.field),
+        value_type = eltype(access.field),
+        space = semantic_identity(access.field.space),
+        relation = semantic_identity(access.relation),
+        version = :stage_entry,
+        mode = access.mode isa _RequiredAccess ? :required : :samples,
+        ghost = access.ghost === nothing ? nothing :
+            semantic_identity(access.ghost),
+        producer = _dependency_inspection(dependency),
+    )
+end
+function _read_inspection(
+        role::Symbol, access::CollectionAccess, dependency = nothing)
+    return (
+        role,
+        kind = :collection,
+        identity = semantic_identity(access.collection),
+        value_type = eltype(access.collection),
+        capacity = access.collection.capacity,
+        law = _collection_access_law_inspection(access.law),
+        producer = _dependency_inspection(dependency),
+    )
+end
+
+_control_part_inspection(::_NoPrefix) = (kind = :none,)
+_control_part_inspection(value::_ParameterPrefix) =
+    (kind = :parameter, parameter = value.parameter.name)
+_control_part_inspection(value::_FieldPrefix) =
+    (kind = :field, identity = semantic_identity(value.field))
+_control_part_inspection(value::_CollectionCount) =
+    (kind = :collection_count,
+        identity = semantic_identity(value.collection))
+_control_part_inspection(::_NoMask) = (kind = :none,)
+_control_part_inspection(value::_MaskSelection) =
+    (kind = :field, identity = semantic_identity(value.field))
+_control_part_inspection(::_NoSubset) = (kind = :none,)
+_control_part_inspection(value::_SubsetSelection) =
+    (kind = :relation, identity = semantic_identity(value.relation))
+_control_part_inspection(::_NoGate) = (kind = :none,)
+_control_part_inspection(value::_ParameterGate) =
+    (kind = :parameter, parameter = value.parameter.name)
+_control_part_inspection(value::_FieldGate) =
+    (kind = :field, identity = semantic_identity(value.field))
+_control_part_with_producer(value, ::Nothing) =
+    _control_part_inspection(value)
+_control_part_with_producer(value, dependency) = merge(
+    _control_part_inspection(value),
+    (producer = _dependency_inspection(dependency),),
+)
+function _control_inspection(control::Control, dependencies = nothing)
+    producers = dependencies === nothing ?
+        (prefix = nothing, mask = nothing, subset = nothing, gate = nothing) :
+        (prefix = dependencies.collection_prefix === nothing ?
+                dependencies.control.prefix : dependencies.collection_prefix,
+            mask = dependencies.control.mask,
+            subset = dependencies.control.subset,
+            gate = dependencies.control.gate)
+    return (
+        prefix = _control_part_with_producer(
+            control.prefix, producers.prefix),
+        mask = _control_part_with_producer(control.mask, producers.mask),
+        subset = _control_part_with_producer(
+            control.subset, producers.subset),
+        gate = _control_part_with_producer(control.gate, producers.gate),
+    )
+end
+
+function _stage_reads_inspection(stage::Stage, dependencies = nothing)
+    names = keys(stage.accesses)
+    access_values = Base.values(stage.accesses)
+    dependency_values = dependencies === nothing ?
+        ntuple(_ -> nothing, length(access_values)) :
+        Base.values(dependencies.accesses)
+    reads = Any[ntuple(index -> _read_inspection(
+            names[index], access_values[index], dependency_values[index]),
+        length(access_values))...]
+    for publication in stage.publications
+        publication.law isa OrderedFold || continue
+        state_dependencies = dependencies === nothing ? nothing :
+            dependencies.state
+        state_names = keys(publication.law.state.components)
+        for (index, component) in enumerate(
+                values(publication.law.state.components))
+            field = component.source isa _FoldInPlace ?
+                component.target : component.source
+            dependency = state_dependencies === nothing ? nothing : begin
+                pair = getfield(state_dependencies, index)
+                component.source isa _FoldInPlace ? pair.target : pair.source
+            end
+            push!(reads, (
+                role = Symbol(:fold_state_, state_names[index]),
+                kind = :fold_state,
+                identity = semantic_identity(field),
+                value_type = eltype(field),
+                space = semantic_identity(field.space),
+                relation = nothing,
+                version = :stage_entry,
+                ghost = nothing,
+                producer = _dependency_inspection(dependency),
+            ))
+        end
+    end
+    return Tuple(reads)
+end
+
+function _stage_relation_uses(stage::Stage)
+    uses = Any[]
+    for access in values(stage.accesses)
+        access isa Access && push!(uses, (
+            relation = semantic_identity(access.relation), direction = :read))
+    end
+    for publication in stage.publications, component in publication.components
+        component isa FieldPublication && push!(uses, (
+            relation = semantic_identity(component.relation),
+            direction = :publication))
+    end
+    stage.control.subset isa _SubsetSelection && push!(uses, (
+        relation = semantic_identity(stage.control.subset.relation),
+        direction = :control))
+    return Tuple(unique(uses))
+end
+
+function _semantic_stage_inspection(stage::Stage, index::Int;
+        dependencies = nothing, planning = nothing)
+    return (
+        index,
+        source = _space_inspection(stage.source),
+        origin = stage.origin,
+        reads = _stage_reads_inspection(stage, dependencies),
+        control = _control_inspection(stage.control, dependencies),
+        publications = map(_stage_publication_context, stage.publications),
+        planning,
+    )
+end
+
+function _semantic_equivalence(law::LocalLaw)
+    _, relations, _ = _law_descriptor_requirements(law)
+    stages = Tuple(map(enumerate(law.stages)) do (index, stage)
+        report = _semantic_stage_inspection(stage, index)
+        publications = map(report.publications) do publication
+            merge(publication, (origin = nothing,))
+        end
+        return merge(report,
+            (origin = nothing, publications, planning = nothing))
+    end)
+    return (
+        parameters = map(_parameter_inspection,
+            law.parameters.declarations),
+        relations = map(relation -> _relation_inspection(relation, nothing),
+            relations),
+        stages,
+        evaluators = map(stage -> (
+                value = stage.evaluator.evaluator,
+                type = typeof(stage.evaluator.evaluator),
+                parameters = map(_parameter_inspection,
+                    stage.evaluator.parameters),
+            ), law.stages),
+    )
+end
+
+function _inspect_local_law(law::LocalLaw)
+    _, relations, _ = _law_descriptor_requirements(law)
+    return (
+        lifecycle = :LocalLaw,
+        parameters = map(_parameter_inspection,
+            law.parameters.declarations),
+        relations = map(relation -> _relation_inspection(relation, nothing),
+            relations),
+        stages = Tuple(map(enumerate(law.stages)) do (index, stage)
+            _semantic_stage_inspection(stage, index)
+        end),
+        planning = nothing,
+        equivalence = _semantic_equivalence(law),
+    )
+end
+
+function _planned_relation_phases(entry::_StageLoweringEntry;
+        reset_fused::Bool = false)
+    isempty(entry.relation_dependencies) && return ()
+    validators = count(dependency ->
+        !(dependency.validator isa _NoRelationContentValidator),
+        entry.relation_dependencies)
+    launches_per_validator = reset_fused ? 2 : 3
+    validation = validators == 0 ? () :
+        (_phase_fact(:relationship_validation,
+            launches_per_validator * validators),)
+    return (validation..., _phase_fact(:relationship_receipt))
+end
+
+_planned_stage_phases(entry::_StageLoweringEntry{
+        A,W,<:_CandidateStageExecutor{<:_DirectIdentityUniqueLayout}}) where {A,W} =
+    (_phase_fact(:direct_identity_unique),)
+function _planned_stage_phases(entry::_StageLoweringEntry{
+        A,W,<:_CandidateStageExecutor{<:_GroupedCandidateLayout}}) where {A,W}
+    phases = Any[_phase_fact(:candidate_reset)]
+    append!(phases, _planned_relation_phases(entry; reset_fused = true))
+    push!(phases, _phase_fact(:candidate_evaluate))
+    for shape in entry.workspace.ports
+        if hasproperty(shape, :atomic_selection)
+            push!(phases, _phase_fact(:resolve_atomic_winner))
+            continue
+        end
+        hasproperty(shape, :grouping_shape) || continue
+        push!(phases, _phase_fact(:destination_grouping_local_sort))
+        shape.grouping_shape.merge_passes == 0 || push!(phases,
+            _phase_fact(:destination_grouping_merge,
+                shape.grouping_shape.merge_passes))
+        push!(phases, _phase_fact(:destination_grouping_directory))
+    end
+    push!(phases, _phase_fact(:candidate_validate))
+    publications = entry.admission.stage.publications
+    _candidate_phase_required(publications,
+        _candidate_atomic_initialization_required) && push!(phases,
+            _phase_fact(:candidate_atomic_initialize))
+    _candidate_phase_required(publications,
+        _candidate_atomic_required) && push!(phases,
+            _phase_fact(:candidate_atomic))
+    push!(phases, _phase_fact(:candidate_finalize_publish))
+    return Tuple(phases)
+end
+function _planned_stage_phases(entry::_StageLoweringEntry{
+        A,W,<:_CollectStageExecutor}) where {A,W}
+    phases = Any[_phase_fact(:collect_reset)]
+    append!(phases, _planned_relation_phases(entry))
+    push!(phases, _phase_fact(:collect_evaluate))
+    for port in entry.workspace.ports
+        items = div(Int(port.candidate_count), _collect_width(port))
+        levels = _collect_scan_level_count(items)
+        push!(phases, _phase_fact(:collect_scan_block, levels))
+        levels == 1 || push!(phases,
+            _phase_fact(:collect_scan_add, levels - 1))
+    end
+    for port in entry.workspace.ports
+        push!(phases, _phase_fact(:collect_scatter))
+        port.sort_required || continue
+        push!(phases, _phase_fact(:collect_local_bitonic))
+        port.merge_passes == 0 || push!(phases,
+            _phase_fact(:collect_merge, port.merge_passes))
+        _is_grouped(port.groups) && push!(phases,
+            _phase_fact(:collect_directory))
+        _is_canonical_order(port.order) && push!(phases,
+            _phase_fact(:collect_validate_order))
+    end
+    append!(phases, (_phase_fact(:collect_finalize),
+        _phase_fact(:collect_publish,
+            cld(length(entry.admission.stage.publications),
+                _POINTWISE_SEGMENT_LIMIT))))
+    return Tuple(phases)
+end
+function _planned_stage_phases(entry::_StageLoweringEntry{
+        A,W,<:_OrderedFoldStageExecutor}) where {A,W}
+    phases = Any[_phase_fact(:ordered_fold_reset)]
+    append!(phases, _planned_relation_phases(entry))
+    push!(phases, _phase_fact(:ordered_fold_evaluate))
+    extent = nextpow(2, max(Int(entry.admission.stage.source_count), 1))
+    bitonic = 0
+    width = 2
+    while width <= extent
+        distance = width >>> 1
+        while distance >= 1
+            bitonic += 1
+            distance >>>= 1
+        end
+        width <<= 1
+    end
+    bitonic == 0 || push!(phases,
+        _phase_fact(:ordered_fold_bitonic, bitonic))
+    append!(phases, (_phase_fact(:ordered_fold_validate_initialize),
+        _phase_fact(:ordered_fold_apply),
+        _phase_fact(:ordered_fold_finalize)))
+    return Tuple(phases)
+end
+
+_phase_count(phases) = sum(phase.count for phase in phases; init = 0)
+
+_stage_layout_name(::_CandidateStageExecutor{<:_GroupedCandidateLayout}) =
+    :grouped_candidate
+_stage_layout_name(::_CandidateStageExecutor{<:_DirectIdentityUniqueLayout}) =
+    :direct_identity_unique
+_stage_layout_name(::_CollectStageExecutor) = :compacted_sequence
+_stage_layout_name(::_OrderedFoldStageExecutor) = :ordered_recurrence
+
+function _segment_materializations(law::LocalLaw, indices)
+    return Tuple(semantic_identity(component.field)
+        for index in indices
+        for publication in law.stages[index].publications
+        for component in publication.components
+        if component isa FieldPublication)
+end
+
+function _physical_segment_inspection(
+        launch::_PointwiseSegmentEntry, law::LocalLaw)
+    indices = map(member -> member.logical_index, launch.members)
+    source = law.stages[first(indices)].source
+    return (
+        logical_stages = indices,
+        family = :direct_pointwise,
+        launch_count = 1,
+        traversal = semantic_identity(source),
+        retained_materializations = launch.retained_materializations,
+        forwarded_values = launch.forwarded_values,
+        boundary_reason = launch.boundary_reason,
+    )
+end
+
+function _physical_segment_inspection(
+        entry::_StageLoweringEntry, law::LocalLaw)
+    index = entry.logical_index
+    phases = _planned_stage_phases(entry)
+    return (
+        logical_stages = (index,),
+        family = _stage_layout_name(entry.executor),
+        launch_count = _phase_count(phases),
+        traversal = semantic_identity(law.stages[index].source),
+        retained_materializations = _segment_materializations(law, (index,)),
+        forwarded_values = (),
+        boundary_reason = :semantic_barrier,
+    )
+end
+
+function _stage_planning_inspection(entry::_StageLoweringEntry,
+        stage::Stage, phases)
+    executor = _stage_executor_name(entry.executor)
+    layout = _stage_layout_name(entry.executor)
+    parameter_slots = entry.admission.stage.parameter_slots
+    prefix_slot = _stage_control_parameter_slot(
+        entry.admission.stage.control.prefix)
+    gate_slot = _stage_control_parameter_slot(
+        entry.admission.stage.control.gate)
+    projection = (
+        evaluator = map(slot -> typeof(slot).parameters[1], parameter_slots),
+        prefix = prefix_slot === nothing ? nothing :
+            typeof(prefix_slot).parameters[1],
+        gate = gate_slot === nothing ? nothing :
+            typeof(gate_slot).parameters[1],
+    )
+    specialization = (
+        executor = typeof(entry.executor),
+        evaluator_signature = entry.admission.signature,
+        result_type = entry.admission.result_type,
+        publication_types = map(typeof,
+            entry.admission.stage.publications),
+        parameter_projection = projection,
+    )
+    return (
+        executor,
+        layout,
+        evaluator_signature = entry.admission.signature,
+        evaluator_result_type = entry.admission.result_type,
+        specialization_signature = specialization,
+        relationship_receipts = map(entry.context.dynamic_relations,
+                entry.relation_dependencies) do identity, dependency
+            (relation = identity,
+                content_validation = !(
+                    dependency.validator isa _NoRelationContentValidator))
+        end,
+        relation_uses = _stage_relation_uses(stage),
+        workspace_paths = (map(leaf -> leaf.path,
+                entry.workspace.leaves)...,
+            map(leaf -> leaf.path, entry.relation_receipts.leaves)...),
+        phases,
+    )
+end
+
+function _plan_inspection(plan::Plan, lifecycle::Symbol;
+        prepared = nothing)
+    law = plan.bound.law
+    _, relations, _ = _law_descriptor_requirements(law)
+    binding = plan.bound.binding
+    proofs = map(relations) do relation
+        identity = semantic_identity(relation)
+        for index in eachindex(binding.relations)
+            candidate = binding.relations[index].relation
+            semantic_identity(candidate) == identity || continue
+            candidate == relation || throw(LocalMathValidationError(
+                "inspection found a relation identity with conflicting schema";
+                stage = :inspect, contract = :relation_schema_identity,
+                expected = relation, actual = candidate))
+            return binding.proofs[index]
+        end
+        throw(LocalMathValidationError(
+            "inspection could not find the validated relation proof";
+            stage = :inspect, contract = :relation_proof,
+            expected = identity, actual = :missing))
+    end
+    stages = Any[]
+    phase_values = Any[]
+    logical_entries = _logical_lowering_entries(plan.lowering)
+    for (index, entry) in enumerate(logical_entries)
+        semantic = law.stages[index]
+        phases = _planned_stage_phases(entry)
+        push!(phase_values, phases)
+        stage_planning = _stage_planning_inspection(entry, semantic, phases)
+        dependencies = _stage_planning_entry(
+            plan.bound, index).dependencies
+        push!(stages, _semantic_stage_inspection(semantic, index;
+            dependencies,
+            planning = stage_planning))
+    end
+    workspace = prepared === nothing ?
+        _workspace_requirement_facts(plan.lowering) :
+        _workspace_requirement_facts(plan.lowering,
+            length(prepared.leases))
+    physical_segments = map(plan.lowering.launches) do launch
+        _physical_segment_inspection(launch, law)
+    end
+    stage_local = sum(segment -> segment.launch_count,
+        physical_segments; init = 0)
+    program_phases = _program_phases(plan.lowering)
+    program_reset_count = _phase_count(program_phases)
+    planning = (
+        backend_environment = _backend_environment(plan.backend),
+        compiler = _lowering_identity(plan.lowering),
+        workspace,
+        workspace_bytes = sum(fact.bytes for fact in workspace; init = 0),
+        program_phases,
+        stage_phases = Tuple(phase_values),
+        physical_segments = Tuple(physical_segments),
+        stage_local_launch_count = stage_local,
+        program_reset_count,
+        base_provider_launch_count = stage_local + program_reset_count,
+    )
+    return (
+        lifecycle,
+        parameters = map(_parameter_inspection,
+            law.parameters.declarations),
+        relations = map(_relation_inspection, relations, proofs),
+        stages = Tuple(stages),
+        planning,
+        equivalence = _semantic_equivalence(law),
+    )
+end
+
 """
     LocalMath.inspect(plan::Plan)
 
diff --git a/src/execution/stage_program.jl b/src/execution/stage_program.jl
index 34295f7..8907023 100644
--- a/src/execution/stage_program.jl
+++ b/src/execution/stage_program.jl
@@ -1469,576 +1469,3 @@ function prepare(law::LocalLaw, bindings::Pair...;
     planned = plan(bound; backend)
     return prepare(planned; workspace, lease_capacity, dependency_arity)
 end
-
-@inline function _stage_parameter_slot_inspection(
-        slot::_StageParameterSlot{T}) where {T}
-    bounds = slot.bounds isa _ClosedParameterBounds ?
-        (lower = slot.bounds.lower, upper = slot.bounds.upper) : nothing
-    return (name = slot.name, type = T, bounds)
-end
-_stage_parameter_layout_inspection(layout::_StageParameterLayout) =
-    map(_stage_parameter_slot_inspection, layout.slots)
-
-_lowering_identity(::_StageProgramLowering) =
-    :stage_local_erased_kernelabstractions_v1
-
-_parameter_inspection(declaration::Parameter) = (
-    name = declaration.name,
-    type = _parameter_type(declaration),
-    bounds = declaration.bounds isa _ClosedParameterBounds ?
-        (lower = declaration.bounds.lower,
-            upper = declaration.bounds.upper) : nothing,
-)
-
-_space_kind_inspection(::Space{_IndexSpaceKind}) = :index
-_space_kind_inspection(::Space{_ProductSpaceKind}) = :product
-_space_kind_inspection(::Space{K}) where {K} = K
-_space_structure_inspection(::Space{K,N,_PlainSpaceStructure}) where {K,N} = nothing
-_space_structure_inspection(
-        space::Space{_ProductSpaceKind,N,S}) where {N,S<:_ProductSpaceStructure} =
-    (factors = map(_space_inspection, _space_factors(space)),)
-
-_space_inspection(space::Space) = (
-    identity = semantic_identity(space),
-    kind = _space_kind_inspection(space),
-    extent = size(space),
-    structure = _space_structure_inspection(space),
-)
-
-_relation_representation_inspection(::_IdentityRelation) = (family = :identity,)
-_relation_representation_inspection(value::_AffineRelation) =
-    (family = :affine, offsets = value.offsets, origin = value.origin)
-_relation_representation_inspection(value::_FixedRelation) =
-    (family = :fixed, degree = value.degree)
-_relation_representation_inspection(value::_ProductRelation) =
-    (family = :product, factors = map(semantic_identity, value.factors),
-        degree = value.degree)
-_relation_representation_inspection(value::_ComposedRelation) =
-    (family = :composed, factors = map(semantic_identity, value.factors),
-        degree = value.degree)
-_relation_representation_inspection(value::_BoundaryRelation) =
-    (family = :boundary, base = semantic_identity(value.base),
-        policy = _boundary_policy_facts(value.policy), degree = value.degree)
-_relation_representation_inspection(value::_RuntimeRelation) =
-    (family = :runtime, degree = value.degree, key_type = value.key_type,
-        ownership = value.ownership)
-_relation_representation_inspection(value::_FieldIndexRelation) =
-    (family = :field_index, keys = semantic_identity(value.keys),
-        degree = value.degree, optional = value.optional)
-_relation_representation_inspection(value::_MaskedRelation) =
-    (family = :masked, base = semantic_identity(value.base),
-        mask = semantic_identity(value.mask), degree = value.degree)
-_relation_representation_inspection(value::_SelectedRelation) =
-    (family = :selected, base = semantic_identity(value.base),
-        injection = semantic_identity(value.injection), degree = value.degree)
-_relation_representation_inspection(value::_InverseRelation) =
-    (family = :inverse, forward = semantic_identity(value.forward),
-        degree = value.degree)
-_relation_representation_inspection(value::_PackedRelation) =
-    (family = :packed, degree = value.degree, capacity = value.capacity,
-        layout = value.layout, ownership = value.ownership)
-
-_relation_footprint_inspection(relation::Relation{_IdentityRelation}) =
-    (strength = :exact, kind = :identity)
-_relation_footprint_inspection(relation::Relation{<:_AffineRelation}) =
-    merge((strength = :exact,), _relation_footprint(relation))
-function _relation_footprint_inspection(
-        relation::Relation{<:_BoundaryRelation})
-    relation.representation.base.representation isa _AffineRelation ||
-        return merge((strength = :bounded,), _relation_footprint(relation))
-    return merge((strength = :exact,), _relation_footprint(relation))
-end
-_relation_footprint_inspection(
-        relation::Relation{<:Union{_RuntimeRelation,_PackedRelation}}) =
-    (strength = :opaque, kind = :runtime_bounded,
-        degree = degree_bound(relation))
-_relation_footprint_inspection(relation::Relation{<:_FieldIndexRelation}) =
-    (strength = :opaque, kind = :bounded_indirect,
-        degree = degree_bound(relation),
-        keys = semantic_identity(relation.representation.keys))
-_relation_footprint_inspection(relation::Relation) =
-    merge((strength = :bounded,), _relation_footprint(relation))
-
-_ownership_inspection(::_ComputedOwnership) = :computed
-_ownership_inspection(::_LocalOwnership) = :local
-_ownership_inspection(::_SharedOwnership) = :shared
-_ownership_inspection(::_GhostOwnership) = :ghost
-_ownership_inspection(::_ExternalOwnership) = :external
-_ownership_inspection(::_TemporaryOwnership) = :temporary
-
-function _relation_inspection(relation::Relation, proof)
-    proof_value = proof === nothing ? nothing : (
-        ownership = _ownership_inspection(proof.binding_schema.ownership),
-        bounds = proof.evidence.bounds,
-        multiplicity = proof.evidence.multiplicity,
-        coverage = proof.evidence.coverage,
-        canonical_order = proof.evidence.canonical_order,
-        physical_representation = proof.binding_schema.representation,
-        physical_leaves = proof.binding_schema.physical_leaves,
-    )
-    return (
-        identity = semantic_identity(relation),
-        domain = semantic_identity(domain(relation)),
-        codomain = semantic_identity(codomain(relation)),
-        schema_epoch = schema_epoch(relation),
-        representation = _relation_representation_inspection(
-            relation.representation),
-        proof = proof_value,
-        footprint = _relation_footprint_inspection(relation),
-    )
-end
-
-_collection_access_law_inspection(::_BoundedGroup{K}) where {K} =
-    (kind = :bounded_group, maximum = K)
-_collection_access_law_inspection(::_SourcePositionsAccess{K,L}) where {K,L} =
-    (kind = :source_position, width = K, lane = L)
-
-_dependency_inspection(::Nothing) = nothing
-_dependency_inspection(value::_ExternalFieldDependency) =
-    (kind = :external, resource = :field, identity = value.field_id)
-_dependency_inspection(value::_PrecedingFieldDependency) =
-    (kind = :stage, resource = :field, identity = value.field_id,
-        stage = value.stage)
-_dependency_inspection(value::_PrecedingCollectionDependency) =
-    (kind = :stage, resource = :collection,
-        identity = value.collection_id, stage = value.stage,
-        role = value.role)
-_dependency_inspection(value::_RelationUse) =
-    (kind = :relation, identity = value.relation_id)
-
-function _read_inspection(role::Symbol, access::Access, dependency = nothing)
-    return (
-        role,
-        kind = :field,
-        identity = semantic_identity(access.field),
-        value_type = eltype(access.field),
-        space = semantic_identity(access.field.space),
-        relation = semantic_identity(access.relation),
-        version = :stage_entry,
-        mode = access.mode isa _RequiredAccess ? :required : :samples,
-        ghost = access.ghost === nothing ? nothing :
-            semantic_identity(access.ghost),
-        producer = _dependency_inspection(dependency),
-    )
-end
-function _read_inspection(
-        role::Symbol, access::CollectionAccess, dependency = nothing)
-    return (
-        role,
-        kind = :collection,
-        identity = semantic_identity(access.collection),
-        value_type = eltype(access.collection),
-        capacity = access.collection.capacity,
-        law = _collection_access_law_inspection(access.law),
-        producer = _dependency_inspection(dependency),
-    )
-end
-
-_control_part_inspection(::_NoPrefix) = (kind = :none,)
-_control_part_inspection(value::_ParameterPrefix) =
-    (kind = :parameter, parameter = value.parameter.name)
-_control_part_inspection(value::_FieldPrefix) =
-    (kind = :field, identity = semantic_identity(value.field))
-_control_part_inspection(value::_CollectionCount) =
-    (kind = :collection_count,
-        identity = semantic_identity(value.collection))
-_control_part_inspection(::_NoMask) = (kind = :none,)
-_control_part_inspection(value::_MaskSelection) =
-    (kind = :field, identity = semantic_identity(value.field))
-_control_part_inspection(::_NoSubset) = (kind = :none,)
-_control_part_inspection(value::_SubsetSelection) =
-    (kind = :relation, identity = semantic_identity(value.relation))
-_control_part_inspection(::_NoGate) = (kind = :none,)
-_control_part_inspection(value::_ParameterGate) =
-    (kind = :parameter, parameter = value.parameter.name)
-_control_part_inspection(value::_FieldGate) =
-    (kind = :field, identity = semantic_identity(value.field))
-_control_part_with_producer(value, ::Nothing) =
-    _control_part_inspection(value)
-_control_part_with_producer(value, dependency) = merge(
-    _control_part_inspection(value),
-    (producer = _dependency_inspection(dependency),),
-)
-function _control_inspection(control::Control, dependencies = nothing)
-    producers = dependencies === nothing ?
-        (prefix = nothing, mask = nothing, subset = nothing, gate = nothing) :
-        (prefix = dependencies.collection_prefix === nothing ?
-                dependencies.control.prefix : dependencies.collection_prefix,
-            mask = dependencies.control.mask,
-            subset = dependencies.control.subset,
-            gate = dependencies.control.gate)
-    return (
-        prefix = _control_part_with_producer(
-            control.prefix, producers.prefix),
-        mask = _control_part_with_producer(control.mask, producers.mask),
-        subset = _control_part_with_producer(
-            control.subset, producers.subset),
-        gate = _control_part_with_producer(control.gate, producers.gate),
-    )
-end
-
-function _stage_reads_inspection(stage::Stage, dependencies = nothing)
-    names = keys(stage.accesses)
-    access_values = Base.values(stage.accesses)
-    dependency_values = dependencies === nothing ?
-        ntuple(_ -> nothing, length(access_values)) :
-        Base.values(dependencies.accesses)
-    reads = Any[ntuple(index -> _read_inspection(
-            names[index], access_values[index], dependency_values[index]),
-        length(access_values))...]
-    for publication in stage.publications
-        publication.law isa OrderedFold || continue
-        state_dependencies = dependencies === nothing ? nothing :
-            dependencies.state
-        state_names = keys(publication.law.state.components)
-        for (index, component) in enumerate(
-                values(publication.law.state.components))
-            field = component.source isa _FoldInPlace ?
-                component.target : component.source
-            dependency = state_dependencies === nothing ? nothing : begin
-                pair = getfield(state_dependencies, index)
-                component.source isa _FoldInPlace ? pair.target : pair.source
-            end
-            push!(reads, (
-                role = Symbol(:fold_state_, state_names[index]),
-                kind = :fold_state,
-                identity = semantic_identity(field),
-                value_type = eltype(field),
-                space = semantic_identity(field.space),
-                relation = nothing,
-                version = :stage_entry,
-                ghost = nothing,
-                producer = _dependency_inspection(dependency),
-            ))
-        end
-    end
-    return Tuple(reads)
-end
-
-function _stage_relation_uses(stage::Stage)
-    uses = Any[]
-    for access in values(stage.accesses)
-        access isa Access && push!(uses, (
-            relation = semantic_identity(access.relation), direction = :read))
-    end
-    for publication in stage.publications, component in publication.components
-        component isa FieldPublication && push!(uses, (
-            relation = semantic_identity(component.relation),
-            direction = :publication))
-    end
-    stage.control.subset isa _SubsetSelection && push!(uses, (
-        relation = semantic_identity(stage.control.subset.relation),
-        direction = :control))
-    return Tuple(unique(uses))
-end
-
-function _semantic_stage_inspection(stage::Stage, index::Int;
-        dependencies = nothing, planning = nothing)
-    return (
-        index,
-        source = _space_inspection(stage.source),
-        origin = stage.origin,
-        reads = _stage_reads_inspection(stage, dependencies),
-        control = _control_inspection(stage.control, dependencies),
-        publications = map(_stage_publication_context, stage.publications),
-        planning,
-    )
-end
-
-function _semantic_equivalence(law::LocalLaw)
-    _, relations, _ = _law_descriptor_requirements(law)
-    stages = Tuple(map(enumerate(law.stages)) do (index, stage)
-        report = _semantic_stage_inspection(stage, index)
-        publications = map(report.publications) do publication
-            merge(publication, (origin = nothing,))
-        end
-        return merge(report,
-            (origin = nothing, publications, planning = nothing))
-    end)
-    return (
-        parameters = map(_parameter_inspection,
-            law.parameters.declarations),
-        relations = map(relation -> _relation_inspection(relation, nothing),
-            relations),
-        stages,
-        evaluators = map(stage -> (
-                value = stage.evaluator.evaluator,
-                type = typeof(stage.evaluator.evaluator),
-                parameters = map(_parameter_inspection,
-                    stage.evaluator.parameters),
-            ), law.stages),
-    )
-end
-
-function _inspect_local_law(law::LocalLaw)
-    _, relations, _ = _law_descriptor_requirements(law)
-    return (
-        lifecycle = :LocalLaw,
-        parameters = map(_parameter_inspection,
-            law.parameters.declarations),
-        relations = map(relation -> _relation_inspection(relation, nothing),
-            relations),
-        stages = Tuple(map(enumerate(law.stages)) do (index, stage)
-            _semantic_stage_inspection(stage, index)
-        end),
-        planning = nothing,
-        equivalence = _semantic_equivalence(law),
-    )
-end
-
-function _planned_relation_phases(entry::_StageLoweringEntry;
-        reset_fused::Bool = false)
-    isempty(entry.relation_dependencies) && return ()
-    validators = count(dependency ->
-        !(dependency.validator isa _NoRelationContentValidator),
-        entry.relation_dependencies)
-    launches_per_validator = reset_fused ? 2 : 3
-    validation = validators == 0 ? () :
-        (_phase_fact(:relationship_validation,
-            launches_per_validator * validators),)
-    return (validation..., _phase_fact(:relationship_receipt))
-end
-
-_planned_stage_phases(entry::_StageLoweringEntry{
-        A,W,<:_CandidateStageExecutor{<:_DirectIdentityUniqueLayout}}) where {A,W} =
-    (_phase_fact(:direct_identity_unique),)
-function _planned_stage_phases(entry::_StageLoweringEntry{
-        A,W,<:_CandidateStageExecutor{<:_GroupedCandidateLayout}}) where {A,W}
-    phases = Any[_phase_fact(:candidate_reset)]
-    append!(phases, _planned_relation_phases(entry; reset_fused = true))
-    push!(phases, _phase_fact(:candidate_evaluate))
-    for shape in entry.workspace.ports
-        if hasproperty(shape, :atomic_selection)
-            push!(phases, _phase_fact(:resolve_atomic_winner))
-            continue
-        end
-        hasproperty(shape, :grouping_shape) || continue
-        push!(phases, _phase_fact(:destination_grouping_local_sort))
-        shape.grouping_shape.merge_passes == 0 || push!(phases,
-            _phase_fact(:destination_grouping_merge,
-                shape.grouping_shape.merge_passes))
-        push!(phases, _phase_fact(:destination_grouping_directory))
-    end
-    push!(phases, _phase_fact(:candidate_validate))
-    publications = entry.admission.stage.publications
-    _candidate_phase_required(publications,
-        _candidate_atomic_initialization_required) && push!(phases,
-            _phase_fact(:candidate_atomic_initialize))
-    _candidate_phase_required(publications,
-        _candidate_atomic_required) && push!(phases,
-            _phase_fact(:candidate_atomic))
-    push!(phases, _phase_fact(:candidate_finalize_publish))
-    return Tuple(phases)
-end
-function _planned_stage_phases(entry::_StageLoweringEntry{
-        A,W,<:_CollectStageExecutor}) where {A,W}
-    phases = Any[_phase_fact(:collect_reset)]
-    append!(phases, _planned_relation_phases(entry))
-    push!(phases, _phase_fact(:collect_evaluate))
-    for port in entry.workspace.ports
-        items = div(Int(port.candidate_count), _collect_width(port))
-        levels = _collect_scan_level_count(items)
-        push!(phases, _phase_fact(:collect_scan_block, levels))
-        levels == 1 || push!(phases,
-            _phase_fact(:collect_scan_add, levels - 1))
-    end
-    for port in entry.workspace.ports
-        push!(phases, _phase_fact(:collect_scatter))
-        port.sort_required || continue
-        push!(phases, _phase_fact(:collect_local_bitonic))
-        port.merge_passes == 0 || push!(phases,
-            _phase_fact(:collect_merge, port.merge_passes))
-        _is_grouped(port.groups) && push!(phases,
-            _phase_fact(:collect_directory))
-        _is_canonical_order(port.order) && push!(phases,
-            _phase_fact(:collect_validate_order))
-    end
-    append!(phases, (_phase_fact(:collect_finalize),
-        _phase_fact(:collect_publish,
-            cld(length(entry.admission.stage.publications),
-                _POINTWISE_SEGMENT_LIMIT))))
-    return Tuple(phases)
-end
-function _planned_stage_phases(entry::_StageLoweringEntry{
-        A,W,<:_OrderedFoldStageExecutor}) where {A,W}
-    phases = Any[_phase_fact(:ordered_fold_reset)]
-    append!(phases, _planned_relation_phases(entry))
-    push!(phases, _phase_fact(:ordered_fold_evaluate))
-    extent = nextpow(2, max(Int(entry.admission.stage.source_count), 1))
-    bitonic = 0
-    width = 2
-    while width <= extent
-        distance = width >>> 1
-        while distance >= 1
-            bitonic += 1
-            distance >>>= 1
-        end
-        width <<= 1
-    end
-    bitonic == 0 || push!(phases,
-        _phase_fact(:ordered_fold_bitonic, bitonic))
-    append!(phases, (_phase_fact(:ordered_fold_validate_initialize),
-        _phase_fact(:ordered_fold_apply),
-        _phase_fact(:ordered_fold_finalize)))
-    return Tuple(phases)
-end
-
-_phase_count(phases) = sum(phase.count for phase in phases; init = 0)
-
-_stage_layout_name(::_CandidateStageExecutor{<:_GroupedCandidateLayout}) =
-    :grouped_candidate
-_stage_layout_name(::_CandidateStageExecutor{<:_DirectIdentityUniqueLayout}) =
-    :direct_identity_unique
-_stage_layout_name(::_CollectStageExecutor) = :compacted_sequence
-_stage_layout_name(::_OrderedFoldStageExecutor) = :ordered_recurrence
-
-function _segment_materializations(law::LocalLaw, indices)
-    return Tuple(semantic_identity(component.field)
-        for index in indices
-        for publication in law.stages[index].publications
-        for component in publication.components
-        if component isa FieldPublication)
-end
-
-function _physical_segment_inspection(
-        launch::_PointwiseSegmentEntry, law::LocalLaw)
-    indices = map(member -> member.logical_index, launch.members)
-    source = law.stages[first(indices)].source
-    return (
-        logical_stages = indices,
-        family = :direct_pointwise,
-        launch_count = 1,
-        traversal = semantic_identity(source),
-        retained_materializations = launch.retained_materializations,
-        forwarded_values = launch.forwarded_values,
-        boundary_reason = launch.boundary_reason,
-    )
-end
-
-function _physical_segment_inspection(
-        entry::_StageLoweringEntry, law::LocalLaw)
-    index = entry.logical_index
-    phases = _planned_stage_phases(entry)
-    return (
-        logical_stages = (index,),
-        family = _stage_layout_name(entry.executor),
-        launch_count = _phase_count(phases),
-        traversal = semantic_identity(law.stages[index].source),
-        retained_materializations = _segment_materializations(law, (index,)),
-        forwarded_values = (),
-        boundary_reason = :semantic_barrier,
-    )
-end
-
-function _stage_planning_inspection(entry::_StageLoweringEntry,
-        stage::Stage, phases)
-    executor = _stage_executor_name(entry.executor)
-    layout = _stage_layout_name(entry.executor)
-    parameter_slots = entry.admission.stage.parameter_slots
-    prefix_slot = _stage_control_parameter_slot(
-        entry.admission.stage.control.prefix)
-    gate_slot = _stage_control_parameter_slot(
-        entry.admission.stage.control.gate)
-    projection = (
-        evaluator = map(slot -> typeof(slot).parameters[1], parameter_slots),
-        prefix = prefix_slot === nothing ? nothing :
-            typeof(prefix_slot).parameters[1],
-        gate = gate_slot === nothing ? nothing :
-            typeof(gate_slot).parameters[1],
-    )
-    specialization = (
-        executor = typeof(entry.executor),
-        evaluator_signature = entry.admission.signature,
-        result_type = entry.admission.result_type,
-        publication_types = map(typeof,
-            entry.admission.stage.publications),
-        parameter_projection = projection,
-    )
-    return (
-        executor,
-        layout,
-        evaluator_signature = entry.admission.signature,
-        evaluator_result_type = entry.admission.result_type,
-        specialization_signature = specialization,
-        relationship_receipts = map(entry.context.dynamic_relations,
-                entry.relation_dependencies) do identity, dependency
-            (relation = identity,
-                content_validation = !(
-                    dependency.validator isa _NoRelationContentValidator))
-        end,
-        relation_uses = _stage_relation_uses(stage),
-        workspace_paths = (map(leaf -> leaf.path,
-                entry.workspace.leaves)...,
-            map(leaf -> leaf.path, entry.relation_receipts.leaves)...),
-        phases,
-    )
-end
-
-function _plan_inspection(plan::Plan, lifecycle::Symbol;
-        prepared = nothing)
-    law = plan.bound.law
-    _, relations, _ = _law_descriptor_requirements(law)
-    binding = plan.bound.binding
-    proofs = map(relations) do relation
-        identity = semantic_identity(relation)
-        for index in eachindex(binding.relations)
-            candidate = binding.relations[index].relation
-            semantic_identity(candidate) == identity || continue
-            candidate == relation || throw(LocalMathValidationError(
-                "inspection found a relation identity with conflicting schema";
-                stage = :inspect, contract = :relation_schema_identity,
-                expected = relation, actual = candidate))
-            return binding.proofs[index]
-        end
-        throw(LocalMathValidationError(
-            "inspection could not find the validated relation proof";
-            stage = :inspect, contract = :relation_proof,
-            expected = identity, actual = :missing))
-    end
-    stages = Any[]
-    phase_values = Any[]
-    logical_entries = _logical_lowering_entries(plan.lowering)
-    for (index, entry) in enumerate(logical_entries)
-        semantic = law.stages[index]
-        phases = _planned_stage_phases(entry)
-        push!(phase_values, phases)
-        stage_planning = _stage_planning_inspection(entry, semantic, phases)
-        dependencies = _stage_planning_entry(
-            plan.bound, index).dependencies
-        push!(stages, _semantic_stage_inspection(semantic, index;
-            dependencies,
-            planning = stage_planning))
-    end
-    workspace = prepared === nothing ?
-        _workspace_requirement_facts(plan.lowering) :
-        _workspace_requirement_facts(plan.lowering,
-            length(prepared.leases))
-    physical_segments = map(plan.lowering.launches) do launch
-        _physical_segment_inspection(launch, law)
-    end
-    stage_local = sum(segment -> segment.launch_count,
-        physical_segments; init = 0)
-    program_phases = _program_phases(plan.lowering)
-    program_reset_count = _phase_count(program_phases)
-    planning = (
-        backend_environment = _backend_environment(plan.backend),
-        compiler = _lowering_identity(plan.lowering),
-        workspace,
-        workspace_bytes = sum(fact.bytes for fact in workspace; init = 0),
-        program_phases,
-        stage_phases = Tuple(phase_values),
-        physical_segments = Tuple(physical_segments),
-        stage_local_launch_count = stage_local,
-        program_reset_count,
-        base_provider_launch_count = stage_local + program_reset_count,
-    )
-    return (
-        lifecycle,
-        parameters = map(_parameter_inspection,
-            law.parameters.declarations),
-        relations = map(_relation_inspection, relations, proofs),
-        stages = Tuple(stages),
-        planning,
-        equivalence = _semantic_equivalence(law),
-    )
-end
diff --git a/src/inspection.jl b/src/inspection.jl
index 960a930..00283b3 100644
--- a/src/inspection.jl
+++ b/src/inspection.jl
@@ -138,7 +138,15 @@ function _show_space_summary(io::IO, space::Space; identity::Bool = true)
     print(io, "Space(extent=")
     show(io, size(space))
     kind = space_kind(space)
-    kind === _IndexSpaceKind || print(io, ", kind=", nameof(kind))
+    if kind === _ProductSpaceKind
+        factors = _space_factors(space)
+        print(io, ", kind=:product, factor_extents=")
+        show(io, map(size, factors))
+        print(io, ", factor_ids=")
+        show(io, map(_short_semantic_identity, factors))
+    elseif kind !== _IndexSpaceKind
+        print(io, ", kind=", nameof(kind))
+    end
     identity && print(io, ", id=", _short_semantic_identity(space))
     print(io, ")")
 end
diff --git a/test/test_descriptor_presentation.jl b/test/test_descriptor_presentation.jl
index c1eafc3..ae61d9c 100644
--- a/test/test_descriptor_presentation.jl
+++ b/test/test_descriptor_presentation.jl
@@ -6,6 +6,8 @@ const LMDP = LocalMath
 
 @testset "semantic descriptors have compact mathematical displays" begin
     cells = LMDP.Space((4, 5))
+    factors = (LMDP.Space(2), LMDP.Space(3))
+    product = LMDP.Space(factors)
     values = LMDP.Field(cells, Float32)
     fixed = LMDP.FixedRelation(cells => cells; degree = 4)
     keys = LMDP.Field(cells, NTuple{2,Int32})
@@ -17,6 +19,7 @@ const LMDP = LocalMath
     records = LMDP.Collection(Tuple{Int32,Float32}, 12)
 
     space_text = sprint(show, cells)
+    product_text = sprint(show, product)
     field_text = sprint(show, values)
     fixed_text = sprint(show, fixed)
     indexed_text = sprint(show, indexed)
@@ -25,6 +28,10 @@ const LMDP = LocalMath
     detailed_relation = sprint(show, MIME("text/plain"), fixed)
 
     @test occursin("extent=(4, 5)", space_text)
+    @test occursin("kind=:product", product_text)
+    @test occursin("factor_extents=((2,), (3,))", product_text)
+    @test occursin("factor_ids=", product_text)
+    @test !occursin("_ProductSpaceKind", product_text)
     @test occursin("Field(Float32", field_text)
     @test occursin("FixedRelation", fixed_text)
     @test occursin("degree=4", fixed_text)