Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Decomposition inertia in a quadratic field

Example

In a quadratic Galois extension of number fields, let G=C2. For any nonzero base prime the three possibilities are: split: (e,f,g)=(1,1,2), D=I=1, Frobenius identity; inert: (1,2,1), D=C2, I=1, Frobenius the nonidentity element; ramified: (2,1,1), D=I=C2, arithmetic Frobenius coset identity in D/I.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Galois prime decomposition efg: For a finite Galois extension L/K and nonzero prime p, every P above p has the same ramification index e and residue degree f. If there are g such primes, then efg=[L:K].

[F2]

Orders of decomposition and inertia groups: For finite Galois L/K and nonzero P∣p, writing e and f for its ramification index and residue degree, ∣D(P/p)∣=ef,∣I(P/p)∣=e,∣D(P/p)/I(P/p)∣=f. The prime P is unramified over p if and only if its inertia group is trivial.

[F3]

Frobenius order is residue degree: For finite Galois L/K and nonzero P∣p, the arithmetic Frobenius coset has order f(P/p) in D/I. If P is unramified, Frob⁡P has the same order in D.

Verification

1.1

Positive integers e,f,g with efg=2 have exactly the three displayed triples: the single factor 2 occurs in exactly one coordinate. These correspond respectively to split, inert, and ramified ideal factorizations.

F1
2.1

The formulas ∣D∣=ef and ∣I∣=e determine the subgroups, since C2 has only its identity subgroup and itself. For e=1 the Frobenius order is f, giving identity in the split case and the unique element of order two in the inert case. In the ramified case D/I has order f=1, so the residue coset is identity; there is no assertion of a unique lift.

F2F3step 1.1∎

Depends on

Used by

Dependency tree · two levels

10 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