Documentation

GQ2.DetRamified

The ramified base determinant theorem, wired #

The two §6.3 Kummer cores lemma_6_17_dim / lemma_6_17_vanish are stated (frozen) upstream in GQ2/SectionSix.lean but proved downstream — the dimension clause by ResidueLift.lemma_6_17_dim_final (the deep-part proof) and the vanishing clause by VanishClose.lemma_6_17_vanish_final (the Lemma 6.17 vanishing proof).

This leaf places prop_6_18_ramified downstream of both _final proofs and cites them through the reduction DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish. This placement breaks the import cycle that would arise if the theorem lived with the shared definitions in SectionSix.

Amendment (the architecture review flag): lemma_6_17_vanish_final carries the reciprocity datum (R : LocalReciprocity, horient : TameUnitOrientation R B.tameF) — the c2c4 route to the involution hunram (odd tame inertia ⟹ the involution extension is unramified, in CFT vocabulary). So prop_6_18_ramified gains (R, horient) as hypotheses (the hc/hV2 precedent); consumers discharge them at B := boundaryMapsWitness via TameOrientationWitness.tameFHom_tameUnitOrientation (B10′) with R := localReciprocity (B5).

Axioms: std-3 + {B6, B7, B9, B11a} (B11b/B12/B13 have since been discharged as in-repo std-3 theorems/defs; the original budget was lemma_6_17_dim_final's B6/B7/B11a/B12/B13 + lemma_6_17_vanish_final's B9/B11a/B11b/B13, joined through card_Q0loc_zero_eq_of_dim_of_vanish, which adds only B6/B7 via D) — the full §6.3 deep-part budget, no new axiom, no sorryAx.

source
theorem GQ2.DetRamified.prop_6_18_ramified {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [DistribMulAction C V] (D : TateDuality 2) (R : LocalReciprocity) (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) (horient : TameUnitOrientation R B.tameF) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) :
Nat.card { x : ContCoh.H1 AbsGalQ2 V // SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) + 2 ^ (m - 1)

Proposition 6.18 (dyadic base determinant theorem), eq. (115), ramified case — wired downstream (the deep-part proof/f2d statement-move): the local base determinant form has the positive Gauss sign, #(Q⁰_loc)⁻¹(0) = 2^{2m−1} + 2^{m−1} (#V = 2^{2m}). With Prop 6.9 this is Corollary 6.19(iv): the two sources have equal base Gauss sums.

Proved from the two §6.3 Kummer cores now that both are proved downstream: ResidueLift.lemma_6_17_dim_final (#X₊² = #H¹) and VanishClose.lemma_6_17_vanish_final (Q⁰_loc|X₊ = 0), fed to the banked Lagrangian-Arf count card_Q0loc_zero_eq_of_dim_of_vanish. Amended (the architecture review flag) with (R, horient) — the reciprocity datum lemma_6_17_vanish_final requires; consumers discharge it at the boundary-maps witness.

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