# Information System Model — Formal Semantics

*Note: For the interested reader, this section provides the rigorous mathematical foundation for the IS-Model, combining Type Theory for structural definitions and Set Theory for multi-tenant Context topologies. The uninterested reader can skip this chapter because the core concepts have already been described narratively in the previous sections.*

## Type Theory

Following standard type theory notation (e.g., Pierce), we formalize the structural constraints of the model. The graph model is rooted in two absolute base abstract Types: **Entity** and **Relation**. *(Note: The **`Property`** base Type, which governs embedded values, exists outside this topological instance model since its data fields lack an independent graph identity).*

### Typing Relation

```eval_rst
Let :math:`x` be a concrete instance in the graph. We define two distinct predicates to separate the native structural shape from polymorphic conformance:
```

```eval_rst
1. **Declared Type:** We write :math:`\text{declaredType}(x) = T` to indicate the exact concrete Type :math:`T` assigned to the instance at creation.
2. **Subtype Conformance:** We write :math:`x \models U` to indicate that :math:`x` conforms to Type :math:`U`.
```

```eval_rst
**Single Instantiation Rule:**
An instance is natively declared under exactly ONE concrete Type (which defines its base shape).

.. math::

   \text{declaredType}(x) = T \implies \forall T' \neq T, \text{declaredType}(x) \neq T'
```

### Subtyping (Inheritance)

```eval_rst
We write :math:`S <: T` to indicate that Type :math:`S` is a subtype (specialization) of Type :math:`T`.
Following the principle of safe substitution (Rule of Subsumption), any instance conforms to its declared Type and to all its supertypes:

.. math::

   x \models U \iff \text{declaredType}(x) <: U
```

```eval_rst
*(Note: Every type is trivially a subtype of itself, so* :math:`T <: T` *and* :math:`x \models \text{declaredType}(x)` *are always true).*
```

**Base Type Constraints:**

```eval_rst
- Let :math:`\mathbb{I}` be the set of all graph instance Types. A graph instance Type is exclusively either an **Entity** or a **Relation**.

.. math::

   \forall T \in \mathbb{I}, \quad T <: Entity \oplus T <: Relation
```

The foundation of the model defines four core topological Types descending from the graph base Types: **Resource** and **Facet** (descending from **Entity**), and **IsRelatedTo** and **ConsistsOf** (descending from **Relation**). Every concrete graph instance must be of a Type that extends one of these four (or, in the case of **ConsistsOf**, it can instantiate the base Type itself, as it is uniquely concrete among the foundational topologies).

**Core Type Constraints:**

```eval_rst
- **Resource** and **Facet** are mutually exclusive **Entity** branches.

.. math::

   T <: Entity \implies (T <: Resource \oplus T <: Facet)

- **IsRelatedTo** and **ConsistsOf** are mutually exclusive **Relation** branches.

.. math::

   T <: Relation \implies (T <: IsRelatedTo \oplus T <: ConsistsOf)

- **IsRelatedTo** strictly connects a source **Resource** to a target **Resource** (where :math:`IRT` denotes an **IsRelatedTo** schema definition):

.. math::

   IRT <: IsRelatedTo \implies \text{source}(IRT) <: Resource \land \text{target}(IRT) <: Resource

- **ConsistsOf** strictly connects a source **Resource** to a target **Facet** (where :math:`CO` denotes a **ConsistsOf** schema definition):

.. math::

   CO <: ConsistsOf \implies \text{source}(CO) <: Resource \land \text{target}(CO) <: Facet
```

### System Fields

```eval_rst
Every instance is formally equipped with base properties. We denote the existence of a property field :math:`p` on an instance :math:`x` as :math:`\exists p(x)`.
```

```eval_rst
- Universal Identification and Provenance:

.. math::

   \forall x : Entity \cup Relation, \exists \text{id}(x) \land \exists \text{metadata}(x)

- **Relation**-exclusive Behavior:

.. math::

   \forall e : Relation, \exists \text{propagationConstraint}(e)
```

### Formal Topological Uniqueness Invariants

To ensure deterministic operations, unambiguous garbage collection, and prevent "double-counting" during polymorphic queries, the IS-Model enforces the following structural uniqueness invariants on the global graph topology:

**1. Facet Exclusivity (Single Ownership):**
A **Facet** instance is intrinsically a characterizing aspect of a single **Resource** instance. It must be attached via exactly one **ConsistsOf** instance globally. In other words, a **Facet** instance cannot be attached to multiple **Resource** instances, nor can it be attached via multiple **ConsistsOf** instances to the same **Resource** instance.

```eval_rst
.. math::

   \forall f \mid \text{declaredType}(f) <: Facet, \quad \exists! e_{co} \mid \text{declaredType}(e_{co}) <: ConsistsOf \land \text{target}(e_{co}) = f

*(Note: Because* :math:`e_{co}` *is strictly unique for any given* :math:`f`\ *, the contextual dependency formula* :math:`C(f) = C(e_{co})` *is mathematically absolute).*
```

**2. IsRelatedTo Polymorphic Uniqueness:**
Two specific **Resource** instances cannot be linked via multiple **IsRelatedTo** instances belonging to the same polymorphic lineage. If two distinct **IsRelatedTo** instances link the exact same source and target **Resource** instances, neither **Relation** instance's Type can be a subtype of the other. This prevents semantic redundancy (e.g., preventing a generic `Hosts` relation and a specialized `MyHosts <: Hosts` relation from existing simultaneously linking the same two **Resource** instances). Re-asserting the same semantic connection through a more specialized type makes no sense; the correct operational pattern is to delete the generic relation and create the specialized one, since polymorphic queries (which are enabled by default) will still return it when querying the supertype.

