Back to Combinatorics

Capstone C: Algebraic Combinatorics Explorer

October 13, 2026 Wasil Zafar 19 min read

Implement tableaux, RSK, hook-length counts, and symbolic identity experiments

Table of Contents

  1. Tableau conventions and data representation
  2. Hook-length counting with exhaustive verification
  3. RSK insertion and reverse insertion
  4. Experiments with symmetric-function products
  5. From experimental identity to mathematical explanation
  6. Algebraic explorer report and assessment

Tableau conventions and data representation

The explorer connects exact enumeration, an invertible insertion algorithm, and a polynomial identity. Fix English diagrams: rows are left aligned, the longest row is at the top, and row and column indices increase downward and to the right. A shape is a partition $\lambda=(\lambda_1,\ldots,\lambda_\ell)$ with positive weakly decreasing parts; its size is $n=\sum_i\lambda_i$. The empty shape is allowed and has one empty tableau.

A standard Young tableau, abbreviated SYT, fills the diagram with $1,\ldots,n$ exactly once, increasing strictly along rows and down columns. A semistandard Young tableau, abbreviated SSYT, uses a specified positive alphabet, is weakly increasing along rows, and strictly increasing down columns. Repeated entries are permitted in different columns but not in the same column. Here semistandard always means this row-weak, column-strict convention; transposed conventions require different insertion inequalities.

Represent a tableau by a tuple of row tuples when storing an immutable object and by lists of row lists during insertion. Empty rows are removed. A shape is not a list of column lengths, and row order is not interchangeable. The Python code uses zero-based indices, while mathematical cell coordinates $(i,j)$ below are one-based. Review symmetric functions and Young tableaux, representation-theoretic combinatorics, and bijective, algebraic and computer-assisted enumeration for the broader background.

Project Brief

Algebraic Combinatorics Explorer

Conventions: insert into the first row, bump the first entry strictly greater than the incoming value, and carry the bumped entry to the next row. If no larger entry occurs, append. Reverse insertion replaces the rightmost entry strictly smaller than the carried value. The strict inequalities are paired; changing one changes the correspondence.

Distinguishing examples: shape $(2,1)$ with rows $(1,2)$ and $(3)$ is standard. Rows $(1,1)$ and $(2)$ are semistandard but not standard. Rows $(1,2)$ and $(1)$ violate column strictness. A one-row tableau with repeated entries can be semistandard, while a one-column tableau cannot contain repeats.

Project parameters: enumerate standard tableaux for every shape of size at most six, compare with corner deletion and hook lengths, test permutation RSK through size seven, and test words on alphabet $\{1,2,3\}$ through length five. Explore the identity $s_{(2,1)}s_{(1)}=s_{(3,1)}+s_{(2,2)}+s_{(2,1,1)}$ in two, three, and four variables, then prove it for every finite alphabet.

Worked hook instance: shape $(3,2)$ has hooks $4,3,1$ in its first row and $2,1$ in its second. Their product is 24, predicting $5!/24=5$ standard tableaux. The insertion word $(3,1,4,2,5)$ will produce this shape and a complete reversible trace.

Hook-length counting with exhaustive verification

The hook of a cell contains that cell, all cells to its right in the same row, and all cells below it in the same column. If $\lambda'_j$ is the height of column $j$, its length is $h(i,j)=\lambda_i-j+\lambda'_j-i+1$. The classical hook-length theorem says

$$f^\lambda=\frac{n!}{\prod_{(i,j)\in\lambda}h(i,j)}.$$

This is an established theorem for standard tableaux of straight partition shapes, not the corresponding single-product formula for arbitrary skew shapes. Its original source is Frame, Robinson, and Thrall's The Hook Graphs of the Symmetric Group, published in 1954. The general hook-length proof is an imported result here; this project independently verifies its small predictions rather than proving the theorem from tests.

For a combinatorial check independent of hook products, the largest label must occupy a removable corner: a cell whose removal leaves a partition diagram. Deleting it gives a smaller standard tableau; conversely append the largest label at that corner. These inverse operations prove

$$f^\lambda=\sum_{\mu\text{ obtained by deleting one corner of }\lambda}f^\mu,\qquad f^\varnothing=1.$$

The direct enumerator tries every bijective filling of each diagram and filters by the defining inequalities. It does not generate its objects using the corner recurrence or the hook formula. Counts, duplicate tests, and two independently derived predictions must agree.

