axeyum-cas's Pratt certificate conditions are re-derived inside the kernel for every prime below the measured unary-numeral ceiling

Identifier: F:cas-ntheory-pratt-certificate-kernel-reconstructed
Proof route: cas-certificate
External status: proved
Axiom footprint: kernel.axiom-free-every-emitted-theorem-checked-by-Kernel-axiom-footprint-and-asserted-empty, cas.the-witness-and-the-factorization-come-from-the-cas-producer-the-kernel-re-checks-them-it-does-not-re-derive-them, cas.the-lucas-implication-is-not-reconstructed-only-the-certificate-conditions-are-so-nothing-here-establishes-primality, cas.the-translator-residue-of-and-factor-product-are-rust-and-are-checked-by-evaluation-tests-not-by-the-trusted-gate, cas.the-mersenne-89-headline-instance-is-out-of-reach-and-stays-cas-internal-see-F-cas-ntheory-pratt-primality-mersenne89

Recorded description

For each prime n in {2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47} and, recursively, every prime factor base appearing in its certificate tree, the Pratt (Lucas) certificate axeyum-cas's ntheory_certify::certify_prime produces -- a witness a, the complete prime factorization of n-1, and one subcertificate per factor base -- has each of its three arithmetic conditions re-derived as a kernel theorem admitted through crate::Kernel::add_declaration and axiom-free: Check.pratt_factorization_<n> : Eq Nat (prod q_i^e_i) (n-1) (the CAS checker's G6, completeness of the factorization); Check.pratt_fermat_<n> : Int.ModEq (ofNat n) (Int.pow (ofNat a) (n-1)) Int.one (G8); and Check.pratt_order_<n>_q<q> : Not (Int.ModEq (ofNat n) (Int.pow (ofNat a) ((n-1)/q)) Int.one) for each factor base q (G9, order maximality). The Fermat and order theorems are NOT closed by letting the kernel reduce a^(n-1) -- every Nat numeral here is unary, and that route walls below n = 20. They are built by square-and-multiply with reduction at every step, out of Int.pow_add, Int.pow_succ, Int.modEq_mul_general (unconditional in the modulus) and Int.modEq_trans, so the largest numeral the kernel forms is bounded by n^2. This does NOT establish that n is prime: the step from the certificate's conditions to primality is Lucas's theorem and is not derived here.

Formal statement

(for each n in {2,3,5,7,11,13,17,19,23,29,31,37,41,43,47} with certificate (a, [(q_i, e_i)]))
(theorem Check.pratt_factorization_n : Eq Nat (prod-pow [(q_i, e_i)]) (n - 1))
(theorem Check.pratt_fermat_n     : Int.ModEq (Int.ofNat n) (Int.pow (Int.ofNat a) (n - 1)) Int.one)
(theorem Check.pratt_order_n_q    : Not (Int.ModEq (Int.ofNat n) (Int.pow (Int.ofNat a) ((n - 1) / q)) Int.one))   ; one per factor base q
; each admitted by crate::Kernel::add_declaration with an empty axiom_footprint.
; NOT stated, and NOT implied: IsPrime n. The Lucas implication is absent.

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-reconstructed-pratt-certificate-conditions

Kind: kernel-term
Status: checked

Supports: for every prime in the reconstructed set and every factor base in its certificate tree, the G6/G8/G9 conditions of the CAS's own Pratt certificate are admitted as kernel theorems by crate::Kernel::add_declaration, each checked to be a Theorem (not an Axiom or Opaque) with an empty Kernel::axiom_footprint, against a pinned lower bound of 40 emitted theorems so a route that stopped after the first prime fails rather than passing quietly

Checker command

cargo test -p axeyum-lean-kernel --release --lib int_prelude::cas_pratt_bridge_tests::tests::pratt_certificates_are_kernel_reconstructed -- --exact 2>/dev/null | grep -cE '^test int_prelude::cas_pratt_bridge_tests::tests::pratt_certificates_are_kernel_reconstructed \.\.\. ok$'

Evidence notes

kernel-reconstructed (ADR-0601 SS2): the checker_command names axeyum-lean-kernel and the trust anchor is crate::Kernel::add_declaration. This closes, for the reachable primes only, the gap that fact F:cas-ntheory-pratt-primality-mersenne89's own notes named as structural ('a kernel reconstruction ... would hit the measured unary-numeral cost wall'). The prediction was right about the NAIVE route and wrong about the family: reducing at every step, rather than at the end, moves the wall from below n = 20 to several hundred. ADR-1622 records the measurement and the ceiling.

