Header-only C++20 library for arithmetic in Z2[[t]]: carry chains, formal derivatives, forward differences, Witt vectors, basis conversions, power series composition and reversion. Umbrella header dyadic.h includes all sub-headers from include/dyadic/.

#include <dyadic.h>
#include <cstdio>
using namespace dyadic;
int main() {
 Polynomial<4, uint64_t> p{{1, 2, 3, 4}};
 // Formal derivative: D(P)(t) = dP/dt
 auto dp = formal_derivative(p); // {2, 6, 12, 0}
 for (auto c : dp) std::printf("%lu ", c);
 // Forward difference: Δ(P)(t) = P(t+1) − P(t)
 auto fp = forward_difference(p); // {9, 18, 12, 0}
 // Basis conversions (exact roundtrip)
 auto ff = change_basis<FallingFactorialBasis>(p);
 auto back = change_basis<MonomialBasis>(ff); // == p
 // Evaluate P(5) = 1 + 2·5 + 3·25 + 4·125 = 586
 auto y = p.eval(5);
 // Witt vector ring operations
 WittVector<3, uint64_t> a{{1, 2, 3}}, b{{4, 5, 6}};
 auto sum = a + b; // Witt addition (via ghost map)
 auto prod = a * b; // Witt multiplication
 // Power series reversion (Lagrange inversion)
 Polynomial<6, uint64_t> P{{0, 1, 1}}; // t + t2
 auto Q = reversion(P);
 // Q = t − t2 + 2t3 − 5t4 + 14t5 − 42t6 + ...
 // (stored as unsigned Z2 values: −1 ≡ 264−1, etc.)
}

• C++20 compiler (GCC 12+, Clang 17+, MSVC 2022+)
• No external dependencies
• detail::uint128_t (software 128-bit pair) provides uint64_t word support without unsigned __int128
• Clang needs -fconstexpr-steps=50000000 for compile-time proofs; GCC needs -fconstexpr-ops-limit=200000000

WittVector<3, uint64_t> a{{1, 2, 3}}, b{{4, 5, 6}};
auto sum = a + b;
auto prod = a * b;
// Frobenius and Verschiebung
auto fa = a.frobenius();
auto vb = b.verschiebung();
// F(V(a)) == V(F(a)) — verified at compile time
// Adams operation ψn
auto psi = adams_operation(a, 3);
// Teichmüller lift: τ(x) = (x, 0, 0, ...) (N is required)
auto tau = teichmueller_lift<4>(uint64_t{7});
// ghost_j(τ(ab)) = ghost_j(τ(a)) · ghost_j(τ(b)) — verified at compile time

// NOTE: operator* uses carry-chain (2-adic ring).
// poly_divmod_cw / poly_gcd_cw use coefficient-wise (standard ring).
// Use poly_mul_cw() and verify_divmod_cw() for verification.
Polynomial<3, uint64_t> A{{1, 2, 1}}; // (x+1)2
Polynomial<2, uint64_t> B{{1, 1}}; // (x+1)
auto [Q, R] = poly_divmod_cw(A, B); // Q=(x+1), R=0
bool ok = verify_divmod_cw(A, Q, B, R); // true: A=Q·B+R ✓
auto G = poly_gcd_cw(A, B); // G=(x+1) — divides both

Polynomial<6, uint64_t> P{{0, 1, 1}}; // P(t) = t + t2
Polynomial<6, uint64_t> Q{{0, 1, 2}}; // Q(t) = t + 2t2
auto PQ = compose(P, Q); // P(Q(t)) — degree (N-1)*(M-1)+1 = 26
auto R = reversion(P); // Lagrange inverse: P(R(t)) = t
// R(t) = t − t2 + 2t3 − 5t4 + 14t5 − 42t6 + ...
// (stored in Z2: negative coefficients wrap modulo 2^W)

#include <dyadic/verify.h> // triggers all static_asserts at compile time
// If it compiles, all 22 named static_assert proofs passed.

Day-to-day compiles include a sampled subset. For the full exhaustive suite (2562 cases, 8K+ multiplication cases), define DYADIC_HEAVY_PROOFS.

