The necessity engine and the 11 −1-leaves #
This file proves the B7′-3 component of hilbertSymbol_dyadic, coordinated with the
parallel B7′-4 development described in docs/orchestration/b7prime-b34-coordination.md. It provides the machinery that proves a
dyadic Hilbert symbol is −1 — i.e. a ternary form has no nontrivial ℚ₂-zero — from a finite
mod-2^k obstruction, and applies it to the eleven −1 residue leaves.
exists_int_triple— clear denominators: a nontrivialℚ₂-solution scales (via a common denominator fromIsFractionRing ℤ_[2] ℚ_[2]) to a nontrivialℤ_[2]-solution.exists_primitive_triple— the 2-adic descent: if all three coordinates are non-units they are all divisible by2; halve and recurse on theℕ-measureΣ valuationᵢ(valuation 0 = 0, so zeros are handled uniformly), which strictly decreases. Terminates byNat.strong_induction_on.not_isHilbertSolvable_of_mod— push a primitiveℤ_[2]-solution through the ring homPadicInt.toZModPow k(IsUnit.mappreserves the odd coordinate), contradicting adecide-checked non-solvability overZMod (2^k).- the 11
−1-leaves, each adecideatk = 3(ZMod 8, 512 triples, plaindecide).
Necessity never touches the Hensel square criterion, so this file imports GQ2.HilbertSymbolDyadic
only (the shared coercion helpers unit2_coe / unitCoe_coe live there).
Integralization: a ℚ₂-solution scales into ℤ_[2] #
Integralization. A nontrivial ℚ₂-zero of A X² + B Y² − Z² (with A, B ∈ ℤ_[2]) scales,
by a common denominator, to a nontrivial ℤ_[2]-zero.
The 2-adic descent to a primitive solution #
Primitivity descent. A nontrivial ℤ_[2]-solution has a primitive one — with some
coordinate a unit. If none is a unit, all are divisible by 2; halving strictly drops the measure
Σ valuation.
The mod-2^k obstruction #
Non-solvability from a finite obstruction. If A X² + B Y² = Z² has no primitive solution
over ZMod (2^k) (some coordinate a unit), it has no nontrivial ℚ₂-solution: integralize,
primitivize, and push through the ring hom PadicInt.toZModPow k (which sends the unit
coordinate to a unit by IsUnit.map).
The two −1-leaf families #
Both reduce hilbertSymbol … = -1 to a decide-checked non-solvability over ZMod 8, threading
the axiom's unitCoe/unit2 wrappers through unitCoe_coe/unit2_coe. The decide
obligation is passed as hdec so each concrete leaf below supplies it by by decide
(512 triples, no native_decide).
Unit·unit −1-leaf: (u, v)₂ = -1 at residues (ru, rv) for which ru x² + rv y² = z² has no
primitive ZMod 8 solution.
(u, 2v) −1-leaf: (u, 2v)₂ = -1 at residues (ru, rv) for which ru x² + 2 rv y² = z² has
no primitive ZMod 8 solution.
The 11 −1-leaves (plan §1 inventory; each decide at ZMod 8) #
Unit·unit: {3,3}, {3,7}, {7,7}. (u, 2v): u₀=3, v₀∈{1,5}; u₀=5, v₀∈{1,3,5,7};
u₀=7, v₀∈{3,7}. The by decide on each certifies it is a genuine mod-8 −1 leaf.