Save the panel as algebraic_lab.py and run python3 algebraic_lab.py in an empty output directory. It uses only the standard library, writes algebraic-data.json, prints the interpreter version and deterministic data checksum, and stops at a failed assertion. The reference run used Python 3.12.14. The conversion routines are specified for valid tableaux and corresponding pairs; their internal assertions do not constitute a complete parser for untrusted input.

from collections import Counter
from functools import cache
from itertools import combinations_with_replacement, permutations, product
from math import factorial, prod
from pathlib import Path
import hashlib
import json
import sys


def shapes(n, largest=None):
    if n == 0:
        yield ()
        return
    for first in range(min(n, n if largest is None else largest), 0, -1):
        for rest in shapes(n - first, first):
            yield (first,) + rest


def valid(t, standard=False):
    lengths = list(map(len, t))
    if any(k <= 0 for k in lengths) or lengths != sorted(lengths, reverse=True):
        return False
    flat = [v for row in t for v in row]
    if any(v <= 0 for v in flat):
        return False
    if standard and sorted(flat) != list(range(1, len(flat) + 1)):
        return False
    for r, row in enumerate(t):
        if any(row[c] > row[c + 1] for c in range(len(row) - 1)):
            return False
        if r and any(t[r - 1][c] >= x for c, x in enumerate(row)):
            return False
    return True


def fill(shape, values):
    t, offset = [], 0
    for width in shape:
        t.append(tuple(values[offset:offset + width]))
        offset += width
    return tuple(t)


def standard_tableaux(shape):
    for p in permutations(range(1, sum(shape) + 1)):
        t = fill(shape, p)
        if valid(t, standard=True):
            yield t


@cache
def corner_count(shape):
    if not shape:
        return 1
    total = 0
    for r, width in enumerate(shape):
        if r == len(shape) - 1 or width > shape[r + 1]:
            reduced = list(shape)
            reduced[r] -= 1
            total += corner_count(tuple(x for x in reduced if x))
    return total


def hook_count(shape):
    hooks = [width - c + sum(other > c for other in shape[r + 1:])
             for r, width in enumerate(shape) for c in range(width)]
    numerator, denominator = factorial(sum(shape)), prod(hooks)
    assert numerator % denominator == 0
    return numerator // denominator


def insert(t, x):
    r = 0
    while r < len(t):
        for c, y in enumerate(t[r]):
            if y > x:
                t[r][c], x = x, y
                break
        else:
            t[r].append(x)
            return r, len(t[r]) - 1
        r += 1
    t.append([x])
    return r, 0


def reverse_insert(t, r):
    x = t[r].pop()
    if not t[r]:
        t.pop(r)
    for u in range(r - 1, -1, -1):
        c = max(c for c, y in enumerate(t[u]) if y < x)
        t[u][c], x = x, t[u][c]
    return x


def rsk(word):
    p, q, trace = [], [], []
    for k, x in enumerate(word, 1):
        r, c = insert(p, x)
        if r == len(q):
            q.append([])
        assert c == len(q[r])
        q[r].append(k)
        assert valid(p) and valid(q, standard=True)
        assert list(map(len, p)) == list(map(len, q))
        trace.append({'step': k, 'input': x,
                      'P': [row[:] for row in p], 'Q': [row[:] for row in q]})
    return p, q, trace


def inverse_rsk(p, q):
    p, q = [row[:] for row in p], [row[:] for row in q]
    output = []
    for k in range(sum(map(len, q)), 0, -1):
        r = next(r for r, row in enumerate(q) if row[-1] == k)
        q[r].pop()
        if not q[r]:
            q.pop(r)
        output.append(reverse_insert(p, r))
        assert valid(p) and valid(q, standard=True)
    assert not p and not q
    return tuple(reversed(output))


def semistandard_tableaux(shape, m):
    for values in product(range(1, m + 1), repeat=sum(shape)):
        t = fill(shape, values)
        if valid(t):
            yield t


def schur(shape, m):
    polynomial = Counter()
    for t in semistandard_tableaux(shape, m):
        values = tuple(x for row in t for x in row)
        polynomial[tuple(values.count(i) for i in range(1, m + 1))] += 1
    return polynomial


