CounterexampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Mixing scaled and unscaled Minkowski covolumes fails

Statement refuted

For $K = Q (i)$ the unscaled Minkowski image of $O_{K}$ is $Z^{2}$ , of covolume $1$ , and the $\sqrt{2}$ -scaled image, obtained by multiplying both real coordinates of the unscaled embedding by $\sqrt{2}$ , is the lattice $\sqrt{2} Z^{2}$ , of covolume $2$ . The statement refuted is the claim that the unscaled covolume $2^{- r_{2}} \sqrt{∣ d_{K} ∣} = 1$ may serve as the covolume of the scaled lattice $\sqrt{2} Z^{2}$ in the equality form of Minkowski's theorem. Assume the Axiom of Choice. The closed disc of radius $6 / 5$ has area $36 π / 25 > 4 = 2^{2} \cdot 1$ and is compact, convex and centrally symmetric, so under that claim Minkowski's equality criterion would predict a nonzero point of $\sqrt{2} Z^{2}$ in the disc; but every nonzero vector of $\sqrt{2} Z^{2}$ has length $\sqrt{2} > 6 / 5$ . The correct covolume of the scaled lattice is $2$ , and with the threshold $2^{2} \cdot 2 = 8 > 36 π / 25$ the true criterion makes no prediction. Mixing the two normalizations is therefore invalid.

Facts & Assumptions

Given: The Axiom of Choice, the field $K = Q (i)$ , its ring of integers $O_{K} = Z [i]$ , the unscaled Minkowski embedding $σ$ , and the closed disc $D = {x \in R^{2} : ∣ x ∣ \leq 6 / 5}$ .

[A1]

The Axiom of Choice implies the Axiom of Countable Choice (AC implies DC implies countable choice), the choice hypothesis of the area computation [F5], invoked in step 1.2; the equality-form Minkowski criterion [F6] is applied under the Axiom of Choice assumed in the statement.

[F1]

For $d = - 1$ the quadratic-field formulas give $O_{Q (\sqrt{- 1})} = Z [\sqrt{- 1}] = Z [i]$ and $d_{K} = 4 \cdot (- 1) = - 4$ (Integers in a quadratic field, Discriminant of a quadratic field).

[F2]

$K = Q (i)$ has signature $(r_{1}, r_{2}) = (0, 1)$ , and the unscaled Minkowski embedding sends $x$ to the pair $(Re τ (x), Im τ (x))$ of the single complex embedding; hence $σ (O_{K}) = Z^{2}$ (Unscaled Minkowski embedding).

[F3]

For a nonzero integral ideal $a$ the unscaled image is a full lattice with $covol (σ (a)) = 2^{- r_{2}} \sqrt{∣ d_{K} ∣} N a$ ; applied to $a = O_{K}$ this gives $covol (σ (O_{K})) = 2^{- 1} \sqrt{4} = 1$ (Covolume of an integral ideal lattice).

[F4]

For a full lattice with $Z$ -basis $b_{1}, \dots, b_{n}$ the covolume is $∣ \det (b_{1}, \dots, b_{n}) ∣$ ; the scaled lattice $\sqrt{2} Z^{2}$ has basis $\sqrt{2} e_{1}, \sqrt{2} e_{2}$ , so its covolume is $∣ \det (\sqrt{2} I_{2}) ∣ = 2$ (Full Euclidean lattice and covolume).

[F5]

The closed disc of radius $ρ$ has area $π ρ^{2}$ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F6]

Minkowski convex-body theorem at equality: a compact convex centrally symmetric $C \subseteq R^{n}$ with $vol (C) \geq 2^{n} covol (Λ)$ contains a nonzero point of the full lattice $Λ$ (Minkowski convex-body theorem at equality).

[F7]

The finite-remainder Gregory--Leibniz formula at $N = 7$ has partial sum $33976 / 45045 > 3 / 4$ and positive remainder, so $π > 3 > 25 / 9$ . At $N = 2$ the partial sum is $13 / 15$ and the remainder is negative, so $π / 4 < 13 / 15 < 1$ and $π < 4$ (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

Proof

1.1F1F2F3

By [F1] the field is $K = Q (i)$ with $O_{K} = Z [i]$ and $d_{K} = - 4$ , so $r_{2} = 1$ and [F3] gives $covol (σ (O_{K})) = 2^{- 1} \sqrt{4} = 1$ , while [F2] identifies the unscaled lattice itself as $σ (O_{K}) = Z^{2}$ .

1.2F5F7A1givenalgebra

The disc $D = {x \in R^{2} : ∣ x ∣ \leq 6 / 5}$ is compact, convex and centrally symmetric, and by [F5], with the Countable Choice hypothesis supplied by [A1], its area is $π (6 / 5)^{2} = 36 π / 25$ . By [F7], $π > 3 > 25 / 9$ , so this area exceeds $4 = 2^{2} \cdot 1$ .

2.1F4step 1.1

The scaled lattice is $Γ : = \sqrt{2} Z^{2} = {(\sqrt{2} a, \sqrt{2} b) : a, b \in Z}$ , the image of $O_{K}$ under the coordinatewise $\sqrt{2}$ -scaling of $σ$ ; by [F4] its covolume is $covol (Γ) = ∣ \det (\sqrt{2} I_{2}) ∣ = 2$ .

3.1step 2.1algebra

Every nonzero $x = (\sqrt{2} a, \sqrt{2} b) \in Γ$ has $∣ x ∣^{2} = 2 (a^{2} + b^{2}) \geq 2 > 36 / 25 = (6 / 5)^{2}$ , so $∣ x ∣ > 6 / 5$ and $x \notin D$ ; hence $D \cap Γ = {0}$ .

4.1F6step 1.2step 3.1

If the unscaled covolume $1$ were used as the covolume of $Γ$ , then step 1.2 would verify all hypotheses of the equality-form criterion [F6] for $C = D$ and $Λ = Γ$ , and [F6] would produce a nonzero point of $D \cap Γ$ , contradicting step 3.1. This refutes the mixed-convention claim.

5.1F6F7step 2.1step 1.2∎

The correct criterion is not violated: by step 2.1 the true covolume of $Γ$ is $2$ , so the threshold is $2^{2} \cdot 2 = 8$ . By [F7], $36 π / 25 < 144 / 25 < 8$ , so the hypothesis of [F6] fails and [F6] yields no lattice point in $D$ .

Remarks

The two normalizations differ by the factor $\sqrt{2}$ in each complex coordinate: the unscaled convention has $covol (σ (a)) = 2^{- r_{2}} \sqrt{∣ d_{K} ∣} N a$ , while the scaled convention has covolume $\sqrt{∣ d_{K} ∣} N a$ and $\sqrt{2}$ -weighted complex coordinates. The numerical coincidence that $36 π / 25$ lies between $4 = 2^{2} \cdot 1$ and $8 = 2^{2} \cdot 2$ is what makes the disc of radius $6 / 5$ a witness: it is large enough for the wrong threshold and too small for the right one.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
William A. Stein, Algebraic Number Theory: A Computational Approach (standard reference, not scraped)