The sufficiency engine and the +1 witness leaves

This file proves the B7′-4 component of hilbertSymbol_dyadic, coordinated through docs/orchestration/b7prime-b34-coordination.md. It supplies, in namespace GQ2.HilbertSymbol, the +1 side of the leaf dispatch: the Hensel value glue plus the seven explicit-witness leaves and the u ≡ 1 (mod 8) freebie family.

• hilbertSymbol_eq_one_of_value — if a·x² + b·y² equals a 2-adic integer ≡ 1 (mod 8) (hence a square t² by DyadicSquares.isSquare_of_toZModPow_eq_one, t ≠ 0), then (x, y, t) is a nontrivial zero, so (a, b)₂ = 1.
• seven witness leaves (hilbertSymbol_uu_* for unit·unit {3,5},{5,5},{5,7}, hilbertSymbol_u2v_* for (u, 2v) {3,3},{3,7},{7,1},{7,5}), each refine-ing the glue at the witness/value from plan §1;
• hilbertSymbol_left_one — u ≡ 1 (mod 8) ⟹ (u, b)₂ = 1 for any b, via hilbertSymbol_isSquare_left (a unit ≡ 1 (mod 8) is a square).

Placement (per b7prime-b34-coordination.md): own new file, imports GQ2.HilbertSymbolDyadic (shared coercion helpers unit2_coe/unitCoe_coe, and hilbertSymbol_isSquare_left) + GQ2.DyadicSquares (Hensel square criterion); namespace GQ2.HilbertSymbol; strictly upstream of Foundations/Axioms.lean. The −1 necessity leaves are B7′-3 (HilbertSymbolNecessity.lean); the dispatch capstone is B7′-5 (HilbertSymbolDyadicClose.lean, downstream of both).

Residue → leaf map (for B7′-5 dispatch). Unit·unit (u,v) is +1 iff not both ∈ {3,7}: u ≡ 1 or v ≡ 1 → hilbertSymbol_left_one (the latter after hilbertSymbol_comm); else the three hilbertSymbol_uu_* (with comm covering the swaps). For (u, 2v): u ≡ 1 → hilbertSymbol_left_one; the +1 non-1 cases are exactly hilbertSymbol_u2v_{33,37,71,75}.

theorem GQ2.HilbertSymbol.hilbertSymbol_eq_one_of_value {a b : ℚ_[2]ˣ} (x y w : ℤ_[2]) (hw : (PadicInt.toZModPow 3) w = 1) (heq : ↑a * ↑x ^ 2 + ↑b * ↑y ^ 2 = ↑w) : hilbertSymbol a b = 1

The Hensel value glue. If a·x² + b·y² equals a 2-adic integer w ≡ 1 (mod 8) — hence a square t² with t ≠ 0 — then (x, y, t) is a nontrivial zero of a X² + b Y² − Z², so the Hilbert symbol is +1.

The seven +1 witness leaves (plan §1)

theorem GQ2.HilbertSymbol.hilbertSymbol_uu_35 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 3) (hv : (PadicInt.toZModPow 3) ↑v = 5) : hilbertSymbol (unitCoe u) (unitCoe v) = 1

Unit·unit leaf {3,5}: witness (x,y) = (2,1), value 4u + v ≡ 1 (mod 8).

theorem GQ2.HilbertSymbol.hilbertSymbol_uu_55 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 5) (hv : (PadicInt.toZModPow 3) ↑v = 5) : hilbertSymbol (unitCoe u) (unitCoe v) = 1

Unit·unit leaf {5,5}: witness (1,2), value u + 4v ≡ 1 (mod 8).

theorem GQ2.HilbertSymbol.hilbertSymbol_uu_57 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 5) (hv : (PadicInt.toZModPow 3) ↑v = 7) : hilbertSymbol (unitCoe u) (unitCoe v) = 1

Unit·unit leaf {5,7}: witness (1,2), value u + 4v ≡ 1 (mod 8).

theorem GQ2.HilbertSymbol.hilbertSymbol_u2v_33 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 3) (hv : (PadicInt.toZModPow 3) ↑v = 3) : hilbertSymbol (unitCoe u) (unit2 * unitCoe v) = 1

(u, 2v) leaf {3,3}: witness (1,1), value u + 2v ≡ 1 (mod 8).

theorem GQ2.HilbertSymbol.hilbertSymbol_u2v_37 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 3) (hv : (PadicInt.toZModPow 3) ↑v = 7) : hilbertSymbol (unitCoe u) (unit2 * unitCoe v) = 1

(u, 2v) leaf {3,7}: witness (1,1), value u + 2v ≡ 1 (mod 8).

theorem GQ2.HilbertSymbol.hilbertSymbol_u2v_71 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 7) (hv : (PadicInt.toZModPow 3) ↑v = 1) : hilbertSymbol (unitCoe u) (unit2 * unitCoe v) = 1

(u, 2v) leaf {7,1}: witness (1,1), value u + 2v ≡ 1 (mod 8).

theorem GQ2.HilbertSymbol.hilbertSymbol_u2v_75 {u v : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 7) (hv : (PadicInt.toZModPow 3) ↑v = 5) : hilbertSymbol (unitCoe u) (unit2 * unitCoe v) = 1

(u, 2v) leaf {7,5}: witness (1,1), value u + 2v ≡ 1 (mod 8).

The u ≡ 1 (mod 8) freebie family

theorem GQ2.HilbertSymbol.hilbertSymbol_left_one {u : ℤ_[2]ˣ} (hu : (PadicInt.toZModPow 3) ↑u = 1) (b : ℚ_[2]ˣ) : hilbertSymbol (unitCoe u) b = 1

Freebie: a first slot u ≡ 1 (mod 8) is a square, so (u, b)₂ = 1 for every b. Covers every leaf with u ≡ 1 in both families (and, after hilbertSymbol_comm, every v ≡ 1).