def multiply(a, b):
    out = Counter()
    for x, c in a.items():
        for y, d in b.items():
            out[tuple(u + v for u, v in zip(x, y))] += c * d
    return out


def complete(k, m):
    out = Counter()
    if k >= 0:
        for values in combinations_with_replacement(range(m), k):
            out[tuple(values.count(i) for i in range(m))] += 1
    return out


def jacobi_trudi(shape, m):
    out = Counter()
    for p in permutations(range(len(shape))):
        sign = (-1) ** sum(p[i] > p[j] for i, j in combinations_indices(len(p)))
        term = Counter({(0,) * m: 1})
        for i, j in enumerate(p):
            term = multiply(term, complete(shape[i] - i + j, m))
        for exponent, coefficient in term.items():
            out[exponent] += sign * coefficient
    return Counter({e: c for e, c in out.items() if c})


def combinations_indices(n):
    return ((i, j) for i in range(n) for j in range(i + 1, n))


def main():
    assert valid(((1, 1), (2,))) and not valid(((1, 1), (2,)), True)
    assert not valid(((1, 2), (1,)))
    hook_rows = []
    for n in range(7):
        square_sum = 0
        for shape in shapes(n):
            tableaux = list(standard_tableaux(shape))
            f = len(tableaux)
            assert len(set(tableaux)) == f == corner_count(shape) == hook_count(shape)
            square_sum += f * f
            hook_rows.append({'shape': shape, 'count': f})
            if n <= 5:
                for p in tableaux:
                    for q in tableaux:
                        w = inverse_rsk([list(r) for r in p], [list(r) for r in q])
                        a, b, _ = rsk(w)
                        assert tuple(map(tuple, a)) == p and tuple(map(tuple, b)) == q
        assert square_sum == factorial(n)
    round_trips = 0
    for n in range(8):
        for word in permutations(range(1, n + 1)):
            p, q, _ = rsk(word)
            assert valid(p, True) and inverse_rsk(p, q) == word
            round_trips += 1
    for n in range(6):
        for word in product(range(1, 4), repeat=n):
            p, q, _ = rsk(word)
            assert inverse_rsk(p, q) == word
    identities = []
    for m in (2, 3, 4):
        terms = {shape: schur(shape, m) for shape in ((2, 1), (1,), (3, 1), (2, 2), (2, 1, 1))}
        for shape, poly in terms.items():
            assert poly == jacobi_trudi(shape, m)
        lhs = multiply(terms[2, 1], terms[1,])
        rhs = terms[3, 1] + terms[2, 2] + terms[2, 1, 1]
        assert lhs == rhs
        images = set()
        for t in semistandard_tableaux((2, 1), m):
            for x in range(1, m + 1):
                u = [list(row) for row in t]
                r, _ = insert(u, x)
                assert valid(u)
                image = tuple(map(tuple, u))
                assert image not in images
                images.add(image)
                y = reverse_insert(u, r)
                assert y == x and tuple(map(tuple, u)) == t
        targets = {t for shape in ((3, 1), (2, 2), (2, 1, 1))
                   for t in semistandard_tableaux(shape, m)}
        assert images == targets
        identities.append({'variables': m, 'coefficients': sorted(lhs.items())})
    _, _, trace = rsk((3, 1, 4, 2, 5))
    payload = {'max_hook_size': 6, 'max_permutation_size': 7,
               'hook_counts': hook_rows, 'permutation_round_trips': round_trips,
               'trace': trace, 'schur_products': identities}
    data = json.dumps(payload, sort_keys=True, separators=(',', ':')) + '\n'
    Path('algebraic-data.json').write_text(data, encoding='utf-8')
    print('Python:', sys.version.split()[0])
    print('shapes:', len(hook_rows), 'permutation round trips:', round_trips)
    print('hook counts, both inverse directions, words, and Schur identities passed')
    print('SHA256:', hashlib.sha256(data.encode()).hexdigest())


if __name__ == '__main__':
    main()

There are 30 shapes across sizes zero through six. For size four, the counts in partition order $(4),(3,1),(2,2),(2,1,1),(1,1,1,1)$ are $1,3,2,3,1$. For size five, the counts for $(5),(4,1),(3,2),(3,1,1),(2,2,1),(2,1,1,1),(1,1,1,1,1)$ are $1,4,5,6,5,4,1$. Shape $(3,2,1)$ at size six has hook product 45 and count $720/45=16$. The JSON retains every shape and exact count, including the empty case.

