ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 four square roots of one modulo $128$ are $1, 63, 65, 127$

Example

The solutions of $x^{2} \equiv 1 (m o d 128)$ are

$x \equiv 1, 63, 65, 127 (m o d 128) .$

Facts & Assumptions

Given: The modulus $128 = 2^{7}$ .

[L1]

Every unit modulo $2^{7}$ has a unique form $(- 1)^{ε} 5^{j}$ with $ε \in {0, 1}$ and $j$ modulo $32$ (For $k \geq 3$ , $(Z / 2^{k} Z)^{\times} ≅ C_{2} \times C_{2^{k - 2}}$ , generated uniquely as $(- 1)^{ε} 5^{j}$ ).

Verification

technique · direct

1.1

Any solution of $x^{2} = 1$ is a unit, with inverse $x$ . It therefore has the unique form in [L1]. Squaring that form gives $5^{2 j}$ , which is $1$ exactly when $32 ∣ 2 j$ , equivalently $j \equiv 0$ or $16 (m o d 32)$ .

L1algebra

1.2

Repeated squaring gives $5^{16} \equiv 65 (m o d 128)$ .

algebra

2.1

Combining the two values of $j$ from step 1.1 with the two signs gives $1, - 1, 65, - 65$ , namely $1, 127, 65, 63$ modulo $128$ ; uniqueness in [L1] shows there are no others.

step 1.1step 1.2L1∎

Depends on

For $k\ge3$, $(\mathbb Z/2^k\mathbb Z)^\times\cong C_2\times C_{2^{k-2}}$, generated uniquely as $(-1)^\varepsilon5^j$

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: 34 results over 7 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

Peter Hackman, Elementary Number Theory, Example C.IV.9 (standard reference, not scraped)

The four square roots of one modulo 128128 are 1,63,65,1271,63,65,127