# From a set family to a support graph—or a checked rejection

Example for **An intrinsic interval-deletion characterization of digraph support families**, manuscript entry 29, SHA-256 `74a88c8c0b5389c8eb0f7ff73655f82ba75f6f79246594ae36629706e225fce0`.

A directed graph supports a vertex subset when every selected vertex has at least one predecessor inside that subset. Loops are allowed; an empty predecessor row makes its vertex unusable. The paper characterizes exactly which listed families arise this way on the **same ground set**. This package provides a usable recognizer, explicit certificates, graph reconstruction, Horn closure operations and visible-vertex projection.

## Run

Python 3.11 or newer. The algorithms use the standard library; NumPy and Matplotlib generate figures.

```sh
python -m venv .venv
# Windows: .venv\Scripts\activate
# macOS/Linux: source .venv/bin/activate
python -m pip install -r requirements.txt
python -m unittest -v test_example.py
python example.py --output outputs
```

The default run takes seconds. Outputs include four search certificates, reconstructed rows, a trace CSV, worked-example results, two figure pairs, a console summary and provenance hashes. The default examples are exact combinatorial objects, so numerical physical parameters are not applicable.

## Inputs and reusable objects

Edit `VERTICES`, `FAMILY`, `RESIDUAL_POLICY` and the budgets at the top of `example.py`. `SetFamily.from_subsets` accepts ordinary labelled subsets. Internally, a subset is a bit mask: for labels (a,b,c), a=1, b=2, c=4 and abc=7. Each certificate records its ordered labels and target-family masks; `family.names(mask)` decodes any input's own ordering.

```python
from example import SetFamily, IntervalRecognizer, check_trace
family = SetFamily.from_subsets(('a','b','c'),
    ((), ('a',), ('a','b'), ('a','b','c')))
result = IntervalRecognizer(family, policy='largest_reverse').solve()
if result['status'] == 'success':
    graph = check_trace(family, result['trace'])
    print(graph.predecessors)  # (1, 1, 2): loop at a, a->b, b->c
elif result['status'] == 'rejected':
    print('All eligible root branches were exhausted and checked.')
else:
    print('Unresolved within the node budget.')
```

`IntervalRecognizer` starts with U equal to the full power set. It selects an inclusion-maximal residual S in U minus the target family. An eligible unused root r lies in S but in no target-family member contained in S. The step removes precisely the interval of subsets X with r in X and X contained in S. This commits the predecessor row P(r)=E minus S. Unused vertices receive loops.

Both supplied policies choose a largest-cardinality maximal residual, differing only in their bit-mask tie-break. The paper permits any fixed maximal-residual policy; root choices still need branching. The recognizer memoizes exact (U, used-roots) states. A node budget returns `unresolved`, never a false rejection. The truth-table budget limits the full power-set representation separately. The default is 4,096 subsets and 100,000 search states.

`check_trace` checks maximality, eligibility, fresh roots and exact termination, then reconstructs and independently verifies the graph. Successful roots are exactly the excluded singletons, each used once; loops are therefore determined by the family. A realization need not be unique, and this reconstruction is not claimed to optimize the number of arcs in general.

`check_rejection` independently traverses the saved search DAG. At every node it recomputes the chosen maximal residual, all eligible roots and each child's complete state. It rejects missing children, truncated branching, successful leaves or inconsistent states. Its validity as a non-realizability certificate invokes the paper's completeness theorem. It is not a Lean kernel check.

## Why branching matters

For the chain family `{empty, a, ab, abc}`, select residual bc first. Choosing root b followed by root c at ac succeeds. Choosing root c first leaves ac needing the already-used root c, so that branch fails although the family is realizable. The first figure shows three target families; the second compares these successful and unsuccessful root paths.

The conjunction family `{empty, a, b, ab, abc}` is union-closed but not graph-realizable. Its maximal nonmembers ac and bc both need c as their root. A predecessor row offers alternatives; it cannot require both a and b. `hall_matching` exposes this root shortage, returning a deficient collection when matching fails. This matching test is necessary, not sufficient: the paper's six-vertex example passes the initial matching but the recognizer rejects after **322 memoized states**. These are states of this implementation, not a count of theorem-proof steps or a polynomial-time bound.

