E∞-page of the synthetic Adams SS #
BHS Corollary A.9, Proposition 3.12: The E∞-data for the synthetic Adams spectral sequence of ν(X).
Formalization bridge: The E∞-data is associated with the synthetic Adams
SS for ν(X). Links SynAdamsEInfty to SynAdamsSS.
Rigidity theorem #
The rigidity theorem (BHS Theorem A.8) states: E₂^{s,t,w}(SynAdamsSS(νX)) ≅ E₂^{s,t}(AdamsSS(X)) ⊗ F₂[λ]_w with differential correspondence d_r^syn(x) = λ^{r-1} · d_r^cl(x).
Since the full statement requires Z[λ]-module infrastructure not yet formalized, we axiomatize the key consequences: degeneration transfer and weight-range vanishing.
BHS Theorem A.8 (rigidity — degeneration transfer): If the classical Adams SS degenerates at page N, then the synthetic Adams SS for ν(X) also degenerates at page N.
BHS Theorem A.8 (rigidity — negative weight vanishing): For w < 0, E₂^{s,t,w}(SynAdamsSS(νX)) = 0. This is because E₂ ≅ E₂^cl ⊗ F₂[λ] and F₂[λ] has no negative degree part.
BHS Theorem A.8 (rigidity — above-diagonal vanishing): For w > t, E_r^{s,t,w}(SynAdamsSS(νX)) = 0 for all r ≥ 2. This reflects the F₂[λ]-module structure: the polynomial degree w is bounded by t.
λ-Bockstein spectral sequence #
The λ-Bockstein SS is obtained from the exact couple Σ^{0,1}(νX) →[λ] νX → νX/λ. The rigidity theorem implies it coincides with the synthetic Adams SS.
BHS Theorem A.1 (λ-Bockstein identification): The synthetic Adams SS for νX coincides with the λ-Bockstein SS. The key consequence: both start at page r₀ = 2 and have the same differential degrees. Full E₂-level identification requires Z[λ]-module formalization.
E∞ computations #
E∞ vanishing for ν(X) (BHS Prop 3.12): For t < w, E∞^{s,t,w}(νX) = 0. The permanent cycles in weight w cannot contribute below the diagonal t = w.
BHS Corollary A.9, Proposition 3.12: E∞ weight monotonicity for ν(X). For w₁ ≤ w₂ ≤ t, there is a natural surjection E∞^{s,t,w₁}(νX) ↠ E∞^{s,t,w₂}(νX). This reflects the quotient map Z∞/B_{1+t-w₁} → Z∞/B_{1+t-w₂} arising from B_{1+t-w₁} ⊆ B_{1+t-w₂}.
BHS Corollary A.9, Proposition 3.12: The weight maps are epimorphisms (surjections).
BHS Corollary A.11, Proposition 3.13: E∞ of ν(X)/λʳ vanishing. E∞^{s,t,w}(νX/λʳ) = 0 outside the range 0 ≤ t - w < r. The nonzero entries are isomorphic to Z_{r-t+w}/B_{1+t-w} of the classical Adams SS.