The involution spine — discharging the c2a package

ShapiroDeepness.hvanish_involution_of_deepClass (the proved assembly) is parameterized by an abstract "Kummer presentation package" hc2a and by hunram. This file discharges hc2a from the concrete QuadraticAdjoin.exists_kummer_presentation (the Lemma 6.17 vanishing proof), leaving a version hvanish_involution_of_deepClass' that no longer carries the abstract package — only the tower (k ≤ L, hindex) and the unramifiedness hunram (the latter supplied by the Lemma 6.17 vanishing proof's UnramifiedBridge.hunram_involution at the call site / f2d).

The one real brick is the fixing-index-2 → degree-2 bridge finrank_extendScalars_eq_two: [G_k : G_L] = 2 ⟹ [L : k] = 2. Route (base-↥k framing): transport the index along IntermediateField.fixingSubgroupEquiv k, then run InfiniteGalois.normalAutEquivQuotient (Gal(ℚ̄₂/k) ⧸ G_L ≃ Gal(L/k), using index-2 ⟹ normal) composed with IsGalois.card_aut_eq_finrank. Everything else is the deep-unit norm bridge (LocalKummer.norm_sub_one_lt_of_isDeepUnit) and A ∈ L from IsDeepUnit's fixedness (InfiniteGalois.fixedField_fixingSubgroup).

The fixing-index-2 → degree-2 bridge

theorem GQ2.ShapiroDeepness.finiteDimensional_extendScalars (k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥L] (hkL : k ≤ L) : FiniteDimensional ℚ_[2] ↥(IntermediateField.extendScalars hkL)

extendScalars hkL (i.e. L viewed over ↥k) is ℚ_[2]-finite when L is: the identity on the shared carrier is a ℚ_[2]-linear equivalence ↥L ≃ₗ ↥(extendScalars hkL).

theorem GQ2.ShapiroDeepness.index_extendScalars_fixingSubgroup (k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (hkL : k ≤ L) : (IntermediateField.extendScalars hkL).fixingSubgroup.index = (L.fixingSubgroup.subgroupOf k.fixingSubgroup).index

Index transport: the fixing subgroup of extendScalars hkL inside Gal(ℚ̄₂/↥k) is the image of L.fixingSubgroup.subgroupOf k.fixingSubgroup under fixingSubgroupEquiv k, so the two have equal index.

theorem GQ2.ShapiroDeepness.finrank_extendScalars_eq_two (k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥L] (hkL : k ≤ L) (hindex : (L.fixingSubgroup.subgroupOf k.fixingSubgroup).index = 2) : Module.finrank ↥k ↥(IntermediateField.extendScalars hkL) = 2

The bridge (the Lemma 6.17 vanishing proof core): a fixing-index-2 subextension has relative degree 2.

Discharging the c2a package

theorem GQ2.ShapiroDeepness.kummer_presentation_of_index_two (k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] [FiniteDimensional ℚ_[2] ↥L] (hkL : k ≤ L) (hindex : (L.fixingSubgroup.subgroupOf k.fixingSubgroup).index = 2) (A : AlgebraicClosure ℚ_[2]) (hdeep : SectionSix.IsDeepUnit L.fixingSubgroup A) : ∃ (d : (↥k)ˣ) (δ : AlgebraicClosure ℚ_[2]) (u : (↥k)ˣ) (v : ↥k), δ ^ 2 = ↑↑d ∧ δ ∈ L ∧ L.fixingSubgroup.subgroupOf k.fixingSubgroup = (MulAction.stabilizer (Kummer.GaloisGroup ℚ_[2]) δ).subgroupOf k.fixingSubgroup ∧ A = ↑↑u + ↑v * δ

hc2a discharged (the Lemma 6.17 vanishing proof): the abstract Kummer presentation package of hvanish_involution_of_deepClass, proved from QuadraticAdjoin.exists_kummer_presentation.

The c2b vanish lemma (hc2a discharged)