## Verification without listing the whole power set

`SupportGraph.verify_explicit_family` implements the paper's polynomial certificate check for an explicitly listed family. It first verifies all listed members. The complementary Horn theory has one rule P(r) -> r per head. `HornTheory.next_closure` uses Ganter's lectic NextClosure procedure to enumerate its models and test their complements against the list, stopping at the first missing member. At most m+1 models need checking for a family with m listed members.

This **verifies a supplied graph** in polynomial time in ground size plus list size. It does not make graph discovery polynomial. The interval recognizer explicitly materializes 2^n subsets and has factorial worst-case branching in the number b of excluded singletons. Its reported un-memoized call bound is sum over j=0..b of b!/(b-j)!. Representation costs and interior scans are additional.

`HornTheory.normalize_completion` makes the proof mechanism concrete when a hypothetical single-head completion is supplied. It verifies accepted rules G are contained in completion L and that the residual model B is minimal. A violated rule A->r has closure_G(A)=B; replacing it by B->r keeps all completion models. In the example G={a->b}, L={a->b,a->c}, the body a genuinely changes to ab. Omitting the accepted rule a->b would make that replacement unsound. This finite demonstrator is not an algorithm for discovering an unknown completion.

## Projection is different from deletion

`SupportGraph.eliminate(label)` and `project(visible)` implement exact existential projection of hidden vertices. If a removed vertex v supports r and has a loop, r gets a loop. If v supports r without a loop, replace that dependence with v's predecessors; otherwise retain r's row. Relabelling preserves the retained vertex order.

For a two-cycle a<->h, the full supported sets are empty and {a,h}. Projecting onto a gives empty and {a}, realized by a loop. `delete(('a',))` instead removes h and its support, leaving only empty. These are set-family operations, not physical kinetic interventions. The code checks the projected interior formula as well as the entire family.

`independent_product` builds disjoint unions and rejects overlapping labels. Intersection on a shared ground is different: intersecting the support families with rows P(c)={a} and P(c)={b}, with loops at a,b, gives the non-realizable conjunction family. The paper proves closure under projection, so hidden vertices cannot rescue that conjunction as a projected support family. Finite projection tests illustrate the theorem; they do not prove it for all sizes.

## Elementary and general catalytic systems

`StructuralCRS.elementary(graph)` constructs reactions r_i: food -> product_i, with product_j catalysing r_i exactly when j is a predecessor of i. A loop becomes self-catalysis by the reaction's own product. Its RAFs plus the empty set reproduce the support family. Catalysts are checked in final food closure; no kinetic startup claim is made.

The separate three-reaction example uses a: f->x, b: f->y, c: x+y->z, all catalysed by food f. Its food-generation requirement supplies a genuine conjunction and realizes `{empty,a,b,ab,abc}`. Thus failure of the graph recognizer excludes an elementary same-ground realization, not every general RAF realization. The paper's broader antimatroid/support-family factorization is existential; this package does not search for all possible antimatroid factors or claim uniqueness of such factors.

## Scientific checks and scope

Seven test groups compare both policies on all 256 families on three vertices against all 512 labelled graphs; verify exact roots, interiors, four chain realizations and two cycle realizations; tamper with certificates and enforce budget distinctions; reproduce the Hall counterexample; check NextClosure and explicit-list verification, including a 40-coordinate one-member list without a power-set scan; check every three-vertex graph under single-vertex projection and all 256 disjoint products of two two-vertex graphs; test normalization and empty/full boundary cases; and verify elementary/general CRS semantics.

The three-vertex census gives 55 realizable families among 61 union-closed families containing empty. The package does not rerun the manuscript's four-vertex census or Lean development. It checks exact finite constructions and receipts; the paper supplies the universal characterization, normalization and projection proofs. No kinetics, thermodynamics or quantitative biological model is inferred from support graphs.

Manuscript map: criterion and traces, Sections 2–3; Horn normalization, Section 4; exact roots, Section 6; recognition and explicit-list certificate, Section 7; Hall obstructions, Section 8; projection/deletion/products, Section 9; RAF interpretation, Section 10.

Licensing: MIT is proposed for these original example files, pending the owner's decision. No license grant is made here; manuscript licensing remains separate.