Each shape of size $n$ requires $n!$ candidate fillings in this transparent enumerator, with $O(n)$ inequality checks per filling. The independent recurrence is memoized by shape. The code also checks $\sum_{\lambda\vdash n}(f^\lambda)^2=n!$ through size six; the RSK bijection explains that identity later. This aggregate check supplements the per-shape checks and cannot replace them.

Exercise: compute $f^{(2,2)}$ by hooks and by corners. Solution: hooks are $3,2,2,1$, giving $24/12=2$. There is one removable corner, leaving $(2,1)$, whose two standard tableaux give the same answer.

RSK insertion and reverse insertion

This implementation uses the row-insertion RSK correspondence for permutations and its word variant. For a permutation $w_1\cdots w_n$, start with empty insertion and recording tableaux $P,Q$. Insert $w_k$ into $P$ and put the time label $k$ in the newly created cell of $Q$. For repeated-letter words, $P$ is semistandard and $Q$ is standard; for permutations both are standard. General matrix or two-line-array RSK, including its ordering and tie conventions, is outside this implementation's scope. The primary historical reference is Knuth's Permutations, matrices, and generalized Young tableaux.

Insertion invariants before testing: replacing the first entry $y>x$ by $x$ preserves row weakness, since entries before it are at most $x$ and entries after it are at least $y$. Carry $y$ downward. If its previous column was $c$, the next replacement or append position is at most $c$: an existing cell immediately below the previous $y$ was greater than $y$, or the next row ends before that column. Thus the bumping path moves weakly left as it descends.

The entry above a replacement is strictly smaller than its new value. At the same column it is the smaller entry just inserted in the preceding row; farther left it is at most that preceding inserted value. The entry below remains greater: it was greater than the old replaced value, or is replaced later by that old value. These inequalities preserve column strictness. At termination, the weakly left path ensures that an append leaves a partition shape and creates one outer corner. Only existing values are moved, and one new value is added.

Since shapes grow by outer corners, every entry above or to the left of the new recording label $k$ was placed earlier. Thus $Q$ is standard and shares $P$'s shape. Distinct permutation values make $P$ standard as well. These are the mathematical reasons for the code's validity assertions; passing assertions is not their proof.

Worked trace, writing rows separated by a slash:

  • Insert 3: $P=(3)$; $Q=(1)$.
  • Insert 1: 1 bumps 3; $P=(1)/(3)$; $Q=(1)/(2)$.
  • Insert 4: append in row one; $P=(1,4)/(3)$; $Q=(1,3)/(2)$.
  • Insert 2: 2 bumps 4, which appends in row two; $P=(1,2)/(3,4)$; $Q=(1,3)/(2,4)$.
  • Insert 5: append in row one; $P=(1,2,5)/(3,4)$; $Q=(1,3,5)/(2,4)$.

To invert, locate the largest label in $Q$, which occupies a removable corner. Remove it and the corresponding end cell of $P$, carrying that $P$ entry upward. In each preceding row, replace the rightmost entry smaller than the carried value, carrying the displaced entry further upward. The final displaced value is the recovered letter. Collect letters in reverse time order.

Why the inverse exists: immediately above a lower-row end cell is a smaller entry, so the first upward choice exists. Later reverse steps move weakly right as they ascend. Row weakness is preserved by choosing the rightmost smaller entry; column strictness is preserved by the same paired inequalities in reverse. In a forward bump, every entry after the replacement is at least the value that was bumped, while the inserted entry is smaller. Therefore the reverse rule selects exactly that replacement. Step-by-step cancellation proves both compositions are identities, by induction on the number of insertions. The same reverse inequalities apply to any semistandard $P$ and standard $Q$ of the same shape, giving a word that reinserts to the pair.

For the displayed trace, reverse outputs are $5,2,4,1,3$, recovering $(3,1,4,2,5)$ after reversal. At the second reverse step, remove 4 from row two, replace the rightmost smaller entry 2 in row one by 4, and output 2. This concretely checks the strict reverse inequality.

