axeyum-cas's prime factorization certificate is independently re-checked across eight instances, including negatives and units

Identifier: F:cas-ntheory-factorization-certificate
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.factorization-certificate-not-kernel-reconstructed, cas.exact-i128-modular-arithmetic-mul-mod-pow-mod-written-independently-of-ntheory, cas.reuses-the-pratt-primality-checker-per-factor-base-not-the-pratt-producer

Recorded description

For each n in {1, -1, 12, -12, 360, 1024, 2147483647, 1999966} (the last = 999983 * 2, a large prime times two), axeyum-cas's ntheory_certify::certify_factorization produces a FactorizationCertificate -- the (prime, exponent) list together with a Pratt certificate per prime base -- and ntheory_certify::check_factorization_certificate independently re-derives and confirms: the bases are strictly ascending (canonical, duplicate-free), every exponent is at least one, the product prod(base^exponent) equals |n| exactly, and every base is itself certified prime via the independent Pratt route (F:cas-ntheory-pratt-primality-mersenne89's checker, check_primality_certificate). n=0 has no certificate -- the empty product is 1 and no finite product of primes is 0, so certify_factorization(0) correctly returns None.

Formal statement

(assert (and
  (forall ((n Int)) (=> (member n (1 -1 12 -12 360 1024 2147483647 1999966))
    (exists ((factors (List (Pair Int Nat))))
      (and (strictly-ascending (map fst factors))
           (forall ((e Nat)) (=> (member e (map snd factors)) (>= e 1)))
           (= (prod-pow factors) (abs n))
           (forall ((p Int)) (=> (member p (map fst factors)) (is-prime p)))))))
  (not (exists ((factors (List (Pair Int Nat)))) (certifies-factorization 0 factors)))))
; independently re-derived by ntheory_certify::check_factorization_certificate,
; which itself calls check_primality_certificate (not certify_prime) per factor base.

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

cas-internal-factorization-eight-instances

Kind: witness-replay
Status: checked

Supports: certify_factorization produces a canonical prime factorization for eight instances spanning negatives, units, a large-prime-times-two, and a Mersenne prime, and check_factorization_certificate independently re-derives the product identity plus per-factor primality; certify_factorization(0) correctly declines

Checker command

cargo test -p axeyum-cas --lib ntheory_certify::ntheory_certify_tests::certifies_factorizations_including_negatives_and_units -- --exact 2>/dev/null | grep -cE '^test ntheory_certify::ntheory_certify_tests::certifies_factorizations_including_negatives_and_units \.\.\. ok$'

Evidence notes

cas-internal (ADR-0601 SS2): checker_command names only axeyum-cas. check_factorization_certificate's per-factor primality check calls check_primality_certificate (the CHECKER), not certify_prime (the PRODUCER) -- grepped directly at the F5 guard site -- so this route does not silently trust the factorization's own primality claim about its bases; it re-derives it via the same independent Pratt route as F:cas-ntheory-pratt-primality-mersenne89. Proved by breaking: see ADR-1055 for the break/restore transcript run during registration.

Provenance

{
  "date": "2026-08-31",
  "established_by": "axeyum-cas ntheory_certify::certify_factorization / ntheory_certify::check_factorization_certificate (crates/axeyum-cas/src/ntheory_certify.rs, landed per ADR-0745); this fact registers it into the ledger per ADR-1055",
  "source": "the existing unit test ntheory_certify::ntheory_certify_tests::certifies_factorizations_including_negatives_and_units, read directly from crates/axeyum-cas/src/ntheory_certify/ntheory_certify_tests.rs",
  "prior_art": [
    {
      "who": "Euclid; Gauss",
      "what": "existence and uniqueness of prime factorization (the Fundamental Theorem of Arithmetic)",
      "year": -300,
      "where": "Euclid's Elements, Book IX (existence); Gauss's Disquisitiones Arithmeticae, 1801 (the modern uniqueness statement)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}