Polynomial<6, uint8_t> p{{0, 0, 0, 0, 0, 255}};
if (!check_taylor_roundtrip_precision(p))
 // T5 = 5! · 255 = 30600 > 256 — high bits lost
WittVector<4, uint32_t> w{{1, 2, 3, 4}};
if (!check_witt_recovery_precision(w))
 // Some rj ≥ 232−j — ghost recovery inexact

As a header collection — copy dyadic.h and the include/dyadic/ directory into your project's include path, then #include <dyadic.h> (umbrella) or #include <dyadic/core.h> (individual header).

With CMake:

cmake -B build -DDYADIC_BUILD_TESTS=ON
cmake --build build
ctest --test-dir build

Optional: -DDYADIC_HEAVY_PROOFS=ON for exhaustive compile-time proofs.

Via CI script:

./ci_compile_check.sh

All tests pass under GCC 14+ and Clang 17+ with ASan+UBSan. CI covers GCC (light + heavy proofs), Clang, and MSVC on Windows.

• Two ring semantics: operator* uses carry-chain poly_mul (correct Z2 arithmetic with overflow propagation). Functions with _cw suffix (poly_divmod_cw, poly_gcd_cw, poly_mul_cw) operate coefficient-wise (standard ring). These are different rings — use poly_mul_cw() and verify_divmod_cw() to verify divmod/gcd results.
• quad_width<W> alias: Shorthand for widen_t<dword_t<W>> (up to ×ばつ word width), used by ghost-map accumulation and unsaturated polynomial products.
• assert preconditions: All silent-failure points (poly_divmod_cw with zero/even divisor, witt_exp with v2(a0) < 2, witt_log/witt_inverse with even a0, reversion with even P[1]) now use assert(). Invalid inputs trigger SIGABRT in debug builds. A few functions return 0 for invalid inputs by design rather than asserting: poly_discriminant_cw returns 0 when degree < 1 or leading coefficient is even; det_laplace returns 0 for dim > 6 (use Bareiss via determinant_cw instead).
• Compile-time cached Stirling/Pascal tables: detail::STIRLING_CACHE<N,W> and detail::PASCAL_CACHE<N,W> are inline constexpr globals — computed once per (N,W) at compile time, shared across all basis conversion and difference calls.
• Auto-vectorization hints: poly_mul_unsaturated and poly_mul use DYADIC_RESTRICT (__restrict__) and #pragma GCC ivdep on their inner multiply-accumulate loops, enabling the compiler to generate SIMD code for runtime invocations without breaking constexpr.

See docs/complexity.md for a complete function-by-function breakdown.

All operations are constexpr; runtime performance matches compile-time complexity bounds. The carry-chain poly_mul and mul_unsigned are auto-vectorized with SIMD hints (#pragma GCC ivdep, DYADIC_RESTRICT) and use hardware unsigned __int128 accumulation for uint64_t where available.

• Polynomial::degree() renamed to max_degree(): The old name was misleading (it returned N−1, the maximum possible degree, not the actual degree). Added actual_degree() member function.
• Taylor basis roundtrip: T_k = k! · FF_k wraps when FF_k ≥ 2^W / k!. Use small coefficients for exact roundtrips. FallingFactorial basis has no such limitation.
• Witt precision window: Recovery r_j = (G_j − S_j) / 2^j requires r_j < 2^{W−j}.
• Witt exp/log term truncation: Uses valuation-aware dynamic term counting with ×ばつ bit-width budget. Requires v2(x) ≥ 2 for exp convergence (mathematical limit — v2(x) = 1 stalls at ≤ log2(n)+1). Log converges for v2(y) ≥ 1 (~135 terms at 128-bit).
• detail::uint128_t is a software 128-bit pair — no unsigned __int128 required. __int128 is used as a hot-path optimization in binom() (dyadic/combinatorial.h), poly_mul() and mul_unsigned() (dyadic/core.h/arith.h, ×ばつ speedup at deg=63 for uint64_t), div_unsigned_knuth() (dyadic/arith.h, hardware trial-division / multiply-subtract for ×ばつ speedup), and the p-adic series in witt_log/witt_exp (dyadic/witt.h, hardware multiply-accumulate). All paths guarded by __SIZEOF_INT128__.

This project is made available under the terms of the MIT License.