axeyum-cas's CRT certificate (both the solution and the inconsistency direction) is independently re-checked across six systems, and every one of them is re-derived inside the kernel

Identifier: F:cas-ntheory-crt-certificate
Proof route: cas-certificate
External status: proved
Axiom footprint: kernel.axiom-free-every-emitted-theorem-checked-by-Kernel-axiom-footprint-and-asserted-empty, cas.exact-i128-modular-arithmetic-independent-of-ntheory, cas.independent-gcd-lcm-checker-gcd-checker-lcm-added-2026-08-31-see-notes, cas.the-solution-the-modulus-and-the-conflicting-pair-come-from-the-cas-producer-the-kernel-re-checks-them-it-does-not-re-derive-them, cas.uniqueness-of-the-solution-modulo-M-is-not-among-the-reconstructed-obligations-Int-crt-unique-is-proved-in-int-prelude-crt-and-is-not-used-here

Recorded description

For each of the solvable congruence systems x=2(mod 3), x=3(mod 5), x=2(mod 7) (unique solution 23 mod 105); x=1(mod 4), x=3(mod 6) (non-coprime moduli, unique solution 9 mod 12); the empty system (trivial solution 0 mod 1); and x=5(mod 1) (trivial modulus), axeyum-cas's ntheory_certify::certify_crt produces a CrtCertificate::Solution{solution, modulus}, and ntheory_certify::check_crt_certificate independently re-derives and confirms: the solution is canonical (0 <= solution < modulus), every input congruence holds, AND modulus is the LEAST common multiple of the input moduli (not merely a common one -- recording only a common multiple would accept, e.g., 24 as a 'modulus' for the second system, which satisfies both congruences and is a common multiple of 4 and 6, but is not the least one, 12). For each of the inconsistent systems x=0(mod 2), x=1(mod 4) and x=1(mod 6), x=2(mod 9), x=3(mod 4), certify_crt instead produces a CrtCertificate::Inconsistent{left, right} naming a genuinely conflicting pair of congruences, independently re-verified by recomputing gcd(m_left, m_right) and confirming a_left != a_right modulo it. Every numeral appearing in all six systems is at most 105, so unlike the Pratt family (whose ledger headline is 2^89-1) the kernel can reach ALL of them: crates/axeyum-lean-kernel/src/int_prelude/cas_crt_bridge_tests.rs re-derives each certificate's obligations as theorems admitted through crate::Kernel::add_declaration and axiom-free -- Check.crt_congruence_<id>_<i> : Int.ModEq (ofNat m_i) (ofNat x) (ofNat a_i) (the checker's R3), Check.crt_least_modulus_<id> : Eq Nat (Nat.lcm-fold of the moduli) M (R4, LEASTNESS, the guard that rejects 24 for the second system), Check.crt_canonical_<id> : Nat.lt x M (R2), and, for each inconsistent system, Check.crt_inconsistent_<id> : forall (x : Int), Int.ModEq (ofNat m_left) x (ofNat a_left) -> Int.ModEq (ofNat m_right) x (ofNat a_right) -> False (R6). The last is universally quantified over x, so no reduction can close it: it goes through Int.modEq_of_mul_left at g = gcd(m_left, m_right), then Int.modEq_symm and Int.modEq_trans to Int.ModEq g a_left a_right, which unfolds to a false equation between two distinct numerals.

Formal statement

(assert (and
  (crt-solution (2 3) (3 5) (2 7)) = (23 . 105)
  (crt-solution (1 4) (3 6)) = (9 . 12)                 ; non-coprime moduli, LEAST common multiple 12
  (crt-solution) = (0 . 1)                              ; empty system, trivial
  (crt-solution (5 1)) = (0 . 1)                        ; trivial modulus
  (crt-inconsistent (0 2) (1 4))                        ; 0 != 1 (mod gcd(2,4)=2)
  (crt-inconsistent (1 6) (2 9) (3 4))                  ; a genuinely conflicting pair exists
))
; where crt-solution's SECOND component is REQUIRED to be the least common
; multiple of the input moduli, independently re-derived by
; check_crt_certificate's R4 guard -- not merely a common multiple.
; kernel-reconstructed (ADR-1622): each of the six systems' obligations is
; admitted by crate::Kernel::add_declaration as
;   Check.crt_congruence_<id>_<i> / Check.crt_least_modulus_<id> /
;   Check.crt_canonical_<id> / Check.crt_inconsistent_<id>
; with an empty Kernel::axiom_footprint. NOT reconstructed: Int.crt_exists
; and Int.crt_unique are proved elsewhere in int_prelude and are not used
; here, so uniqueness of the solution modulo M is not connected to these
; theorems.

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

cas-internal-crt-six-systems

Kind: witness-replay
Status: checked

Supports: certify_crt produces a correct Solution certificate (with the LEAST common multiple, not merely a common one) for four solvable systems, and a correct Inconsistent certificate for two unsolvable systems; check_crt_certificate independently re-derives and confirms each

Checker command

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

Evidence notes

cas-internal (ADR-0601 SS2): checker_command names only axeyum-cas. FINDING FROM THIS FACT'S OWN REGISTRATION (ADR-1055): as first written, check_crt_certificate's R4 (leastness) and R6 (conflict) guards called crate::ntheory::lcm/crate::ntheory::gcd DIRECTLY -- correct, but not independent of the crate this checker exists to check, and in tension with this module's own stated design principle ('written here rather than reused from ntheory on purpose') and with ADR-0745's claim that 'the modular arithmetic is this module's own, not ntheory's', which as written did not actually cover gcd/lcm. Fixed before this fact was registered: added checker_gcd/checker_lcm (a from-scratch Euclidean algorithm) and routed R4/R6 through them; added ntheory_certify_tests::independent_gcd_lcm_agree_with_ntheory (72 comparisons) pinning agreement with ntheory::gcd/ntheory::lcm the same way the module already does for pow_mod. Re-ran the adversarial mutation sweep (scripts/tests/test-ntheory-certificate-guards.sh) after the fix: R4 and R6 are still each killed by their existing forgery fixtures (forged_crt_modulus_is_a_common_multiple_but_not_the_least; forged_crt_rejects_a_fabricated_conflict_over_a_solvable_system + forged_crt_rejects_out_of_range_conflict_indices), measured=23 survivors=3 unchanged (G1/G5/G10, the three documented resource guards).

cas-internal-crt-gcd-lcm-independence

Kind: witness-replay
Status: checked

Supports: the checker_gcd/checker_lcm helpers check_crt_certificate now uses agree with crate::ntheory::gcd/crate::ntheory::lcm across 72 (a,b) pairs, so the independence fix did not change what the checker accepts or rejects, only where its arithmetic comes from

Checker command

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

Evidence notes

cas-internal (ADR-0601 SS2). Supporting evidence for the fix described in the first evidence row's notes, added 2026-08-31 alongside this fact.

kernel-reconstructed-crt-all-six-systems

Kind: kernel-term
Status: checked

Supports: all six systems -- four solvable, two inconsistent -- have every obligation of their CAS certificate admitted as a kernel theorem by crate::Kernel::add_declaration, each checked to be a Theorem (not an Axiom or Opaque) with an empty Kernel::axiom_footprint, against pinned counts (exactly 4 solvable, exactly 2 inconsistent, at least 16 theorems) so a run that silently covered only one direction fails rather than passing quietly

Checker command

cargo test -p axeyum-lean-kernel --release --lib int_prelude::cas_crt_bridge_tests::tests::crt_certificates_are_kernel_reconstructed -- --exact 2>/dev/null | grep -cE '^test int_prelude::cas_crt_bridge_tests::tests::crt_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 fact is the one number-theory certificate family whose EVERY claimed instance the kernel can reach -- its largest numeral is 105, where the Pratt family's headline is a 27-digit Mersenne number -- which is why it flips whole rather than being split under ADR-0603. ADR-1622 records the cost comparison that chose it.

kernel-refuses-a-merely-common-crt-modulus

Kind: kernel-term
Status: checked

Supports: with EVERY guard belonging to the reconstruction route switched off (RouteGuards::none), crate::Kernel::add_declaration refuses the CAS module's own recorded near-miss -- residues [(1,4),(3,6)] with modulus 24, which satisfies both congruences, IS a common multiple, and leaves the solution canonical, so only leastness separates it from 12 -- and also refuses a fabricated Inconsistent witness naming a pair that does not conflict, while the GENUINE certificates run with the same guards off are still admitted

Checker command

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

Evidence notes

This is the kernel-side counterpart of the R4 leastness guard whose independence this fact's own registration once had to fix on the CAS side (see the first evidence row's notes). The reconstruction does not inherit that fix -- it restates leastness over the kernel's own Nat.lcm, so the two checks share no arithmetic at all. A companion test (a_fabricated_conflict_is_refused_by_the_kernel) covers the R6 direction over the three-congruence system, where only the pair (0,1) genuinely conflicts and the pair (1,2) does not.

Provenance

{
  "date": "2026-08-31",
  "established_by": "axeyum-cas ntheory_certify::certify_crt / ntheory_certify::check_crt_certificate (crates/axeyum-cas/src/ntheory_certify.rs, landed per ADR-0745); independence fix (checker_gcd/checker_lcm) and this fact's registration both per ADR-1055",
  "source": "the existing unit test ntheory_certify::ntheory_certify_tests::certifies_crt_in_both_directions, read directly from crates/axeyum-cas/src/ntheory_certify/ntheory_certify_tests.rs",
  "prior_art": [
    {
      "who": "Sun Tzu (Sunzi); traditionally the Chinese Remainder Theorem",
      "what": "existence and uniqueness (modulo the LCM) of a simultaneous solution to a system of congruences with pairwise coprime moduli; the non-coprime generalisation used here is a routine extension",
      "year": 400,
      "where": "Sunzi Suanjing (Master Sun's Mathematical Manual), circa 3rd-5th century CE",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}