Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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.

{qQ:q0, q2<2}\{q \in \mathbb{Q} : q \ge 0,\ q^2 < 2\} is closed and bounded in Q\mathbb{Q} and is not compact

Statement refuted

Refuted claim: in every ordered field a closed bounded set is compact, so the completeness hypothesis of the Heine-Borel characterisation is unnecessary (FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness).

The witness is the ordered field Q\mathbb{Q} (The rationals as equivalence classes of pairs of integers, The rationals form a totally ordered field) together with

S  :=  {qQ:q0 and q2<2}.S \;:=\; \{\, q \in \mathbb{Q} : q \ge 0 \text{ and } q^2 < 2 \,\} .

The set SS is bounded, is closed in Q\mathbb{Q}, and is not compact in Q\mathbb{Q}, all with respect to the vocabulary of Open cover, subcover, compact subset of R\mathbb{R} (every open cover has a finite subcover), and sequentially compact subset transposed from R\mathbb{R} to Q\mathbb{Q} exactly as set out in FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness, where the refutation is carried out in full. This item records the witness and says what makes it work.

Facts & Assumptions

Given: The ordered field Q\mathbb{Q} and the set S:={qQ:q0 and q2<2}S := \{\, q \in \mathbb{Q} : q \ge 0 \text{ and } q^2 < 2 \,\}, with "open in Q\mathbb{Q}", "closed in Q\mathbb{Q}", "bounded" and "compact in Q\mathbb{Q}" as defined in FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness.

[A1]

The refuted claim: in every ordered field a closed bounded set is compact.

[L1]

SS is nonempty and bounded, has no greatest element, is closed in Q\mathbb{Q}, and the family {{yQ:y<r}:rS}\{\, \{\, y \in \mathbb{Q} : y < r \,\} : r \in S \,\} is a cover of SS by sets open in Q\mathbb{Q} with no finite subfamily covering SS (FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness).

[L3]

No rational number squares to 22 (FALSE: some rational number squares to 2).

[L4]

Squaring is strictly monotone on the nonnegatives of an ordered field (Squaring is monotone on the nonnegatives).

Counterexample

technique · direct
1.1

Q\mathbb{Q} is an ordered field by [L2], so it is a legitimate instance of the claim [A1].

A1L2
1.2

SS is bounded and closed in Q\mathbb{Q} by [L1]; the closedness rests on the fact that no rational squares to 22 ([L3]), which is what makes the complement of SS split into the rationals below 00 and those whose square exceeds 22, and on the monotonicity of squaring ([L4]), which is what makes each of those two pieces open in Q\mathbb{Q}.

L1L2L3L4
1.3

SS is not compact in Q\mathbb{Q}: the cover exhibited in [L1] consists of sets open in Q\mathbb{Q}, covers SS because SS has no greatest element, and admits no finite subfamily covering SS, since the largest index of such a subfamily is itself a member of SS that the subfamily leaves uncovered.

L1L2
2.1

So the ordered field Q\mathbb{Q} carries a bounded set that is closed in Q\mathbb{Q} and not compact in Q\mathbb{Q}, and the claim [A1] is refuted.

step 1.1step 1.2step 1.3A1L1

Remarks

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: 62 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