# Definition 1 formalizes an evolutionary selection model as a DAG G^(T) over trait variables X^(0)...X^(T), heritable factors epsilon^(0)...epsilon^(T), and reproduction/selection indicators S^(0)...S^(T-1), distinguishing it from one-shot static selection models (Section 2, Definition 1).

**Verdict: VERIFIED.**

The implementation instantiates the four printed edge families directly. For a static trait graph with `d` traits, trait-edge count `m`, and `q=|pa(S)|`, it independently checks

- `|V| = 2d(T+1)+T`, and
- `|E| = m(T+1)+qT+d(T+1)+dT`.

| Audit | Passed | Tested |
| --- | ---: | ---: |
| acyclic | 26,064 | 26,064 |
| node-count formula | 26,064 | 26,064 |
| edge-count formula | 26,064 | 26,064 |
| exact edge-family inventory | 26,064 | 26,064 |
| larger `d=6..20`, `T=1..5` constructions | 60 | 60 |

The one-shot graph has only `X union {S}`. Each unrolled graph instead has generation-indexed traits and factors plus exactly `T` reproduction indicators, so the structural distinction is explicit rather than inferred from a statistic.

## Destructive control

One inheritance edge is removed from an otherwise valid `G^(3)`. The mutant has one edge fewer than the closed-form requirement and is rejected by the same inventory gate.

## Evidence

Exact output: `outputs/exact_graph_audit.json`. Independent gates: `outputs/oracle_gates.json`. Executed mutation: `outputs/destructive_controls.json`.

## Limitations

This verifies the formal DAG construction, not the biological realism of independent, component-wise inherited factors. The paper identifies that assumption as a limitation.