The program tests 5,914 permutations across sizes zero through seven, and all 364 words of lengths zero through five over a three-letter alphabet. It also starts from every same-shape pair of standard tableaux through size five and checks the opposite round trip. Testing only word-to-pair-to-word could miss a failure of surjectivity; pair-to-word-to-pair addresses that independently. In general, the inverse proof gives the bijection and hence $n!=\sum_{\lambda\vdash n}(f^\lambda)^2$.

Exercise: insert word $(1,1)$. Solution: $P$ is the row $(1,1)$ and $Q$ the row $(1,2)$. Bumping the first entry greater than or equal to the incoming value would instead change the shape, violating our convention.

Experiments with symmetric-function products

Work in the polynomial ring $\mathbb Z[x_1,\ldots,x_m]$. Define $s_\lambda(x_1,\ldots,x_m)$ as the sum of weights of semistandard tableaux of shape $\lambda$ on alphabet $[m]$. If entry $i$ occurs $a_i$ times, the weight is $x_1^{a_1}\cdots x_m^{a_m}$. There are no factorial denominators or coefficient normalizations. The empty shape contributes one; a shape with a column taller than $m$ contributes zero. These finite-variable specializations are the Schur polynomials under our convention.

Store a polynomial as an exact dictionary from exponent tuples to integer coefficients. The product routine adds exponents and multiplies coefficients, so no floating-point simplification enters. Direct semistandard enumeration computes every coefficient of the chosen identity for $m=2,3,4$:

$$s_{(2,1)}s_{(1)}=s_{(3,1)}+s_{(2,2)}+s_{(2,1,1)}.$$

For a distinct computational route, use the established Jacobi–Trudi identity

$$s_\lambda=\det\bigl(h_{\lambda_i-i+j}\bigr)_{1\le i,j\le\ell},$$

where $h_r$ sums all weakly increasing words of length $r$ on the alphabet, $h_0=1$, and $h_r=0$ for $r<0$. The code constructs these complete homogeneous polynomials independently by combinations with replacement and expands the determinant over permutations, including their signs. Negative intermediate coefficients are retained until cancellation. Jacobi–Trudi is an imported algebraic theorem, not proved by these finite comparisons; its fuller treatment is in the prerequisite symmetric-functions chapter.

Selected three-variable coefficient checks: for $x_1^3x_2$, the product coefficient is 1 and the three right-hand contributions are $1,0,0$. For $x_1^2x_2^2$, they are $2$ and $1,1,0$. For $x_1^2x_2x_3$, they are $4$ and $2,1,1$. For $x_1^4$, all are zero. Thus coefficient one in the Schur-basis expansion does not mean every monomial coefficient is one.

For the last nonzero example, direct enumeration gives

$$s_{(2,1)}=\sum_{i\ne j}x_i^2x_j+2x_1x_2x_3\qquad(m=3).$$

Multiplying by $x_1+x_2+x_3$ supplies two contributions of size one and one of size two to $x_1^2x_2x_3$, totaling four. This hand calculation independently checks a selected product coefficient in addition to the full determinant comparison.

Exercise: why does $s_{(2,1,1)}$ vanish with two variables? Solution: its first column has three cells, requiring three strictly increasing alphabet entries. Specialization can make a whole Schur term disappear; this does not refute the identity in a larger alphabet.

From experimental identity to mathematical explanation

The experiment suggests the one-box Pieri identity for shape $(2,1)$. We now prove the displayed identity for every alphabet size $m\ge1$, using the established insertion invariants rather than extending a finite coefficient table by guesswork.

An object counted on the left is a pair $(T,a)$: a semistandard tableau of shape $(2,1)$ and one letter $a\in[m]$. Its weight is the product of the tableau's weight and the variable $x_a$. Insert $a$ into $T$. Exactly one outer corner is added, and the possible resulting shapes are precisely $(3,1),(2,2),(2,1,1)$. The output remains semistandard and preserves the total multiset of letters, so it has exactly the same monomial weight as the pair.

Conversely, in a tableau of any of those three shapes, the unique cell outside $(2,1)$ is an outer corner. Remove it and reverse-insert its value. The inverse rules return one semistandard tableau of shape $(2,1)$ and one letter of the same alphabet. The reversal and insertion cancel, so this is a weight-preserving bijection between the left-hand pairs and the disjoint union of the three right-hand families. Summing weights proves the polynomial identity, including all coefficients and all finite alphabet sizes. The argument also explains the one-box rule for an arbitrary straight partition shape.

