The corestriction-of-coboundary bridge for Lemma 6.17's vanishing clause #
lemma_6_17_vanish (Q⁰_loc|X₊ = 0) reduces — after the H_V-split embedding of Lemma 6.14 and
the orbit decomposition of Lemma 6.15 — to a sum of per-orbit contributions, each of the form
H²ofFun G_ℚ₂ (cor2Fun U inner) where inner is a scalar cup (free/square orbits) or an Evens
norm (involution orbits). For a deep class every such inner is a coboundary: free/square by
the (94) orthogonality (LocalKummer.cup_deepClasses / HilbertLedger.cup_deep_self), involution
by Lemma 6.16.
This file supplies the reusable brick that turns "inner is a coboundary" into "its corestriction
vanishes in H²" — the cochain heart the Lemma 6.17 vanishing proof scoping doc flagged as "the continuity → B2 step
still needed". Corestriction.cor2Fun_dOne gives cor2Fun U (δ¹c) = δ¹(cor1Fun U c), the trivial
𝔽₂-action (absGal_smul_zmodTwo, rfl) identifies it with the genuine coboundary
dOne (cor1Fun U c), and cor1Fun U c is continuous (ShapiroLedger.continuous_lTrans'), so the
corestriction lands in B² and its class is 0. All std-3, no axiom.
Corestriction of a coboundary vanishes in H² (the Lemma 6.17 vanishing proof, the per-orbit cochain heart):
if inner = δ¹c is the trivial-action coboundary of a continuous 1-cochain c : ↥U → 𝔽₂, then
the degree-2 corestriction cor2Fun U inner is 0 in H²(G_ℚ₂, 𝔽₂).
cor2Fun_dOne rewrites cor2Fun U (δ¹c) = δ¹(cor1Fun U c), which is the coboundary of the
continuous cochain cor1Fun U c (continuous_lTrans'), so it lies in B² and H²ofFun sends it
to 0.
Class-level form (the Lemma-6.15 orbit consumer): if a 2-cocycle inner on the subgroup
↥U has trivial class in H²(↥U, 𝔽₂), its degree-2 corestriction vanishes in H²(G_ℚ₂, 𝔽₂).
This is the shape the per-orbit outputs feed: the free/square-orbit cup and the involution-orbit
Evens norm each vanish in the subgroup's H² (by the (94) orthogonality cup_deepClasses resp.
Lemma 6.16 for a deep class), and corestriction carries that vanishing up to G_ℚ₂. Extracts the
explicit continuous coboundary (H² = 0 + smul_zmodTwo trivial action) and applies
H2ofFun_cor2Fun_coboundary_eq_zero.
The Lemma-6.17 vanishing assembly (the verified reduction, parametric over gap 2) #
The Lemma-6.17 vanishing assembly (the Lemma 6.17 vanishing proof, the verified reduction): if Q⁰_loc at a class
x decomposes as a finite sum of per-orbit corestriction contributions — the monomial expansion
hexp, i.e. Lemma 6.14 through the regular embedding + Lemma 6.15's orbit classes (the
combinatorial "gap 2" of docs/orchestration/p15f2-scoping.md) — and each orbit's inner 2-cocycle vanishes in
the subgroup's H² (hvanish: free/square by the (94) orthogonality cup_deepClasses, involution
by Lemma 6.16, for a deep class), then Q⁰_loc x = 0.
Isolates the remaining combinatorial input hexp from the arithmetic vanishing, which discharges
through the corestriction bridge H2ofFun_cor2Fun_eq_zero_of_H2_eq_zero. Mirrors the f8 pattern:
verified reduction separated from the hard analytic input.
Additivity backbone: reducing hexp to the raw cochain-level orbit decomposition #
hexp (the monomial expansion) is Q⁰_loc x = Σ_orbit iotaF(H2ofFun(cor2Fun …)). Since
Q⁰_loc x = iotaF(H2ofFun(graphPullback dat ρ (out x))) by definition and iotaF is additive,
hexp follows once (a) graphPullback dat ρ (out x) decomposes as a sum of per-orbit
2-cocycles Σ_o φ_o (the genuine combinatorial core — "gap 2", the paper's q∘p monomial
expansion via Lemma 6.14 + the datum decomposition datW = Σ orbitDatum) and (b) each φ_o is
cohomologous to the corresponding cor2Fun (U_o) (inner_o) (Lemma 6.15, banked). The additivity
of iotaF ∘ H2ofFun on cocycles is the reusable plumbing, isolated here.
H²ofFun is additive on a finite sum of continuous 2-cocycles.
The hexp reducer and the full f2 reducer #
The hexp producer (the Lemma 6.17 vanishing proof): the monomial expansion in cochain-level form. If the
graph pullback of the base class decomposes as a finite sum of per-orbit 2-cocycles φ_o
(hdecomp — the combinatorial "gap 2") and each φ_o is cohomologous to cor2Fun (U_o) (inner_o)
(hcoh — Lemma 6.15, banked), then Q⁰_loc x is the orbit sum hexp consumed by
Q0loc_vanish_of_orbit_sum. Pure additivity plumbing (H2ofFun_sum_of_mem_Z2 + iotaF's
map_sum); isolates the raw decomposition hdecomp as the sole remaining combinatorial input.
The full the Lemma 6.17 vanishing proof reducer (lemma_6_17_vanish modulo the monomial expansion): given the raw
per-orbit cochain decomposition hdecomp, the Lemma-6.15 cohomologies hcoh, and the deep-class
per-orbit vanishing hvanish (free/square = cup_deepClasses, involution = lemma_6_16),
Q⁰_loc x = 0. Composes Q0loc_eq_orbit_sum_of_decomp (→ hexp) with
Q0loc_vanish_of_orbit_sum. The sole remaining input for lemma_6_17_vanish is hdecomp —
the q∘p monomial expansion over the regular module (Lemma 6.14 + the datum decomposition).
§6.2 datum-additivity assembly: from the datum-level orbit decomposition to hdecomp #
The paper assembles the multi-orbit contribution as additivity of graphPullback in the datum
(the Lemma-6.15 deviation note, SectionSix.lean:646): once the invariant datum on the regular
module decomposes as a pointwise (block) sum of the per-orbit datums datW = Σ_o datum_o (each an
orbit datum of §6.2 extended by zero to the regular module), its graph pullback is the sum of the
per-orbit pullbacks — each of which is a banked Lemma-6.15 corestriction. This section supplies
that additivity brick and the resulting datum-level reducer, landing the sole remaining input
of lemma_6_17_vanish (through the Lemma-6.14 transport) on the datum identity
datW = Σ_o datf_o and the banked 6.15 cohomologies.
Pointwise (block) sum of factor-set datums (§6.2 assembly): the datum whose factor set and
central corrections are the coordinatewise finite sums. This is the datum-level form of the
paper's multi-orbit decomposition datW = Σ_o datum_o (each datum_o an orbit datum extended by
zero to the regular module 𝔽₂[H_V]^N).
Equations
- GQ2.OrbitVanish.sumDatum s datf = { f := fun (v w : V) => ∑ o ∈ s, (datf o).f v w, m := fun (c : C) (v : V) => ∑ o ∈ s, (datf o).m c v }
Instances For
Additivity of graphPullback in the datum: the graph pullback of a pointwise datum sum is
the sum of the graph pullbacks. This is the paper's "multi-orbit assembly = additivity of
graphPullback in the datum" (Lemma-6.15 deviation note), which turns a datum-level orbit
decomposition datW = Σ_o datf_o into the cochain-level hdecomp consumed by
Q0loc_vanish_of_decomp.
The datum-level the Lemma 6.17 vanishing proof reducer (lemma_6_17_vanish modulo the §6.2 datum decomposition):
if the (regular-module) datum decomposes as a pointwise sum of per-orbit equivariant factor sets
dat = Σ_o datf_o (hdat_eq — the datum-level "gap 2", sumDatum), each per-orbit pullback is
cohomologous to its Lemma-6.15 corestriction (hcoh — free/square = eq. (103)/(104), involution =
eq. (105), all banked in ShapiroLedger), and each corestriction's inner cocycle vanishes in the
subgroup's H² (hvanish — deep-class (94)/6.16), then Q⁰_loc x = 0.
Composes the datum-additivity brick graphPullback_sumDatum (turning hdat_eq into the cochain
decomposition hdecomp) with the full reducer Q0loc_vanish_of_decomp; per-orbit Z²-membership
is discharged from the equivariant-factor-set hypotheses via graphPullback_mem_Z2. Applied at the
regular module V := 𝔽₂[H_V]^N after the Lemma-6.14 transport
Q⁰_loc dat ρ x = Q⁰_loc datW ρ ι_*x, the sole remaining input for lemma_6_17_vanish is
hdat_eq — the datum-level orbit decomposition of §6.2.
Q⁰_loc datum-independence, reduced to its Lemma-6.1/6.4 core #
The orbit route needs the base connecting map computed with the orbit-sum datum on the regular
module, but lemma_6_17_vanish is stated for an arbitrary equivariant factor set dat for q.
Bridging the two requires Q⁰_loc datum-independence: any two equivariant factor sets for the
same form give the same Q⁰_loc (Lemma 6.1 — "different equivariant lifts give cohomologous
cocycles" — feeding Lemma 6.4). Only a special isometry case is banked
(UnramifiedModel.graphPullback_comap_smul_sub_mem_B2, comap along a q-isometry g₀ ∈ C).
This section reduces the general statement to a single crisp cohomological input, exactly as the
rest of f2 was reduced: the difference datum diffDatum dat1 dat2 (pointwise 𝔽₂-sum, = the
char-2 difference) is an equivariant factor set for the zero form
(isEquivariantFactorSet_diffDatum), and graphPullback is additive along it
(graphPullback_diffDatum), so datum-independence follows once the graph pullback of a
zero-form factor set is a coboundary (hcore — DI-core, the isolated Lemma-6.1/6.4 heart:
the class [κ⁰] of a zero-form factor set on V ⋊ C is trivial, so its graph pullback lands in
B²). DI-core is not discharged here: the coboundary Λ(g) = Δφ(b g) needs a quadratic
refinement Δφ of the difference (which exists — the two data share the polar, so Δf is a
symmetric coboundary over 𝔽₂)
corrected against the C-equivariance defect Δm (an H¹(C, V*) obstruction — the genuine Lemma
6.1/6.4 content). It is stated as the parametric hypothesis so consumers and the eventual proof
share the exact interface; see docs/orchestration/p15f2-option1-scoping.md.
The difference datum of two factor sets: the pointwise 𝔽₂-sum of their factor sets and
central corrections. Over 𝔽₂ this is simultaneously the sum and the difference (sub = add), and
is the object measuring how Q⁰_loc can change with the datum choice.
Equations
Instances For
Additivity of graphPullback along the difference datum: graphPullback is 𝔽₂-linear in
the datum, so the pullback of diffDatum dat1 dat2 is the sum of the two pullbacks.
The difference of two equivariant factor sets for the same form is one for the zero form
(Lemma 6.1, gauge level): both share the form q, so their pointwise 𝔽₂-difference kills the
diagonal and the polar, leaving an equivariant factor set for 0. This is the datum whose graph
pullback measures the Q⁰_loc datum-defect.
Q⁰_loc datum-independence, parametric on DI-core (Lemma 6.1/6.4): if the graph pullback of
the zero-form difference datum lands in B² (hcore — the isolated cohomological heart), then
Q⁰_loc agrees for the two equivariant factor sets dat1, dat2 of the same form q. Composes
graphPullback_diffDatum (𝔽₂-linearity, with sub = add in char 2) and H2ofFun_eq_of_sub_mem_B2.
This is the bridge that lets lemma_6_17_vanish (stated for arbitrary dat) be reduced to the
orbit-sum datum on the regular module.
(a1) the C-independent quadratic refinement (the Lemma 6.17 vanishing proof increment A): a zero-form equivariant
factor set Δdat admits a quadratic refinement Δφ with polar Δdat.f, i.e.
Δφ(u+w) = Δφ u + Δφ w + Δdat.f u w (the identity (Q)). The zero form makes Δdat.f symmetric
(f_polar) with zero diagonal (f_diag), so the twisted extension ZFExt — addition
(v,a)+(w,b) = (v+w, a+b+Δdat.f v w) — is an elementary abelian 2-group (hV2), hence an
𝔽₂-vector space; its base-projection is a surjective 𝔽₂-linear map, and any linear right
inverse s gives Δφ v := (s v).fib with (Q) (from s additive). C-independent (no Δm); the
equivariance defect is corrected in increment B.
(a2) the equivariance correction (the Lemma 6.17 vanishing proof increment B): given the C-structure of an odd
normal subgroup I ◁ C acting fixed-point-freely (hVI : V^I = 0), the quadratic refinement of
increment A can be corrected to also satisfy the equivariance-defect identity (E)
Δφ(c•v) = Δφ v + Δdat.m c v, giving the full refinement (Q) ∧ (E) that
graphPullback_mem_B2_of_refinement consumes.
Proof (the banked f1 averaging pattern, cf. inflationVanishes_of_oddNormal): the defect
D c v = Δφ₀(c•v) + Δφ₀ v + Δm c v is additive in v ((Q) + m_quad) and a right 1-cocycle in
c (m_mul). Step A: L₀ = Σ_{i∈I} D i kills the defect on I (cocycle expansion +
mulRight reindex + |I| odd in 𝔽₂), and Δφ = Δφ₀ + L₀ keeps (Q) (L₀ additive).
Step B: normality makes the corrected defect D' I-invariant (D' c (i•v) = D' c v via
c i = i' c, i' = c i c⁻¹ ∈ I), whence
D' c v = Σ_{i∈I} D' c (i•v) = D' c (Σ_{i∈I} i•v) = D' c 0 = 0
since Σ_{i∈I} i•v ∈ V^I = 0. No general H¹(C,V*) theory.
The DI-core cochain assembly — reduced to the existence of a refinement #
DI-core (graphPullback (zero-form factor set) ∈ B²) has an explicit coboundary witness
Λ(g) = Δφ(b g) for a quadratic refinement Δφ : V → 𝔽₂ of the datum, i.e. a Δφ with polar
Δdat.f (hQ: Δφ(u+w) = Δφ u + Δφ w + Δf u w) and equivariance defect Δdat.m
(hE: Δφ(c•v) = Δφ v + Δm c v). The verification δ¹Λ = graphPullback Δdat is the char-2
identity below. This lemma discharges the cochain heart; the sole remaining input for full
DI-core / Q0loc_datum_indep is the existence of such a Δφ for the difference datum — the
H²(V;𝔽₂)-splitting [Δf]=0 (free: Δf has zero diagonal) plus the H¹(C,V*) equivariance
correction (docs/orchestration/p15f2-option1-scoping.md §P0, sub-bricks a1/a2).
Q⁰_loc datum-independence from a refinement (the Lemma 6.17 vanishing proof capstone): a quadratic refinement
Δφ of the difference datum diffDatum dat1 dat2 (with polar hQ and equivariance-defect hE)
makes Q⁰_loc agree for dat1 and dat2. Composes graphPullback_mem_B2_of_refinement (the
coboundary) with Q0loc_datum_indep_of_core. The remaining f2a input is the construction of
Δφ (the H²(V;𝔽₂)-splitting + H¹(C,V*) correction).
(a3) Q⁰_loc datum-independence (the Lemma 6.17 vanishing proof capstone): for two equivariant factor sets
dat1, dat2 of the same form q, an odd normal subgroup I ◁ C acting fixed-point-freely
(hVI : V^I = 0) forces Q⁰_loc dat1 = Q⁰_loc dat2. Composes isEquivariantFactorSet_diffDatum
(the difference is a zero-form datum) → exists_equivariant_refinement (the full (Q)∧(E)
refinement, increments A+B) → Q0loc_datum_indep_of_refinement. This is the f2a result; the
tame instantiation of (I, hIn, hodd, hVI) (e.g. I = zpowers (c tameTau), via the banked
producers
tameInertia_normal / odd_orderOf_tameInertia / fixedByNormal_eq_bot) stays with f2d.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (103) = ⟦eq-shapirosquare⟧
- eq. (105) = ⟦eq-shapiroevens⟧
- Lemma 6.1 = ⟦lem-extraspecialconnecting⟧
- Lemma 6.14 = ⟦lem-regularrealization⟧
- Lemma 6.15 = ⟦lem-orbitshapiro⟧
- Lemma 6.16 = ⟦lem-evensvanish⟧
- Lemma 6.17 = ⟦lem-shapirodet⟧
- Lemma 6.4 = ⟦lem-detnormalizationindependence⟧