Manuscript En02-A@1 · En02-A-v1.tex · proposition · bb1319d5

Proposition: Preservation and the geometric diamond

Resource geometry, ownership, and legal updates › The update grammar · lines 718–742 · proof included or linked

En02-A@1#prop:diamond

Back to manuscript

Legal primitive moves preserve geometric well-formedness and the occupancy bound. Independent geometric transitions commute. For the specified Born quantum semantics, a pair of name-disjoint quantum redexes equipped with independent geometric transitions has the concrete probabilistic diamond.

Proof. Capacity retirement leaves capacity at least occupancy. Deletion preserves acyclicity. Activation preserves it by its guard and preserves identifier uniqueness by moving, rather than copying, the link identifier.

For independent transitions, neither writes data used by the other, and neither invalidates the other's guard. Each therefore produces the same update on its own write footprint in either order. Outside their union both act identically.

The Born quantum diamond follows from the commuting destructive components, disjoint gates, and fresh-name identification. Its joint branch weights are the same in both orders. Combine that equality with the geometric commutation just proved.

Nearby in this section