The coordinates of a quartic L-value: a formalized survey of the classical facts.

For primes p > 5 with p ≡ 5 (mod 8), the quartic generalized Bernoulli number β = B₁,χ₄ is, after a choice of quartic character, a Gaussian integer k + it. This survey collects in one place the classical facts about these coordinates that are otherwise spread across papers from 1976 to 2026: why order four is the first level at which an odd non-real character occurs at prime conductor; what the trace and the relative class number already determine (k and |t|); how the normalization χ₄(2) = i fixes the sign of t and agrees with the quartic Jacobi-sum normalization and with Hudson’s quarter-range coordinates; and the fixed-base digit identity together with what it does not reach. Nothing in this survey is new. Every statement is attributed to its source. The elementary core (Propositions 1.1, 3.1, 3.2, 3.4 except one remark, 3.5 and 4.1, Definition 3.3, and the conjugation and reconstruction statements) is formally verified in Lean 4 with Mathlib; §6 lists what is verified and what is quoted.