# Arity Science knowledge base

The definitions the project has settled (maturity `stable`) and the claims made about them, exported from
the project's registry. Each claim has a status: `supported` (evidence, usually computational), `refuted`
(a counterexample), `proved` or `formalized` (a Lean proof). Mathematics is in LaTeX between `$` signs.
Machine-readable: https://arity.science/hyperiad/agents/catalog.json

## common

### Hyperedge (`common.hyperedge`)

A hyperedge is a list of vertices $(v_1, \dots, v_k)$ with a symmetry type: **directed** (the order matters), **cyclic** (the order matters up to rotation) or **unordered** (only the multiset of vertices matters), and optionally a label. $k$ is its arity; a vertex may repeat. An **input–output** hyperedge $(u_1, \dots, u_a \mid w_1, \dots, w_b)$ has an input block and an output block, $a, b \ge 1$, each with one of the three types, written `InputOutput(S:a,T:b)`; its orderings are those of each block within that block, and one input and one output is the directed binary edge. Its vertices are stored in the canonical order of its symmetry type, the least of its orbit, so two hyperedges are equal exactly when they are the same hyperedge.

Depends on: `common.vertex`

Implemented as: `frontier.hypergraphs.core.Edge`

### Hypergraph (`common.hypergraph`)

A hypergraph is a set of vertices together with a finite **multiset** of hyperedges on them: the order of the edges does not matter, their multiplicity does. Every vertex of an edge belongs to the vertex set, and a label given to a vertex anywhere is the label of that vertex everywhere. The *skeleton* forgets every vertex and edge label and keeps the symmetry types.

Depends on: `common.vertex`, `common.hyperedge`

Implemented as: `frontier.hypergraphs.core.Hypergraph`

### Hypergraph rewrite rule (`common.hypergraph_rule`)

A rewrite rule $L \to R$ is a pair of hypergraphs. A **match** of $L$ in $H$ is a map of $L$'s edges to edges of $H$ of the same arity and symmetry type (injective by default), with a vertex map (injective by default) carrying each edge of $L$ onto its image up to the edge's symmetry, and labels matched: a symbol in $L$ binds, a composite label holding symbols matches structurally (same head, arguments matched in turn), no label is a wildcard, anything else is literal. The **event** replaces the matched edges by $R$'s edges, with $R$'s new vertices freshly named and its labels written in the bindings; a vertex only $L$ has is removed only if no remaining edge uses it.

Depends on: `common.hypergraph`

Implemented as: `frontier.hypergraphs.rewriting.apply_rule`

### Vertex (`common.vertex`)

A vertex is an identifier, any value, optionally carrying a label. Two vertices are the same when their identifiers are; a label of `None` means unlabelled.

Implemented as: `frontier.hypergraphs.core.Vertex`

## hypermatrix

### Array (hypermatrix of order n) (`hypermatrix.array`)

An **$n$-array** is a rectangular family of entries $A = (a_{i_1 i_2 \dots i_n})$ with $1 \le i_k \le d_k$; $(d_1, \dots, d_n)$ are its *dimensions* and $n$ its *order*. A scalar is the array of order $0$. It is *regular* when all $d_k$ are equal. An array carries a declared index symmetry: **rigid** (none), **cyclic** (invariant under cyclic permutations of its indices) or **symmetric** (invariant under all permutations), verified against its entries; only regular arrays can be cyclic or symmetric. Its value domain is read off the entries, never declared.

Implemented as: `hypermatrix.arrays.ArrayObject`

### Contraction by index specification (`hypermatrix.array_multiply`)

`ArrayMultiply([A_1, ..., A_m], spec)` contracts the arrays according to an index specification such as `\"ij,jk->ik\"`: each array is assigned a list of index labels, and the result is $C_{\mathrm{out}} = \sum_{\mathrm{rest}} \prod_k (A_k)_{\mathrm{labels}_k}$, the sum running over every label not in the output. A label may occur in any number of arrays and in the output, so diagonals and multi-way contractions are expressed directly. Without an output part, the labels occurring exactly once survive, in sorted order. The specification may also be given as index lists, `[[1, 2], [2, 3]] -> [1, 3]`.

