The dispatch pyramid and the capstone hilbertSymbol_dyadic'

This is the assembly of the necessity and sufficiency engines into Serre's dyadic Hilbert-symbol formula, with a statement matching the public theorem in Foundations/Axioms.lean.

The pyramid.

1. Parity — symbol_zpow_reduce splits 2^α = 2^{α%2}·(2^{α/2})² in each slot; square-class invariance (hilbertSymbol_mul_sq_left/right) kills the squares, and (α : 𝔽₂) = (α%2 : 𝔽₂) does the same on the formula side. Four parity families remain.
2. (0,0), (0,1) — dyadic_uu / dyadic_u2v: rcases over the 4×4 unit residues (toZModPow_unit_mem), each case closed by a B7′-3 −1-leaf, a B7′-4 +1-witness, or the u ≡ 1 freebie, with the formula side evaluated by decide at the pinned residues.
3. (1,0) — hilbertSymbol_comm + dyadic_u2v with the slots swapped.
4. (1,1) — the design move: (2u, 2v) = (2u, −(2u·2v)) = (2u, −uv·2²) = (2u, −uv) (hilbertSymbol_neg_mul_right + square invariance), landing in dyadic_u2v at (−uv, u); the ε/ω bookkeeping (ε(−uv) = 1+ε(u)+ε(v), ω(−uv) = ω(u)+ω(v), ε² = ε) is a 16-case decide in 𝔽₂.

Foundations/Axioms.lean exposes the capstone hilbertSymbol_dyadic' under the public theorem name hilbertSymbol_dyadic.

The two residue-dispatch families

theorem GQ2.HilbertSymbol.dyadic_uu (u v : ℤ_[2]ˣ) : hilbertSymbol (unitCoe u) (unitCoe v) = signOf (ε u * ε v)

The (0,0) family: unit·unit symbols follow Serre's formula (u, v)₂ = (−1)^{ε(u)ε(v)}. Dispatch over the sixteen residue pairs: ≡ 1 slots are freebies, {3,5},{5,5},{5,7} (and swaps) are B7′-4 witnesses, {3,3},{3,7},{7,7} (and the swap) are B7′-3 decide-leaves.

theorem GQ2.HilbertSymbol.dyadic_u2v (u v : ℤ_[2]ˣ) : hilbertSymbol (unitCoe u) (unit2 * unitCoe v) = signOf (ε u * ε v + ω u)

The (0,1) family: (u, 2v)₂ = (−1)^{ε(u)ε(v) + ω(u)}. Dispatch over the sixteen residue pairs: u ≡ 1 is free, (3,3),(3,7),(7,1),(7,5) are B7′-4 witnesses, the remaining eight are B7′-3 decide-leaves.

The capstone

theorem GQ2.HilbertSymbol.hilbertSymbol_dyadic' (α β : ℤ) (u v : ℤ_[2]ˣ) : hilbertSymbol (unit2 ^ α * unitCoe u) (unit2 ^ β * unitCoe v) = signOf (ε u * ε v + ↑α * ω v + ↑β * ω u)

Serre's dyadic Hilbert-symbol formula (A Course in Arithmetic, Ch. III §1.2, Theorem 1, p = 2; ε, ω the residue characters of Ch. II §3.3): writing a = 2^α u, b = 2^β v with u, v ∈ ℤ₂ˣ, (a, b)₂ = (−1)^{ε(u)ε(v) + α ω(v) + β ω(u)}.

The public statement in Foundations/Axioms.lean is hilbertSymbol_dyadic := hilbertSymbol_dyadic'. This is proved from the definition of hilbertSymbol by solvability of a X² + b Y² = Z² — 2-adic Hensel + finite decides, std-3.