```eval_rst
.. math::

   \forall e_1, e_2 \mid (\text{source}(e_1) = \text{source}(e_2) \land \text{target}(e_1) = \text{target}(e_2) \land e_1 \neq e_2) \implies \neg(\text{declaredType}(e_1) <: \text{declaredType}(e_2) \lor \text{declaredType}(e_2) <: \text{declaredType}(e_1))

Conversely, parallel **IsRelatedTo** instances linking the same two **Resource** instances are explicitly permitted if they belong to entirely orthogonal polymorphic branches (e.g., a ``Discovers`` relation and a ``Uses`` relation), as they capture orthogonally distinct semantic interactions.
```

## Set Theory for Context Membership

The multi-tenant nature of the IS-Model is underpinned by set theory rules governing Context membership for concrete instances.

```eval_rst
Let :math:`C(x)` represent the set of Contexts to which an instance :math:`x` (an **Entity** instance or a **Relation** instance) belongs.
```

### General Relation Context Intersection

```eval_rst
For *any* **Relation** instance :math:`e` (whether **IsRelatedTo** or **ConsistsOf**) linking a source **Resource** instance :math:`r` to a target **Entity** instance :math:`t`, the **Relation** instance can only exist in Contexts where **both** the source and target instances exist.

.. math::

   C(e) \subseteq C(r) \cap C(t)

*Explanation: You cannot define a **Relation** instance in a Context if one of its two endpoints is missing from that Context. The **Relation** instance is strictly constrained by the intersection of the visibility of the two instances it connects.*
*Specifically for **IsRelatedTo** instances, their presence is strictly bounded by this intersection rule, but they are not automatically present just because the intersection exists. They require explicit mathematical addition to the Context set. Even if two **Resource** instances share multiple Contexts, the link between them only exists in the specific subset of those Contexts where it was explicitly created or added. It is not an implicit auto-join.*
```

### Facet Context Dependency

```eval_rst
A **Facet** instance :math:`f` is intrinsically tied to the **ConsistsOf** instance :math:`e_{co}` that connects it to its parent **Resource** instance :math:`r`. A **Facet** instance cannot exist independently of this **ConsistsOf** instance.

.. math::

   C(f) = C(e_{co})

By applying the general intersection rule, it follows that the **Facet** instance can only exist in a subset of the Contexts where its parent **Resource** instance exists:

.. math::

   C(f) \subseteq C(r)

*Explanation: It is mathematically impossible for a **Facet** instance to exist in a Context without its parent **Resource** instance.*
```

### Resource Context Union

```eval_rst
The presence of a **Resource** instance :math:`r` in a Context is exactly the union of all Contexts of its attached **Facet** instances :math:`f_i`.

.. math::

   C(r) = \bigcup_{i} C(f_i)

*Explanation: A **Resource** instance exists in a Context if and only if it has at least one **Facet** instance in that Context.*
```

### Avalanche State Transitions

```eval_rst
Let :math:`e` be a **Relation** instance with source :math:`r` and target :math:`t`. We denote the propagation constraints as :math:`e_{add}` and :math:`e_{remove}`. Let :math:`C_{src}` be the context from which the instance is being shared, and :math:`C_n` be the destination Context.
```

```eval_rst
- **Add Propagation:** Adding :math:`r` to :math:`C_n` from :math:`C_{src}` implies adding both :math:`e` and :math:`t` to :math:`C_n` if the constraint is ``propagate`` and the relation is visible in the source Context.

.. math::

   \text{Add}(r, C_n \leftarrow C_{src}) \land C_{src} \in C(e) \land (e_{add} = propagate) \implies \text{Add}(t, C_n) \land \text{Add}(e, C_n)
```

```eval_rst
- **Direct Relation Add:** Adding a **Relation** instance directly to Context :math:`C_n` requires its source to already exist in :math:`C_n`. The target is automatically pulled into :math:`C_n` to satisfy the relation constraint, regardless of its ``add`` propagation constraint.

.. math::

   \text{Add}(e, C_n) \implies C_n \in C(r) \land \text{Add}(t, C_n)
```

```eval_rst
- **Topological Cleanup:** Removing an instance from Context :math:`C_n` automatically drops all connected **Relation** instances in :math:`C_n`.

.. math::

   \text{Remove}(x, C_n) \implies \forall e \mid (C_n \in C(e) \land (\text{source}(e) = x \lor \text{target}(e) = x)), \text{Remove}(e, C_n)
```

```eval_rst
- **Remove Propagation:** Removing :math:`r` from :math:`C_n` implies removing :math:`t` from :math:`C_n` if the constraint is ``cascade``. Let :math:`E_{rem}` be the set of relations being removed in the current transaction avalanche.

.. math::

   \text{Remove}(r, C_n) \land (e_{remove} = cascade) \implies \text{Remove}(t, C_n)

If the constraint is ``cascadeWhenOrphan``, :math:`t` is removed only if no other incoming **Relation** instances to :math:`t` exist in the candidate post-state of :math:`C_n`. *(Note: Since **ConsistsOf** instances can only target **Facet** instances, if* :math:`t` *is a **Resource** instance, the formula effectively only counts incoming **IsRelatedTo** instances).*

.. math::

   \text{Remove}(r, C_n) \land (e_{remove} = cascadeWhenOrphan) \land (\not\exists e' \mid C_n \in C(e') \land e' \notin E_{rem} \land \text{target}(e') = t) \implies \text{Remove}(t, C_n)
```

### Reference Counting

```eval_rst
An instance :math:`x` is physically destroyed from the global graph (Garbage Collected) if and only if the set of its Contexts becomes empty.

.. math::

   |C(x)| = 0 \iff C(x) = \emptyset \implies x \text{ is physically deleted}
```