Depends on: `hypermatrix.array`

Implemented as: `hypermatrix.algebra.array_multiply`

### Plex algebra (`hypermatrix.hypermatrix_higher_arity.plex_algebra`)

For a closed plex product $\mu$ of order $n$ and arity $k$ and a size $d$, the plex algebra is $(A, \mu)$ with $A = F^{[d]^n}$ the regular $n$-arrays of size $d$ and $\mu: A^k \to A$ the plex product. On basis arrays $\mu(e_{x_1}, \ldots, e_{x_k})$ is a basis array or $0$, so $(A, \mu)$ is the linearization of a partial $k$-ary operation on $[d]^n$.

Depends on: `hypermatrix.plex_product`, `hypermatrix.plex_product_census`

Implemented as: `hypermatrix_higher_arity.plex_algebras.plex_algebra_table`

### Plex diagram (`hypermatrix.plex_diagram`)

A plex diagram is a labelled hypergraph whose edges are plexes (arrays up to the order of their indices), named by their edge labels, and whose vertices are indices; a vertex labelled $\bullet$ is contracted, the others are free. An edge's symmetry type fixes how an array sits on it: a directed edge's vertex order is the array's index order, an unordered edge takes a symmetric array, a cyclic edge a cyclic one.

Depends on: `common.hypergraph`, `hypermatrix.array`

Implemented as: `hypermatrix.plex.plex_diagram`

### Identity search for plex products (`hypermatrix.plex_identity_search`)

Terms in plex products are sorted into classes by the isomorphism type of their diagrams, the isomorphisms fixing every variable and the output order. Terms in one class are equal as operations on arrays; a class with several terms is an identity.

Depends on: `hypermatrix.plex_term_diagram`

Implemented as: `hypermatrix.plex_identities.plex_identity_classes`

### Normal forms of a plex diagram (`hypermatrix.plex_normal_forms`)

