No trinomial x^8+x^k+1 is irreducible over GF(2), established by a shard-manifest Exhausted row whose exhaustion is re-run rather than trusted

Identifier: F:cas-gf2-degree-8-trinomial-exhaustion-rederived
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.gf2-dense-polynomial-arithmetic: candidate construction and irreducibility testing run in axeyum-cas's own Rust GF(2)[x] arithmetic (axeyum_cas::gf2::Gf2Poly / certify_irreducible), not through crate::Kernel::add_declaration., cas.rabin-irreducibility-criterion: each candidate's non-irreducibility is decided by the ABSENCE of a Rabin certificate under certify_irreducible's own search, which is the same criterion F:cas-gf2-degree-400-trinomial-irreducible takes as read for the positive case; here every candidate fails to produce one., cas.exhaustion-rederivation-shares-the-search-with-the-producer: check_shard_directory_with_policy re-derives the Exhausted verdict by calling the SAME search_sparse_half_degree the producer used (crate::gf2_search), under the manifest's own declared policy (manifest_view). It is an independent RUN of the identical deterministic algorithm, not an independently written second implementation the way gf2_independent is for the degree-400 certificate -- a defect shared between producer and this re-derivation could still evade both. What it rules out is a manifest lying about what its own declared search actually found, which is the specific gap ADR-1400 named., cas.gf2-no-kernel-carrier: crate::Kernel has no characteristic-2 polynomial ring. Building one is a new prelude, not a translator.

Recorded description

None of the four trinomials x^8+x+1, x^8+x^2+1, x^8+x^3+1, x^8+x^4+1 is irreducible over GF(2) -- these are exactly the trinomials of degree 8 the deterministic sparse search enumerates under a tail-terms-2 (trinomial-only) policy, in ascending middle-exponent order. The evidence is a shard manifest carrying a single ShardStatus::Exhausted row at degree 8 with candidates_tested = 4, admitted by axeyum_cas::gf2_shard::check_shard_directory_with_policy only after it RE-RUNS axeyum_cas::gf2_search::search_sparse_half_degree under the manifest's own declared policy and confirms both the outcome (Exhausted, not Found) and the exact candidate count. This is not a producer's word taken on trust: ADR-1400 flagged gf2_shard.rs's Exhausted claim as accepted with no re-derivation at the time of the audit; check_shard_directory_with_policy now re-derives it, and the negative control fabricated_exhaustion_is_refused shows a forged Exhausted claim at degree 4 -- where x^4+x+1 IS irreducible -- is rejected with the re-derivation surfacing the counterexample. Cas-internal under ADR-0601 SS2: this kernel has no GF(2)[x], so no bridge exists or is near.

Formal statement

(gf2-shard-exhaustion
  (degree 8) (policy (max-tail-terms 2) (max-candidates 100))
  (enumerated-trinomials (+ x^8 x^1 1) (+ x^8 x^2 1) (+ x^8 x^3 1) (+ x^8 x^4 1))
  (assert (forall f (in f enumerated-trinomials) (not (irreducible f (gf 2)))))
  (row (status Exhausted) (candidates-tested 4))
  (assert (= candidates-tested (rederive-via gf2_search::search_sparse_half_degree))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

cas-gf2-shard-degree-8-genuine-exhaustion

Kind: witness-replay
Status: checked

Supports: the shard manifest's Exhausted row at degree 8 (tail-terms<=2, 4 candidates) is admitted only after re-running the sparse search and confirming both the verdict and the exact candidate count

Checker command

cargo test -p axeyum-cas --lib gf2_shard::tests::genuine_exhaustion_is_admitted_and_charged -- --exact 2>/dev/null | grep -cE '^test gf2_shard::tests::genuine_exhaustion_is_admitted_and_charged \.\.\. ok$'

Evidence notes

Verified both directions on this host: the real test path gives count=1, exit=0; the same command against a deliberately wrong test path (…_WRONG) gives count=0, exit=1. `grep -cE` consumes the whole pipe so it cannot SIGPIPE, and the count is what is tested, so a renamed or deleted test is caught the same way a failing one is.

cas-gf2-shard-degree-4-fabrication-refused

Kind: witness-replay
Status: checked

Supports: a manifest claiming Exhausted at degree 4 -- where x^4+x+1 IS a genuine irreducible trinomial -- is refused: re-derivation finds the certificate the producer would have found and reports the fabricated exhaustion as unmasked

Checker command

cargo test -p axeyum-cas --lib gf2_shard::tests::fabricated_exhaustion_is_refused -- --exact 2>/dev/null | grep -cE '^test gf2_shard::tests::fabricated_exhaustion_is_refused \.\.\. ok$'

Evidence notes

This is the row that makes the first row a checker rather than a decoration: before the repair this audit's own predecessor document names, the entire acceptance body for an Exhausted row was `summary.exhausted += 1` and this exact forged manifest would have passed. Every other field of the forged manifest is well-formed (canonical JSON, complete population, no dangling evidence fields), so re-derivation is the ONLY thing standing between it and a PASS.

Provenance

{
  "date": "2026-09-01",
  "established_by": "lane cas-facts-round-two, following docs/research/11-design-review/2026-09-01-cas-certificate-reconstruction-audit.md's finding #2 (gf2_shard.rs Exhausted accepted on the producer's word) and confirming the repair it called for had since landed (rederive_exhaustion in gf2_shard.rs, calling gf2_search::search_sparse_half_degree). The re-derivation code and its tests pre-existed this fact; the ledger row did not.",
  "source": "the search enumeration and irreducibility testing are this repository's own (axeyum_cas::gf2_search, axeyum_cas::gf2); non-existence of a degree-8 irreducible trinomial over GF(2) is also independently known from published tables of irreducible trinomials (e.g. Zierler & Swan), which this lane did not cross-check against.",
  "prior_art": [
    {
      "who": "Michael O. Rabin",
      "what": "the irreducibility criterion the underlying certificates use (a Frobenius chain plus coprimality witnesses at each prime divisor of the degree)",
      "year": 1980,
      "where": "SIAM Journal on Computing 9(2), 273-280",
      "attribution": "standard attribution; this lane did not consult the primary source"
    }
  ]
}