ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Chinese remainder bijection $\mathbb{Z}/12\to\mathbb{Z}/3\times\mathbb{Z}/4$ computed on all standard representatives

Example

For standard representatives, the Chinese remainder map is

$a$	$([a]_3,[a]_4)$	$a$	$([a]_3,[a]_4)$
$0$	$([0]_3,[0]_4)$	$6$	$([0]_3,[2]_4)$
$1$	$([1]_3,[1]_4)$	$7$	$([1]_3,[3]_4)$
$2$	$([2]_3,[2]_4)$	$8$	$([2]_3,[0]_4)$
$3$	$([0]_3,[3]_4)$	$9$	$([0]_3,[1]_4)$
$4$	$([1]_3,[0]_4)$	$10$	$([1]_3,[2]_4)$
$5$	$([2]_3,[1]_4)$	$11$	$([2]_3,[3]_4)$

Facts & Assumptions

Given: The map $\Phi([a]_{12}):=([a]_3,[a]_4)$ .

[L1]

Every class modulo a positive integer has one standard representative (For $n\ge 1$ , every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$ , so $\lvert\mathbb{Z}/n\rvert=n$ ; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$ ).

[L2]

Since $3,4$ are coprime, $\Phi$ is a bijection and preserves addition and multiplication componentwise (Chinese remainder theorem for a finite pairwise-coprime list: simultaneous residues determine one class modulo the product, and the resulting bijection preserves addition and multiplication).

[L3]

Modular addition and multiplication are computed by adding and multiplying representatives (Addition and multiplication on $\mathbb{Z}/n$ by $[a]_n+[b]_n=[a+b]_n$ and $[a]_n[b]_n=[ab]_n$ ).

Verification

technique · direct

1.1

Reducing each integer $0,\ldots,11$ modulo $3$ and modulo $4$ gives the displayed table. Its entries are all distinct, and [L1] shows that they exhaust the domain and codomain standard pairs, in agreement with [L2].

L1L2

1.2

For a nontrivial addition check, $[7]_{12}+[8]_{12}=[3]_{12}$ , and the table gives $([1]_3,[3]_4)+([2]_3,[0]_4)=([0]_3,[3]_4)$ .

1.3

For a nontrivial multiplication check, $[5]_{12}[7]_{12}=[11]_{12}$ , and the table gives $([2]_3,[1]_4)([1]_3,[3]_4)=([2]_3,[3]_4)$ .

2.1

The table computes the whole bijection, while steps 1.2 and 1.3 instantiate its componentwise arithmetic preservation.

step 1.1step 1.2step 1.3L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

K. Conrad, The Chinese Remainder Theorem (standard reference, not scraped)

The Chinese remainder bijection Z/12→Z/3×Z/4\mathbb{Z}/12\to\mathbb{Z}/3\times\mathbb{Z}/4Z/12→Z/3×Z/4 computed on all standard representatives