The normal forms of a plex diagram under a set of plex rules: the diagrams reached by rewriting with valid plex events (each contracting its match's marked vertices) in every possible order until no rule applies. When a normal form is a single plex, its label is a term whose value is the diagram's; distinct such terms are equal, which is associativity read as confluence.

Depends on: `hypermatrix.plex_rule`

Implemented as: `hypermatrix.plex_identities.plex_normal_forms`

### Plex product (`hypermatrix.plex_product`)

The plex product of a plex diagram on arrays $A_e$ (one per plex name) is the array on the free vertices $C_{\mathrm{free}} = \sum_{\mathrm{marked}} \prod_e (A_e)_{\mathrm{vertices}(e)}$, the indices of each array read in its edge's vertex order; an unordered or cyclic edge requires its array to have that symmetry, which makes the order immaterial. A label that is a term $P(x, y, \ldots)$ of a named diagram $P$ is first evaluated as that plex product.

Depends on: `hypermatrix.plex_diagram`, `hypermatrix.array_multiply`

Implemented as: `hypermatrix.plex.plex_product`

### Enumeration of plex products (`hypermatrix.plex_product_census`)

The closed plex products of order $n$ and arity $k$ (operations $A^k \to A$ on regular $n$-arrays) are the pairs (set partition of the $kn$ argument slots into indices, ordered choice of $n$ of them as the output). They are enumerated up to equality of operation (`strict`), up to a common permutation of index positions (`isomorphism`, which gives isomorphic algebras), additionally up to permuting arguments (`parastrophy`), or up to isomorphism of the plex diagrams as labelled hypergraphs (`hypergraph`).

Depends on: `hypermatrix.plex_diagram`, `hypermatrix.plex_product`

Implemented as: `hypermatrix.plex_enumeration.enumerate_plex_products`

### Plex diagram as a rewrite rule (`hypermatrix.plex_rule`)

A plex diagram $P$ named $p$ gives the rewrite rule whose input is $P$ with each plex name replaced by a label variable (its marked vertices still marked, so they match only contracted indices) and whose output is one directed edge on $P$'s free vertices, in output order, labelled $p(x_1, \ldots, x_k)$ in the variables of its plex names.

Depends on: `hypermatrix.plex_diagram`, `common.hypergraph_rule`

Implemented as: `hypermatrix.plex.plex_rule`

### Diagram of a plex term (`hypermatrix.plex_term_diagram`)

The diagram of a term $P(t_1, \ldots, t_k)$ in plex products is $P$'s diagram with each plex replaced by the diagram of the term that fills it: that term's output vertices are glued to the plex's vertices in order, and its contracted vertices are renamed apart. A variable is a single plex of its own name. The free vertices, in the order of the outermost operation's output, are the output of the term.

Depends on: `hypermatrix.plex_diagram`, `hypermatrix.plex_product`

Implemented as: `hypermatrix.plex_identities.plex_term_diagram`

### Claims in hypermatrix

- **supported** (`hypermatrix.dagger_semiheap`): The ternary product $\eta(a, b, c) = a\, b^{\top} c$ of matrices (the plex diagram $a_{ip} b_{qp} c_{qk}$) is a semiheap, found by confluence on the zigzag chain of five matrices; its three terms equal the chain of matrix products with infix transposes $a\, b^{\top} c\, d^{\top} e$, and the middle one rests on $T$ being an involutive antihomomorphism.
  - evidence (numerical): confluence and identity search, checked numerically
- **supported** (`hypermatrix.fish_semiheap`): The fish product $F(a, b, c)_{ijk} = \sum_{p,q,r} a_{ijp} b_{qrp} c_{qrk}$ is a semiheap: rewriting the long fish of five plexes with the fish rule in every order gives exactly the three normal forms $F(F(a,b,c),d,e)$, $F(a,F(d,c,b),e)$, $F(a,b,F(c,d,e))$. Among the 360 terms with two fish operations in five distinct variables, the identity classes are exactly the instances of this axiom.
  - evidence (literature): heaps-of-fish, Theorem (Fish Associativity)
  - evidence (numerical): confluence and identity search, checked numerically
- **refuted** (`hypermatrix.hypermatrix_higher_arity.algebra_iso_implies_diagram_iso`): Plex products inducing isomorphic algebras have isomorphic plex diagrams.
  - evidence (numerical): x_ab y_ac -> (a,b) and x_ab y_cb -> (a,b) are isomorphic by transposition, but one diagram is an out-star and the other an in-star; 10 of 16 isomorphism classes of (2,2) span several diagram classes
- **refuted** (`hypermatrix.hypermatrix_higher_arity.diagram_iso_implies_algebra_iso`): Plex diagrams isomorphic as labelled hypergraphs (labels up to renaming) induce isomorphic algebras.
  - evidence (numerical): a_ij b_jk -> (i,k) and the same diagram with output (k,i), i.e. ab and (ab)^T: the first is associative, the second not; 6 of 9 hypergraph classes of (n,k) = (2,2) hold non-isomorphic algebras
- **refuted** (`hypermatrix.hypermatrix_higher_arity.linear_is_positional`): Two closed plex products induce linearly isomorphic algebras exactly when their shapes are related by a common permutation of positions.
  - evidence (numerical): x_aa y_ab -> (a,b) (rows of y scaled by the diagonal of x) and x_ab y_ac -> (a,c) (scaled by the row sums) are isomorphic by phi(x)_aa = x_aa - sum_{b != a} x_ab, a linear map that is not a permutation of the basis; checked over Q at d = 2, 3, 4
- **supported** (`hypermatrix.hypermatrix_higher_arity.linear_is_positional_without_diagonals`): For connected closed plex products without diagonals, two induce linearly isomorphic algebras exactly when their shapes are related by a common permutation of positions.
  - evidence (numerical): exhaustive over GL(4, 2): GF(2) linear classes = positional classes for (n,k) = (2,2) (16) and (2,3) (296) at d = 2; open over Q and for larger d
- **supported** (`hypermatrix.hypermatrix_higher_arity.monomial_is_positional`): Two closed plex products induce algebras isomorphic through a permutation of the basis $[d]^n$ exactly when their shapes are related by a common permutation of positions.
  - evidence (numerical): exact (canonical forms of the operation hypergraphs) for (n,k) = (2,2) with and without diagonals, (2,3), (3,2), at d = 2 and d = 3: monomial classes = positional classes in every case
- **supported** (`hypermatrix.hypermatrix_higher_arity.plex_shapes_are_operations`): For $d \ge 2$ two closed plex products define the same operation $A^k \to A$ on $n$-arrays of size $d$ exactly when their shapes (slot partition and output sequence) are equal; at $d = 1$ all of them coincide. The number of distinct $k$-ary plex operations of order $n$ is the number of shapes, the same for every $d \ge 2$ and every commutative semiring with $0 \ne 1$.
  - evidence (argument): on basis arrays the product of a tuple is e_y or 0, defined iff the slot values are constant on the blocks; for d >= 2, colouring the blocks of one partition with two values shows each block of the other lies inside one of its blocks, and conversely, so the partitions agree; then two output blocks coloured differently fix the output order
  - evidence (numerical): all 62 + 3120 + 1712 shapes of (n,k) = (2,2), (3,2), (2,3) give distinct partial operations at d = 2
- **supported** (`hypermatrix.hypermatrix_higher_arity.positional_isomorphism`): Transposing every array by one permutation $\tau$ of the $n$ index positions is an isomorphism from the plex algebra of a shape to that of the shape with every plex and the output reordered by $\tau$.
  - evidence (argument): rename the index variables of the sum; the summation set is unchanged
  - evidence (numerical): every shape and permutation for (n,k) = (2,2), (3,2), (2,3), on random arrays
- **supported** (`hypermatrix.plex_identity_criterion`): Two terms in plex products whose diagrams are isomorphic by a map fixing every variable and the output order are equal as operations, over every commutative semiring and in every dimension. Conversely, for terms in which each variable occurs once, over $\mathbb{Z}$ (or any semiring where positive integers are nonzero) and in dimension $d \ge$ the number of vertices, non-isomorphic diagrams give different operations: the identity search decides equality of such terms.
  - evidence (argument): expansion: the value of a term is the plex product of its diagram, by plex_rewriting_evaluates read backwards (substitution of one plex product into another merges the sums over contracted indices); an isomorphism fixing names and output only renames summation indices. Converse: the coefficient of the monomial given by an injective assignment of indices to the vertices of one diagram is a positive count of assignments of the other's vertices with the same index tuples on every named plex; each such assignment is a surjective name- and output-preserving homomorphism, and homomorphisms both ways between finite diagrams are isomorphisms
  - evidence (numerical): every class found in the review examples agrees on random integer arrays of dimension 3, and terms in different classes disagree
- **supported** (`hypermatrix.plex_rewriting_evaluates`): Rewriting a plex diagram $D$ with the rule of a plex diagram $P$ named $p$ (at an event that contracts $P$'s marked vertices) and evaluating, with $p(\ldots)$ read as the plex product of $P$, gives the same array as evaluating $D$. Rewriting is symbolic plex algebra; two events whose results agree in value but not in label are an associativity-type identity.
  - evidence (numerical): every valid event on random plex diagrams with random integer arrays (directed and symmetric plexes)
  - evidence (argument): the sum over all marked indices of a product splits as a sum over the indices internal to the match of the matched factors, times the rest, because no other factor carries those indices (commutative semiring: associativity, commutativity, distributivity)
- **supported** (`hypermatrix.transpose_involutive_antihomomorphism`): With $M$ the matrix product and $T$ the transposition (both plex diagrams), the identity search over terms in two matrices with at most three operations finds $T(T(a)) = a$ and $T(M(a, b)) = M(T(b), T(a))$, and every identity class it finds is a consequence of these two; over three matrices it finds the associativity $M(M(a, b), c) = M(a, M(b, c))$.
  - evidence (numerical): identity search with numerical check

## References

- [Heaps of Fish: arrays, generalized associativity and heapoids](https://arxiv.org/abs/2205.05456v1): Reference paper: array algebra, the plex formalism, associativity as confluence, the fish product, heapoids
- [Hypergraphs paclet (WolframInstitute`Hypergraphs`)](https://github.com/Zaphyz/hypergraph-paclet/tree/603c5f3053bed232e7fb14009d042a247124e2b9): Reference implementation: hypermatrices and their contraction calculus, hypergraphs, rewriting, causal graphs, and their rendering
