The local (83)-evaluation — the VCocycle ↔ H¹ transport and the pinned Gauss value #
Layer (II) of the source-Gauss residue (design docs/orchestration/p16d6e4a-evaluation-design.md §1): the
descended base-determinant form Q̄⁰ on Z¹_{Γ,ρ}(V) ⧸ B¹ is, over Γ = G_ℚ₂, carried by an
explicit bijection onto (H¹(G_ℚ₂, V), Q⁰_loc) — whose Gauss sum §6.2/§6.3 already computed
(prop_6_18_{unramified,ramified}). Pieces:
- (A) the
Z¹-bridgetoZ1/ofZ1(the shared e3 bridge as reusable declarations): aVCocycleIS a continuous 1-cocycle once theΓ-action onVfactors throughρ'(hcomp); continuity crosses the topology-freeVthrough theiV ∘ ofAddembedding. - (B) the quotient bijection
h1OfVQuot : (Z¹ ⧸ B¹) → H¹(Γ, V)—vCob-cosets map todZero-cosets; bijective. - (C′) the form-compatibility
QZeroBar_eq_Q0loc:Q̄⁰ = Q⁰_loc ∘ Φ, by the provediotaB_eq_iotaFbridge (IotaBridge) + theB¹-shift invariance of the graph pullback (GaussZReduction.graphPullback_shift_mem_B2) absorbing theQuotient.outrepresentative. - (D)/(E) the pinned value
sum_sign_Q0loc_{unramified,ramified}:∑ᶠ sign(Q⁰_loc) = ∓2^mfromprop_6_18+gaussSum_eq+card_H1_eq_card_of_simple.
The e7 assembly composes these with GaussZReduction.gaussZ_reduction to discharge the local
GaussZResidue (hGaussZF). Axioms: (A)/(B)/(C′) are std-3; (D)/(E) carry prop_6_18's
budget (B6 via the D parameter, B7).
(A) the Z¹-bridge, as reusable declarations (the shared e3 bridge) #
The VCocycle → Z¹ bridge (the Prop. 8.9 assembly (A), the e3 bridge as a declaration): under an
action identification γ • v = ρ'(γ) • v, a crossed V-cocycle is a continuous 1-cocycle.
Continuity crosses the topology-free V through the injective iV ∘ ofAdd into the discrete
Bg ⧸ T (IsLocallyConstant.desc).
Equations
- GQ2.SectionEight.AffineTLift.toZ1 hcomp c = ⟨c.c, ⋯⟩
Instances For
The inverse direction: a continuous 1-cocycle is a crossed V-cocycle.
Equations
- GQ2.SectionEight.AffineTLift.ofZ1 hcomp z = { c := ↑z, cont := ⋯, crossed := ⋯ }
Instances For
(B) the quotient bijection (Z¹ ⧸ B¹) → H¹ #
The H¹-class equality criterion, in H1mk vocabulary (H1 is a semireducible def, so
the quotient coercion does not elaborate against it; this is the show-unfolded form).
The quotient map Φ : Z¹_{Γ,ρ}(V) ⧸ B¹ → H¹(Γ, V) (the Prop. 8.9 assembly (B)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
(C′) the form compatibility over G_ℚ₂ #
The form compatibility (the Prop. 8.9 assembly (C′)): under the transport Φ = h1OfVQuot, the
descended base determinant form Q̄⁰ is Q⁰_loc — the abstract iotaB-obstruction and the
Tate-invariant obstruction agree (iotaB_eq_iotaF), and the Quotient.out representative on
the H¹ side differs from the transported cocycle by a B¹-shift, which the graph pullback
absorbs mod B² (graphPullback_shift_mem_B2).
(D)/(E) the pinned Gauss value on (H¹(G_ℚ₂, V), Q⁰_loc) #
The C-action moves some vector (else V ≅ 𝔽₂, contradicting #V = 2^{2m}, m ≥ 1) —
the mover block of prop_6_18_unramified, extracted.
The signed-sum extraction shared by both cases: with zeroCount(Q⁰_loc) and
#H¹ = 2^{2m} known, ∑ᶠ sign(Q⁰_loc) = 2·zeroCount − 2^{2m}.
The pinned local Gauss value, unramified (the Prop. 8.9 assembly (D)/(E)):
∑ᶠ sign(Q⁰_loc) = −2^m — prop_6_18_unramified's zero count through gaussSum_eq.
The pinned local Gauss value, ramified (the Prop. 8.9 assembly (D)/(E)):
∑ᶠ sign(Q⁰_loc) = +2^m — prop_6_18_ramified's zero count through gaussSum_eq.