ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-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 congruence $14x\equiv30\pmod{100}$ has exactly the two solutions $x\equiv45,95\pmod{100}$

Example

The congruence $14x\equiv30\pmod{100}$ has exactly the solution classes

$[45]_{100}\quad\text{and}\quad[95]_{100}.$

Facts & Assumptions

Given: The congruence $14x\equiv30\pmod{100}$ .

[L1]

A linear congruence $ax\equiv b\pmod n$ is solvable exactly when $\gcd(a,n)\mid b$ , and then has exactly $\gcd(a,n)$ solution classes modulo $n$ (For $n\ge1$ , $ax\equiv b\pmod n$ is solvable exactly when $\gcd(a,n)\mid b$ , and then has exactly $\gcd(a,n)$ solution classes modulo $n$ ).

[L2]

The extended Euclidean algorithm produces gcds and Bézout coefficients (The extended Euclidean algorithm: the same descent produces integers $x, y$ with $ax + by = \gcd(a,b)$ , so Bézout coefficients are computed and not merely shown to exist).

[L3]

Congruence modulo $n$ means divisibility of a difference by $n$ (Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$ , including the moduli $0$ and $1$ ).

Verification

technique · direct

1.1

The Euclidean algorithm gives $\gcd(14,100)=2$ , and $2\mid30$ . Cancelling the common factor reduces the congruence to $7x\equiv15\pmod{50}$ .

L1L2L3

1.2

Since $7\cdot43=301\equiv1\pmod{50}$ , multiplication by $43$ gives $x\equiv43\cdot15=645\equiv45\pmod{50}$ .

1.3

The two lifts of this class modulo $100$ are $45$ and $45+50=95$ , and both verify the original congruence: $14\cdot45-30=600$ and $14\cdot95-30=1300$ are divisible by $100$ .

2.1

By [L1] there are exactly two solution classes modulo $100$ , so the two distinct classes in step 1.3 exhaust them.

step 1.1step 1.2step 1.3L1∎

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: 63 results over 22 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

Mathematics LibreTexts, Linear Congruences (standard reference, not scraped)
UPC, Modular Arithmetic notes (standard reference, not scraped)

The congruence 14x≡30(mod100)14x\equiv30\pmod{100}14x≡30(mod100) has exactly the two solutions x≡45,95(mod100)x\equiv45,95\pmod{100}x≡45,95(mod100)