kernel-refuses-a-forged-pratt-witness

Kind: kernel-term
Status: checked

Supports: with EVERY guard belonging to this reconstruction route switched off (RouteGuards::none, which disables the CAS re-check, the Fermat-residue guard and the order-residue guard), crate::Kernel::add_declaration refuses two independent forgeries of the certificate for n = 11 -- a witness that fails Fermat outright (11, non-unit) and a witness that passes Fermat but has order 5 rather than 10 (3, the subtle forgery) -- while the GENUINE certificate run with the same guards off is still admitted, so the refusals are not an artefact of running with the guards off

Checker command

cargo test -p axeyum-lean-kernel --release --lib int_prelude::cas_pratt_bridge_tests::tests::a_corrupted_witness_is_refused_by_the_kernel -- --exact 2>/dev/null | grep -cE '^test int_prelude::cas_pratt_bridge_tests::tests::a_corrupted_witness_is_refused_by_the_kernel \.\.\. ok$'

Evidence notes

The two forgeries fail at DIFFERENT guards on purpose. Forgery A (witness 11) fails G8: the engine builds an honest proof of 11^10 = 0 (mod 11) and the kernel refuses it against the certificate's claim of 1. Forgery B (witness 3) PASSES G8 -- every unit modulo 11 satisfies Fermat -- and fails only G9 at q = 5; there the route hands the kernel the honest a^5 = 1 congruence against a statement asserting the negation, and the kernel refuses. Nothing is fabricated on either side of either refusal: the certificate's claim is the type, the true arithmetic is the term, and the trusted gate is what notices they disagree. A companion test (a_corrupted_factorization_is_refused_by_the_kernel) does the same for G6, using the incompleteness forgery the CAS module records as measured.

kernel-reconstructed-pratt-cost-ceiling-measured

Kind: witness-replay
Status: checked

Supports: the naive route (Eq.refl on emod (pow a m) n, letting the kernel form a^m) is shown to WORK at 3^6 = 729 -- so its absence at larger primes is a cost fact and not a correctness one -- and the reducing route is shown to land on the correct residue, and to REFUSE the neighbouring residue, at eleven (n, a, m) triples including exponents where the residue is not 1; a cost ladder over primes up to the pinned ceiling prints the wall-clock cost of each rung

Checker command

cargo test -p axeyum-lean-kernel --release --lib int_prelude::cas_pratt_bridge_tests::tests::the_reducing_route_reaches_primes_the_naive_one_cannot -- --exact 2>/dev/null | grep -cE '^test int_prelude::cas_pratt_bridge_tests::tests::the_reducing_route_reaches_primes_the_naive_one_cannot \.\.\. ok$'

Evidence notes

The cost ladder is the finding this fact's ceiling is set from, not a decoration: ADR-1622 records the printed numbers. The wall is a n^2 numeral cost and moves quadratically, which is why the reducing route reaches several hundred where the naive one stops below 20.

Provenance

{
  "date": "2026-09-04",
  "established_by": "lane cas-reconstruct (roadmap W1-13), ADR-1622: crates/axeyum-lean-kernel/src/int_prelude/cas_pratt_bridge_tests.rs reconstructs axeyum-cas's ntheory_certify::certify_prime output through crate::Kernel::add_declaration",
  "source": "the CAS certificate is read in-process from axeyum_cas::ntheory_certify::certify_prime -- the same producer F:cas-ntheory-pratt-primality-mersenne89's checker_command cites -- never hand-transcribed",
  "prior_art": [
    {
      "who": "Vaughan Pratt",
      "what": "Pratt certificates: a short, independently verifiable proof of primality via a witness of multiplicative order n-1 and the recursive factorization of n-1",
      "year": 1975,
      "where": "V. Pratt, \"Every Prime Has a Succinct Certificate\", SIAM Journal on Computing 4(3)",
      "attribution": "standard textbook/literature attribution; this lane did not consult the primary source"
    },
    {
      "who": "Edouard Lucas; D. H. Lehmer",
      "what": "the Lucas primality test -- the implication from a witness of order n-1 to the primality of n, which is exactly the step this fact does NOT reconstruct",
      "year": 1876,
      "where": "E. Lucas, \"Theorie des fonctions numeriques simplement periodiques\", American Journal of Mathematics 1; D. H. Lehmer, \"Tests for primality by the converse of Fermat's theorem\", Bulletin of the AMS 33 (1927)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}