Worked bijective instance: start with $T$ having rows $(1,2)/(3)$ and insert letter 1. The first row becomes $(1,1)$ and carries 2 downward; the second row becomes $(2)$ and carries 3 to a new third row. The result $(1,1)/(2)/(3)$ has shape $(2,1,1)$ and weight $x_1^2x_2x_3$. Removing the new third-row cell and reversing the two bumps recovers exactly $T$ and letter 1.

The program explicitly checks this bijection's injectivity, reverse recovery, and full target coverage for the three tested alphabets. There are respectively 4, 24, and 80 source pairs at $m=2,3,4$. The general proof, rather than these finite totals, establishes the identity without an alphabet cutoff.

The notebook should mark the original finite polynomial equality as “observed,” the insertion explanation as a proposed proof until its invariants are checked, and the completed weight-preserving correspondence as “proved.” Hook-length counting, RSK, Jacobi–Trudi, and the one-box Pieri rule are classical results; this project claims a reproducible implementation and exposition, not novelty. A different experimentally discovered product identity needs its own proof or an explicit unproved label. Neither numerical specialization at $x_i=1$ nor agreement in two variables establishes a general symmetric-function identity.

Exercise: why is weight preservation necessary even when the two sets have equal cardinalities? Solution: equal totals prove equality only after setting every variable to one. Matching the multiset of letters proves equality coefficient by coefficient, which is the stronger polynomial statement required here.

Algebraic explorer report and assessment

A complete submission contains algebraic_lab.py, the generated algebraic-data.json, the execution command and interpreter version, the row and alphabet conventions, the worked insertion/reversal trace, the exact hook-count checks, the selected coefficient calculations, and the invariant and bijection proofs. The JSON contains all 30 shape counts, the five-stage trace, the permutation round-trip total, and the full product coefficient dictionaries for the tested alphabets. The code checks additional word and inverse-pair cases during execution even though their individual objects are not stored in the dataset.

The reference data SHA-256 is 2e9596eaa12e5abf7c9cb07c469596979b034bc14ae81c99cec3160739e72399, using sorted JSON keys, compact separators, UTF-8 encoding, and a final newline. A matching checksum establishes identical output bytes, not the validity of the mathematical conventions. Retain source and environment information alongside it, and run from a directory where the expected output filename can be created.

State the limits: exhaustive hook enumeration ends at size six, permutation tests end at seven, word tests end at length five, and the polynomial comparisons use at most four variables. The tested RSK variant records time labels and does not implement general matrix input. The general hook and determinant formulas are imported theorems; the report proves the corner recurrence, insertion invariants, inverse mechanism, and the chosen weight-preserving identity. Exact computations remove rounding error but do not remove the possibility of a shared modeling mistake, which is why independent formulations and hand checks remain necessary.

An application is counting precedence-constrained schedules: cells are tasks, and a task must follow its left and upper neighbors. Standard tableaux encode all legal orderings, while the hook formula supplies their exact number for a straight diagram. Semistandard weights record task categories with repetition, and insertion turns a sequence into a structured pair. Any practical interpretation must preserve the specified precedence and repetition rules before applying these counts.

Criterion and weightRequired evidence and completion standard
Conventions and examples — 10 pointsState English diagrams, straight partition shapes, alphabet, row weakness, column strictness, standard labels, index conventions, and empty cases; include valid and invalid examples.
Hook-length verification — 20 pointsSupply all 30 shape records and agreement among exhaustive fillings, corner deletion, and hook products; show the $(3,2)$ and $(2,2)$ calculations and identify the imported general theorem.
RSK and inverse — 25 pointsGive runnable insertion and reversal, the full five-step trace, invariant and cancellation arguments, all 5,914 permutation tests, repeated-letter tests, and inverse tests starting from tableau pairs.
Symbolic experiments — 15 pointsDocument exact polynomial conventions, complete homogeneous functions and determinant signs; make direct enumeration and Jacobi–Trudi agree and independently calculate the selected monomial coefficients.
Mathematical explanation — 20 pointsProve the one-box product by a bijection with a specified inverse and preserved weights; distinguish finite checks, imported theorems, proved claims, and unproved exploratory patterns.
Reproducible report — 10 pointsDeliver code, exact JSON data, conventions, environment and invocation, trace and verification evidence, proofs, checksum, application assumptions, and explicit range and algorithm limitations.