+++ title = “Cross-Validation Methodology” section = “mathematics” +++
Cross-Validation Methodology
htpy computes five interrelated spectral sequences. These computations are not independent: they are connected by natural maps, comparison theorems, and convergence relationships. htpy exploits these connections as a validation framework, checking that independently computed data agrees where it should.
The validation checks
htpy implements 7 systematic checks, labeled V1 through V7. Each compares two independently computed datasets:
V1: CESS $E_2$ $\geq$ Adams $E_2$ (per-stem totals)
$$\sum_s \dim E_2^{s,n+s}(\text{CESS}) ;\geq; \sum_s \dim E_2^{s,n+s}(\text{Adams})$$
Justification. The CESS converges to the Adams $E_2$ page. Differentials can only decrease dimensions, so the $E_2$ page is at least as large as $E_\infty$.
Sub-checks:
- V1b: Per-bidegree inequality (stronger, but sensitive to the $h_0$ generator placement between $E^$ and $P^$).
- V1c: CESS weight counts at each bidegree match Ext dimensions.
V3: aNSS $E_2$ $\geq$ aNSS $E_\infty$ (per-stem totals)
$$\sum_s \dim E_2^{s,n+s}(\text{aNSS}) ;\geq; \sum_s \dim E_\infty^{s,n+s}(\text{aNSS})$$
Justification. Same reasoning as V1: the aNSS differentials can only decrease dimensions.
Sub-check V3b: aNSS $d_2$ matrix dimensions match $E_2$ dimensions at both source and target bidegrees (849 entries verified).
V5: $C\tau$ Ext $\geq$ Novikov $E_2$ generator counts
$$\dim \operatorname{Ext}^{s,t,w}(C\tau) ;\geq; \text{(Novikov CSV generator count)}$$
Justification. By the Gheorghe–Wang–Xu isomorphism, $C\tau$ Ext equals the Adams–Novikov $E_2$ page. The CSV generator counts may undercount due to $h_0$-tower truncation, so the inequality is $\geq$.
V6: Motivic Adams (JSON) = Isaksen CSV $E_2$
Four sub-checks:
- V6: Round-trip CSV $\to$ JSON fidelity (dimensions match at every tridegree).
- V6b: Per-stem $E_2 \geq E_\infty$ monotonicity.
- V6c: $d_2$ matrix dimensions match $E_2$ at source and target.
- V6d: Metadata consistency (weight ranges, torsion flags).
V7: $\tau$-free motivic Adams $E_2$ = Classical Adams $E_2$
$$\dim \operatorname{Ext}{A{\mathrm{mot}}}^{s,t,t}(\mathbb{F}_2, \mathbb{F}_2) ;=; \dim \operatorname{Ext}_A^{s,t}(\mathbb{F}_2, \mathbb{F}_2)$$
Justification. At the top weight $w = t$ (equivalently $w = n + s$), the motivic Steenrod algebra reduces to the classical Steenrod algebra. The $\tau$-free (top-weight) part of the motivic $E_2$ page equals the classical $E_2$ page.
Verified for $n = 1, \ldots, 33$ and $s \leq 9$.
Test suite
All checks are implemented as automated tests in
tests/cross_validate_ss.rs. The test suite runs as part of
cargo test (quick checks) and cargo test -- --ignored (full
validation including expensive CSV parsing).
Reference data sources
| Source | Description | Location |
|---|---|---|
| BFCC | $\operatorname{Ext}_A$ ranks through stem 256, $d_2$ | reference_data/S0-p2/bfcc/ |
| Bruner–Rognes | Ext basis, generators, relations | reference_data/S0-p2/bruner-rognes/ |
| LWX | Machine-proved Adams differentials, Kervaire CW data | reference_data/cw-spectra/lwx/ |
| Isaksen (motivic) | Motivic Adams $E_2$–$E_6$, $E_\infty$ | reference_data/motivic/isaksen-adams/ |
| Isaksen (Novikov) | Algebraic Novikov $E_2$–$E_5$, $E_\infty$ | reference_data/novikov/isaksen-novikov/ |
What “validated” means
When htpy says a computation is “validated,” it means:
- The computation was performed independently by htpy’s resolution engine.
- The output was compared against at least one external reference dataset.
- All applicable V-checks passed within the overlapping range.
This does not constitute a formal proof. For formal verification, htpy can export Lean 4 certificates that check $d^2 = 0$ and exactness of the resolution.