Elementary identities, the norm-form layer, and parity reduction

This file proves the B7′-2 component of hilbertSymbol_dyadic. It supplies, in namespace GQ2.HilbertSymbol, the elementary Hilbert-symbol algebra the later engines (B7′-3/4/5) rely on:

1. Elementary identities — twelve definition-level theorems (the base definitions in GQ2/HilbertSymbol.lean are unchanged): the symmetry / self-negation / square-class lemmas for IsHilbertSolvable and hilbertSymbol, and the ε/ω residue homomorphism + table facts. Added: hilbertSymbol_mul_sq_right (square-class invariance on the right, via comm) and hilbertSymbol_isSquare_left (a square first slot ⇒ symbol 1).
2. The norm-form characterization isHilbertSolvable_iff (↔ IsSquare a ∨ b ∈ {s² − a t²}), the Brahmagupta identity (the norm set is multiplicatively closed), and the key hilbertSymbol_neg_mul_right : (a, -(a·b)) = (a, b) — the elementary identity that collapses the (1,1) parity family onto (0,1), so the leaves live at mod 8 (no mod-16 blowup).
3. Parity reduction symbol_zpow_reduce (2^α = 2^(α%2)·(2^(α/2))²) and the residue-dispatch helper toZModPow_unit_mem (u mod 8 ∈ {1,3,5,7}), which feed the final leaf rcases.

