The (139) half count for the local source G_ℚ₂ #
Discharge the two per-source hypotheses of half139_via_radData (RecursionSplice.lean) for the
local source Γ = G_ℚ₂ = AbsGalQ2, producing the (139) identity
2·zBC = |M_B|²·exactImageCount in exactly the shape of the RecursionInputs.half139 field
(consumed at the Prop. 8.9 assembly).
Two obligations, per boundary lift ρ of the C-target:
hlem86M— the source's Lemma 8.6 half-torsor count2·#{central M-lifts} = #(M-lifts). This islemma_8_6_local(✓, B6/B7) applied to the transported lower mapρ' = rhoPrime … ρ, withhedgethreaded from theNoDescentfield hypothesis andhρ'fromrhoPrime_surjective(below). ~Pure plumbing.hMcountM— the unrestrictedM-lift count#(M-lifts) = |M_B|². The genuine content:MLiftsis aZ¹_cont(G_ℚ₂, M_B)-torsor and#Z¹ = |M_B|²·#H²(G_ℚ₂, M_B)(card_Z1_eq), so the identity reduces to#H²(G_ℚ₂, M_B) = 1, i.e. the vanishing of theYC-coinvariants ofM_B.
Axioms (audit at close): ⊆ {B6, B7, B9} — B6/B7 via lemma_8_6_local and the local Euler
characteristic behind card_Z1_eq.
rhoPrime surjectivity (both sources) #
The transported lower map ρ' = piBCiso⁻¹ ∘ ρ is surjective. A boundary lift ρ wraps a
ContSurj (ρ.1.2 : Surjective ρ.1.1), and piBCiso.symm is a MulEquiv, so the composite is
onto B/M. Feeds lemma_8_6_local's surjectivity hypothesis.
The M-layer additive module (for the Z¹ count) #
↥D.M is elementary abelian (D.helem), so Additive ↥D.M is a finite 𝔽₂-space; conjugation
by any coset rep of Bg/D.M is well-defined (D abelian ⟹ rep-independent) and gives the
Bg/D.M-action, pulled back through a lower map ρ to a G_ℚ₂-action. These two helpers are the
D.M-analogues of RadicalEdgeLocal's D.T versions.
The (M∨)^C = 0 refutation (Lemma 7.1 / simple-head duality) #
No nonzero conjugation-invariant M-character ((M_B^∨)^{Y} = 0, the operational form of
Lemma 7.1 / Hom_C(M, 𝔽₂) = 0): any additive ψ : ↥M_B → 𝔽₂ invariant under Y-conjugation is
identically zero. A nonzero such ψ would pull back (through s : Blk.K ↠ M_B, s = piB|_K) to a
surjective character φ : Blk.K ↠ 𝔽₂ whose kernel maps to a Y-normal index-2 subgroup X with
Blk.frattiniK ≤ X ≤ Blk.K, contradicting SectionSeven.lemma_7_1_dual. This is the shared
kernel of both hMcountM_local (there via the fixedPts (ElemDual …) packaging) and the Prop. 8.9 assembly's
hpartial_local (the nondegeneracy residue).
The two hypotheses for G_ℚ₂ #
hlem86M for G_ℚ₂ — the source's Lemma 8.6 half-torsor count over every boundary lift,
for the radical datum En.radData l h, threading the NoDescent field hypothesis.
hMcountM for G_ℚ₂ — the unrestricted M-lift count #(M-lifts) = |M_B|².
The proof uses key : #Z¹ = |M_B|²·#fixedPts (card_Z1_eq),
hfix : #fixedPts = 1
(the lemma_7_1_dual bridge — a nonzero YC-invariant functional's kernel gives a Y-normal
index-2 X with Blk.frattiniK ≤ X ≤ Blk.K, refuted by lemma_7_1_dual), the explicit bijection
MLifts D ρ' ≃ Z¹_cont(G_ℚ₂, M_B) (f ↦ (γ ↦ f γ · f₀ γ⁻¹), a Z¹-torsor under the ρ'-conjugation
action), and nonemptiness Nonempty (MLifts D ρ') via the
extension-splitting argument: a continuous set-section s = Quotient.out ∘ ρ' gives a factor-set
2-cocycle c(γ,δ) = s γ · s δ · s(γδ)⁻¹ ∈ Z²(G_ℚ₂, M_B), which is a coboundary c = δ¹ψ because
#H²(G_ℚ₂,M_B) = 1 (card_H2_eq_fixedPts + hfix), and then f γ = (toMul (ψ γ))⁻¹ · s γ is a
continuous homomorphic lift of ρ'. This #MLifts count is also the shared deep input consumed
by the concurrent the Prop. 8.9 assembly (PhaseMuIndep.tcocycle_mu_indep's hML/κM). The route
(all steps over G_ℚ₂ = AbsGalQ2):
- Additive
M-moduleMBmod := Additive ↥(En.radData l h).M(= Additive ↥RF.MB), with theρ'-conjugationDistribMulAction AbsGalQ2 MBmodand the descendedDistribMulAction RF.YC MBmod(factoring throughρ',hcomp), continuity,2-torsion (RF.MB_elem). Pattern: copyRadicalEdgeLocal.lean:73–135(theD.Tversion) withD.T ⤳ D.M, usingD.hM(normality ⟹ conjugation stays inM) andD.hcomm(Mabelian ⟹ the action factors throughBg/M), which are the exactD.T-analogues already invoked there. - Torsor bridge
MLifts D ρ' ≃ Z¹_cont(AbsGalQ2, MBmod)—f ↦ (γ ↦ f γ · f₀ γ⁻¹)for a base liftf₀. Nonemptiness ofMLiftsis a theorem, not a hypothesis: the lift obstruction ofρ' : Γ → YB/M_BthroughYB ↠ YB/M_Blives inH²(AbsGalQ2, M_B), which is0by step 4 — soMLiftsis nonempty and the torsor bijection holds. card_Z1_eq(LocalLiftingDuality.lean:264, B7 Euler char):#Z¹(AbsGalQ2, MBmod) = |MBmod|² · #fixedPts RF.YC (ElemDual MBmod), feedinghρ = rhoPrimesurjectivity (rhoPrime_surjective),hcompfrom step 1,hA₂fromRF.MB_elem.#fixedPts RF.YC (ElemDual MBmod) = 1— i.e.H²(AbsGalQ2, M_B) = 0(card_H2_eq_fixedPts, B6), i.e.(M_B^∨)^{YC} = 0. The group-theoretic input isGQ2.SectionSeven.lemma_7_1_dual(GQ2/SectionSeven/Basic.lean, std-3) — "Khas noY-normal subgroup of index 2 aboveR" =(M^∨)^C = 0, via minimality ofK+ theV = P/Schief dichotomy. Only a bridge (a nonzeroYC-invariant functional's kernel ↦ an index-2Y-normalXwithBlk.frattiniK ≤ X ≤ Blk.K, refuted bylemma_7_1_dual).- Combine:
#MLifts = #Z¹ = |M_B|² · 1 = |M_B|².
The expected axioms are std-3 + B6 + B7 (B6 via card_H2_eq_fixedPts, B7 via
card_Z1_eq).
the Prop. 8.9 assembly result: the (139) half count for G_ℚ₂, in the exact shape of the
RecursionInputs.half139 field (consumed at the Prop. 8.9 assembly).
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Lemma 7.1 = ⟦lem-simplehead⟧
- Lemma 8.6 = ⟦lem-radicaledge⟧