Deep part and the §6 headline (Prop 6.18)

Proof-side layer for Lemma 6.17 (X₊ = deepPart is totally singular, #X₊² = #H¹) and Proposition 6.18 (the dyadic base determinant theorem, eq. (115)). The lemma_6_17_* / prop_6_18_* statements live in GQ2/SectionSix.lean; the heavy proofs are assembled here (this file imports SectionSix once the deep-part/Q0loc symbols are needed) and one-line-spliced, per the Lemma 6.14 proof (RepIndependence) pattern.

Structure of lemma_6_17_dim (#X₊² = #H¹, ramified, Ax B6+B7):

1. Euler-characteristic collapse #H¹ = #V — card_H1_eq_card_of_H0_H2_trivial below (this file): B7's #H¹ = #H⁰·#H²·2^{v₂(#V)} with #H⁰ = #H² = 1.
2. #H⁰ = 1 (V^{G_ℚ₂} = 0) and #H² = 1 ((V^∨)^{G_ℚ₂} = 0 via B6 perfect20) — for a nontrivial simple module on which inertia acts nontrivially. ⚠ NOTE: the frozen lemma_6_17_dim lacks hc : Surjective c; V^{im ρ} is C-stable (so simplicity ⟹ ⊥) only when im ρ ◁ C (e.g. c surjective). Likely a statement amendment (cf. lemma_6_8), flag for the architecture review.
3. #X₊ = 2^m — the Lagrangian half-count: X₊ is self-orthogonal under the B6 Tate pairing on H¹(V) ≅ H¹(V^∨) (deep units pair trivially by (94)), and maximal, so X₊ = X₊^⊥ and #X₊·#X₊^⊥ = #H¹ gives #X₊² = #H¹. This is the hard cohomological core (deep-unit Kummer image + Tate self-duality).

No sorry in this file.

File organisation. The proofs are spread over four sub-modules re-exported here:

• GQ2.DeepPart.QuadraticFp2 — the Gauss-sum-over-a-Lagrangian 𝔽₂ combinatorics.
• GQ2.DeepPart.MuTwoPolarDual — Euler collapse, the μ₂ bricks, and polar self-duality.
• GQ2.DeepPart.Q0locLayer — the Q⁰_loc quadratic structure (eq. (93)) and the deep half X₊.
• GQ2.DeepPart.HermitianCount — the Hermitian-line count (Prop 6.18, unramified).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (115) = ⟦eq-localzeros⟧
• eq. (93) = ⟦eq-squareclassgraded⟧
• Lemma 6.17 = ⟦lem-shapirodet⟧
• Lemma 6.4 = ⟦lem-detnormalizationindependence⟧
• Lemma 6.7 = ⟦lem-unitaryline⟧
• Prop 6.18 = ⟦prop-localzero⟧