Placement. It imports GQ2.HilbertSymbol only (Mathlib-only, upstream of Foundations/Axioms.lean). The GQ2.DyadicSquares import (B7′-1's Hensel square criterion) is not needed here; the necessity and sufficiency engines import it directly.

Restored elementary identities (definition-level; from 2a238af^)

theorem GQ2.HilbertSymbol.isHilbertSolvable_comm (a b : ℚ_[2]) : IsHilbertSolvable a b ↔ IsHilbertSolvable b a

The defining locus is symmetric: swap the roles of X and Y.

theorem GQ2.HilbertSymbol.isHilbertSolvable_self_neg (a : ℚ_[2]) : IsHilbertSolvable a (-a)

a X² + (-a) Y² = Z² has the nontrivial solution (1, 1, 0).

theorem GQ2.HilbertSymbol.isHilbertSolvable_mul_sq_left (a b : ℚ_[2]) {c : ℚ_[2]} (hc : c ≠ 0) : IsHilbertSolvable (a * c ^ 2) b ↔ IsHilbertSolvable a b

Rescaling the first slot by a nonzero square does not change the locus (X ↦ c X).

theorem GQ2.HilbertSymbol.hilbertSymbol_comm (a b : ℚ_[2]ˣ) : hilbertSymbol a b = hilbertSymbol b a

Symmetry of the Hilbert symbol: (a, b)₂ = (b, a)₂.

theorem GQ2.HilbertSymbol.hilbertSymbol_self_neg (a : ℚ_[2]ˣ) : hilbertSymbol a (-a) = 1

(a, -a)₂ = 1.

theorem GQ2.HilbertSymbol.hilbertSymbol_mul_sq_left (a b c : ℚ_[2]ˣ) : hilbertSymbol (a * c ^ 2) b = hilbertSymbol a b

Square-class invariance in the first slot: (a c², b)₂ = (a, b)₂.

theorem GQ2.HilbertSymbol.hilbertSymbol_mul_sq_right (a b c : ℚ_[2]ˣ) : hilbertSymbol a (b * c ^ 2) = hilbertSymbol a b

Square-class invariance in the second slot: (a, b c²)₂ = (a, b)₂ (via comm).

theorem GQ2.HilbertSymbol.hilbertSymbol_isSquare_left {a : ℚ_[2]ˣ} (ha : IsSquare ↑a) (b : ℚ_[2]ˣ) : hilbertSymbol a b = 1

A square first slot gives symbol 1: witness (1, 0, c) with a = c².

theorem GQ2.HilbertSymbol.epsResidue_mul_of_isUnit {r s : ZMod 8} (hr : IsUnit r) (hs : IsUnit s) : epsResidue (r * s) = epsResidue r + epsResidue s

On the unit residues {1,3,5,7} ⊂ ℤ/8, ε is additive.

theorem GQ2.HilbertSymbol.omegaResidue_mul_of_isUnit {r s : ZMod 8} (hr : IsUnit r) (hs : IsUnit s) : omegaResidue (r * s) = omegaResidue r + omegaResidue s

On the unit residues {1,3,5,7} ⊂ ℤ/8, ω is additive.

theorem GQ2.HilbertSymbol.ε_mul (u v : ℤ_[2]ˣ) : ε (u * v) = ε u + ε v

ε is a homomorphism ℤ₂ˣ → 𝔽₂: ε(uv) = ε(u) + ε(v).

theorem GQ2.HilbertSymbol.ω_mul (u v : ℤ_[2]ˣ) : ω (u * v) = ω u + ω v

ω is a homomorphism ℤ₂ˣ → 𝔽₂: ω(uv) = ω(u) + ω(v).

theorem GQ2.HilbertSymbol.epsResidue_table : epsResidue 1 = 0 ∧ epsResidue 3 = 1 ∧ epsResidue 5 = 0 ∧ epsResidue 7 = 1

Residue table for ε: ε ≡ 0 on {1, 5} (≡ 1 mod 4), ε ≡ 1 on {3, 7} (≡ 3 mod 4).

theorem GQ2.HilbertSymbol.omegaResidue_table : omegaResidue 1 = 0 ∧ omegaResidue 3 = 1 ∧ omegaResidue 5 = 1 ∧ omegaResidue 7 = 0

Residue table for ω: ω ≡ 0 on {1, 7} (≡ ±1 mod 8), ω ≡ 1 on {3, 5} (≡ ±3 mod 8).

The norm-form characterization, Brahmagupta, and the (1,1)-family reduction

hilbertSymbol is +1 exactly when the ternary form is solvable; solving for b when y ≠ 0 (and for a when y = 0) turns this into membership of b in the set of norms {s² − a t²} from ℚ₂(√a) (or a being a square). The norm set is multiplicatively closed (Brahmagupta), contains -a (= 0² − a·1²), and is closed under division by squares — the three facts that make (a, -(a·b)) = (a, b).

theorem GQ2.HilbertSymbol.isHilbertSolvable_iff (a b : ℚ_[2]) : IsHilbertSolvable a b ↔ IsSquare a ∨ ∃ (s : ℚ_[2]) (t : ℚ_[2]), b = s ^ 2 - a * t ^ 2

Norm-form characterization: the form a X² + b Y² = Z² has a nontrivial ℚ₂-zero iff a is a square or b is a norm s² − a t² from ℚ₂(√a).

theorem GQ2.HilbertSymbol.brahmagupta (a s t s' t' : ℚ_[2]) : (s ^ 2 - a * t ^ 2) * (s' ^ 2 - a * t' ^ 2) = (s * s' + a * t * t') ^ 2 - a * (s * t' + t * s') ^ 2

Brahmagupta: the norm set {s² − a t²} is closed under multiplication.

theorem GQ2.HilbertSymbol.hilbertSymbol_neg_mul_right (a b : ℚ_[2]ˣ) : hilbertSymbol a (-(a * b)) = hilbertSymbol a b

The (1,1)-family killer: (a, -(a·b))₂ = (a, b)₂. Both -(a·b) and b differ by the norm -a, and the norm set is multiplicatively closed and square-divisible — so b is a norm iff -(a·b) is. This collapses the (1,1) parity family onto (0,1), keeping all leaves at mod 8.

Parity reduction and residue dispatch

theorem GQ2.HilbertSymbol.symbol_zpow_reduce (α : ℤ) : unit2 ^ α = unit2 ^ (α % 2) * (unit2 ^ (α / 2)) ^ 2

Parity split of the 2-power slot: 2^α = 2^(α mod 2) · (2^(α / 2))², so the symbol only sees α mod 2 after square-class invariance.

theorem GQ2.HilbertSymbol.toZModPow_unit_mem (u : ℤ_[2]ˣ) : (PadicInt.toZModPow 3) ↑u = 1 ∨ (PadicInt.toZModPow 3) ↑u = 3 ∨ (PadicInt.toZModPow 3) ↑u = 5 ∨ (PadicInt.toZModPow 3) ↑u = 7

Residue dispatch: the mod-8 residue of a 2-adic unit is one of {1,3,5,7} — the four unit residues, over which the leaf rcases runs.

Coercion helpers for the leaf engines (shared by B7′-3 / B7′-4)

The axiom's arguments are the unit2/unitCoe wrappers; the leaf proofs (necessity via not_isHilbertSolvable_of_mod, sufficiency via explicit witnesses) work with raw ℤ_[2] → ℚ_[2] coercions. These two rfl-lemmas bridge them. Owned by B7′-3 per docs/orchestration/b7prime-b34-coordination.md; B7′-4 imports (does not edit) this file.

theorem GQ2.HilbertSymbol.unit2_coe : ↑unit2 = 2

The ℚ₂-value of the unit 2 is 2.

theorem GQ2.HilbertSymbol.unitCoe_coe (u : ℤ_[2]ˣ) : ↑(unitCoe u) = ↑↑u

unitCoe u, valued in ℚ₂, is the double coercion ℤ₂ˣ → ℤ₂ → ℚ₂ of u.