§8 zero-edge engines: Lemma 8.7 (affine T-lifting) + Prop 8.8, target side #
When the radical edge of the scalar cover p_λ vanishes — the ∃ N-branch of the (140)
case split, i.e. ¬ D.NoDescent — the paper (pp. 40–43) runs three steps to evaluate the
constrained Gauss sum. This file provides the source-generic, target-side halves:
descended_splitting(Lemma 6.21 application): the descent datumNmakesQ = Bg/Ta split extension ofC₀byV, i.e.∃ σ : C₀ →* QsectioningpiQbar. Consumes theκ⁰_qdatum (theEnrichmentfields of the Prop. 8.9 assembly) exactly as the paper's "fix the base determinant class" clause requires.lemma_8_7_count(Lemma 8.7, (131)/(132), count form): the centralM-lifts over a lower mapρfibre over theirV-coordinates with constant multiplicity#Z¹_{Γ,ρ}(T). The torsor structure is the central-obstruction frameworktwistinvolution;Central-invariance under aT-twist isob_twistwith the vanishing variation class (theN-complement hasedge ≡ 0).prop_8_8_target(Prop 8.8, (133)/(134), target side): the edge-killing shear, an instance of the provedlemma_6_22, produces the total scalar phaseDeltaScalar. The Γ-level completed-square (135) — which consumes cor. 5.17 — is out of scope (the Prop. 8.9 assembly, behind the Prop. 5.15 proof firewall).
Plus exists_polar_inverse, the finite-linear-algebra supplier of the shift vectors
a_{χ,κ} of (133) (cf. lemma_8_5's a-data-with-spec).
Design decisions D1–D6 and the full work order: docs/orchestration/p16d4-plan.md. Deviation-ledger
entries D1 (cocycle-level 8.7) and D3 (6.22-normalized Δ): docs/section8-extraction.md.
Everything is finite-group / generic-Γ; no B6/B7, no the Prop. 5.15 proof material; all std-3.
The N-section and the vanishing edge #
In the zero-edge regime we are handed a normal complement N ◁ B̃ with p(N) = T and
z ∉ N (the negation of NoDescent). Since p|_N : N ≅ T is a bijection, its inverse
sectN is a homomorphic section of p over T whose image N is normal — so the edge
cocycle of the resulting TComplement vanishes identically.
A descent datum for the scalar cover: a normal complement N ◁ B̃ to ⟨z⟩ over T
(p(N) = T, z ∉ N). This is the negation of D.NoDescent unpacked; d6 obtains it from
radData_noDescent_iff. Its existence is the zero-edge case of the (140) split.
Instances For
Every element of N covers a T-element (p(N) = T).
p|_N : N → T as a homomorphism.
Equations
- GQ2.SectionEight.AffineTLift.pN Dsc = (D.C.p.comp Dsc.N.subtype).codRestrict D.T ⋯
Instances For
p|_N : N ≅ T as a group isomorphism.
Equations
- GQ2.SectionEight.AffineTLift.eN Dsc = MulEquiv.ofBijective (GQ2.SectionEight.AffineTLift.pN Dsc) ⋯
Instances For
The N-section T → B̃: the inverse of p|_N, landing in the normal complement.
Equations
- GQ2.SectionEight.AffineTLift.sectN Dsc = Dsc.N.subtype.comp (GQ2.SectionEight.AffineTLift.eN Dsc).symm.toMonoidHom
Instances For
The N-section, packaged as a TComplement.
Equations
- GQ2.SectionEight.AffineTLift.SN Dsc = { s := GQ2.SectionEight.AffineTLift.sectN Dsc, sect := ⋯ }
Instances For
The edge vanishes on the N-complement: conjugation preserves the normal N, so
the section's conjugation defect is trivial. This is what makes the (129) variation class
zero in the zero-edge regime.
The descended semidirect structure on Q = Bg/T #
T is normal (it is D.hT), so Q := Bg ⧸ T is a group and the projection piT sits over
piQbar : Q ↠ C₀ (the lift of piC₀, which kills T ≤ M). Its kernel is V = M/T, and
the descent iso descend : M ↠ V gives the inclusion iV : V ↪ Q characterized by
iV (descend m) = piT m. All the extension data of 1 → V → Q → C₀ → 1 reads off iV.
The descended κ⁰_q datum for the zero-edge regime (the Prop. 8.9 assembly Enrichment fields at
a fixed nonzero λ, in the source-generic RadicalCoverData vocabulary). The C-stage
group C₀ (with piC₀ : Bg ↠ C₀, ker = M), the descended module V = M/T with its
C₀-action and the descent surjection descend : M ↠ V, the descended nonsingular form
q̄, and its fixed equivariant factor-set datum (Lemma 6.1's κ⁰_{q̄} — the relative
hypothesis of lemma_6_21). d6 builds one DescData from E : RF.Enrichment at (l,h)
via E.radData l h, RF.piBC, RF.ker_piBC, and the descended-module fields.
- C0 : Type
The
C-stage groupC₀ = B/M. - gC0 : Group self.C0
- fC0 : Finite self.C0
- piC0 : Bg →* self.C0
The projection
piC₀ : B ↠ C₀. - hpiC0 : Function.Surjective ⇑self.piC0
- Vmod : Type
The descended module
V = M/T. - aVmod : AddCommGroup self.Vmod
- fVmod : Finite self.Vmod
The descent surjection
M ↠ V.- hdesc_surj : Function.Surjective ⇑self.descend
- hdesc_conj (bb : Bg) (m : ↥D.M) (hm : bb * ↑m * bb⁻¹ ∈ D.M) : self.descend ⟨bb * ↑m * bb⁻¹, hm⟩ = Multiplicative.ofAdd (self.piC0 bb • Multiplicative.toAdd (self.descend m))
descendintertwinesB-conjugation with theC₀-action throughpiC₀. - qbar : self.Vmod → ZMod 2
The descended form
q̄onV. - hquad : QuadraticFp2.IsQuadraticFp2 self.qbar
- hns : QuadraticFp2.Nonsingular self.qbar
The fixed equivariant factor-set datum for
q̄(Lemma 6.1'sκ⁰_{q̄}).- hdat : IsEquivariantFactorSet self.qbar self.dat
q_λ = q̄ ∘ descendonM.
Instances For
The T-projection Bg ↠ Q.
Equations
- GQ2.SectionEight.AffineTLift.piT = QuotientGroup.mk' D.T
Instances For
T ≤ ker piC₀ (= M), so piC₀ descends to Q.
The connecting map piQbar : Q ↠ C₀, the descent of piC₀ through T ≤ M.
Equations
- GQ2.SectionEight.AffineTLift.piQbar DD = QuotientGroup.lift D.T DD.piC0 ⋯
Instances For
descend and the M-into-Q map have the same kernel T ∩ M.
The V-inclusion iV : V ↪ Q, the descent of M ↪ Bg ↠ Q through descend.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The characterizing identity: iV (descend m) = piT m for m ∈ M. Everything about
iV (injectivity, range, conjugation) is derived from this.
range iV = ker piQbar (= V): the extension 1 → V → Q → C₀ → 1 in lemma_6_21
form.
The conjugation law for the extension (lemma_6_21's hconj): iV intertwines
Q-conjugation with the C₀-action through piQbar.
The descended central double cover and its defect cocycle ξ #
Q̃ := B̃/N ↠ Q = B/T is a central double cover (its kernel is ⟨z̄⟩, z̄ = mk z, missing
1 since z ∉ N). Its defect cocycle ξ — the z̄-sign of the associativity defect of
a set-section — is the 𝔽₂-class of the extension, with ξ(iv, iv) = q̄(v) on the fibre
V. This is the class lemma_6_21 consumes; ξ avoids bundling Q̃ as a CentralCover
(hence no quotient-topology diamond) by reusing only the kernel-sign calculus.
The covering group Q̃ = B̃/N.
Equations
- GQ2.SectionEight.AffineTLift.covQ Dsc = (D.C.cover ⧸ Dsc.N)
Instances For
The descended cover map descP : Q̃ ↠ Q.
Equations
- GQ2.SectionEight.AffineTLift.descP Dsc = QuotientGroup.lift Dsc.N (GQ2.SectionEight.AffineTLift.piT.comp D.C.p) ⋯
Instances For
The central involution z̄ = mk z of the descended cover.
Equations
- GQ2.SectionEight.AffineTLift.zbar Dsc = (QuotientGroup.mk' Dsc.N) D.C.z
Instances For
Kernel elements of descP are 1 or z̄.
The z̄-sign on the descended cover (meaningful on ker descP = {1, z̄}).
Equations
- GQ2.SectionEight.AffineTLift.ccZsign Dsc x = if x = 1 then 0 else 1
Instances For
ccZsign of a z̄-power.
A normalized set-section s₀ : Q → Q̃ of descP (s₀ 1 = 1).
Equations
- GQ2.SectionEight.AffineTLift.s0 Dsc q = if q = 1 then 1 else Function.surjInv ⋯ q
Instances For
The defect 𝔽₂-cocycle ξ of the descended cover: the z̄-sign of the associativity
defect of s₀. This is the class lemma_6_21 consumes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ξ cocycle identity (lemma_6_21's hcocycle): from associativity of
s₀ g · s₀ h · s₀ k, computed via the two central defects.
descended_splitting: the Lemma 6.21 application #
With ξ in hand, the extension 1 → V → Q → C₀ → 1 splits. hξq reads the fibre square
map of ξ off q̄ (via D.hq/hqbar); lemma_6_21 (the Lemma 6.21 proof, proved) then delivers the
group-theoretic section σ : C₀ →* Q.
V has exponent 2 (it is M/T, and M is elementary abelian).
The fibre square identity ξ(iv, iv) = q̄(v) (lemma_6_21's hξq): the descended
cover's square map on V is the descended form. Uses D.hq (cover square relation) pushed
down through hqbar.
descended_splitting (the Prop. 8.9 assembly, 2.2): in the zero-edge regime the extension
1 → V → Q → C₀ → 1 splits — ∃ σ : C₀ →* Q sectioning piQbar. This is Lemma 6.21 at the
descended data, the paper's "B/T ≅ V ⋊ C". d6 provides DD/Dsc from the Enrichment.
Prop 8.8, target side: the edge-killing shear #
The completed-square identity (135), C-level half. Given an edge-killing shear a
(B_q̄(a c, ·) = γ c, i.e. hkill), the general determinant class κ⁰ + Γ_γ + inf δ
shears to κ⁰ + inf(Δ) up to coboundary, where Δ = δ + Θ⁰_q̄(a) + (γ ⌣ a) is the total
scalar phase. Direct instance of the proved lemma_6_22 with the γ + B♭a = 0 collapse.
The Γ-level (135) (which pulls this back along cor. 5.17) is d6, behind the Prop. 5.15 proof firewall.
The total scalar phase Δ = δ + Θ⁰_q̄(a) + (γ ⌣ a) (the (134)-analog; the γ⌣a
cup term is the lemma_6_22-normalized form, D3 — the family is ∃-bound in prop_8_9).
Equations
- GQ2.SectionEight.AffineTLift.DeltaScalar dat γ δ a cd = δ cd + GQ2.SectionSix.thetaPhase dat a cd + GQ2.SectionSix.gammaCupA γ a cd
Instances For
Prop 8.8, target side (the Prop. 8.9 assembly, 2.6): the edge-killing shear collapses the general
determinant class to κ⁰ + inf Δ up to an explicit coboundary.
The polar-inverse supplier (a_{χ,κ}) #
Finite 𝔽₂-linear algebra: a nonsingular quadratic form's polar map B♭ : V ↪ V∨ is
bijective, so every functional φ has a unique polar-preimage a. d5 uses this to define
the (133) shift vectors a_{χ,κ} from γ_χ + γ_κ (cf. lemma_8_5's a-data-with-spec).
exists_polar_inverse (the Prop. 8.9 assembly, 2.5): for nonsingular q on a finite 𝔽₂-space,
every functional φ is B_q(a, ·) for some a.
Lemma 8.7, count form: the T-twist torsor #
In the zero-edge regime the N-complement has edge ≡ 0, so the (129) variation class of
every T-cocycle vanishes. Hence twisting by a T-cocycle preserves the central relation
(central_twist_iff), and the fibres of the T-reduction map on M-lifts are free
T-cocycle torsors on which Central is constant. This is the multiplicity μ = #Z¹(T)
of Lemma 8.7 (131)/(132) — the V-coordinate factorization. The Γ-machinery is the central-obstruction framework's
twist/ob/central_iff_ob_eq_zero, reused verbatim.
The N-complement's variation cochain vanishes (edge ≡ 0).
central_twist_iff (the Prop. 8.9 assembly, 2.4b): in the zero-edge regime, twisting an M-lift by
a T-cocycle preserves the central relation — the (129) variation class is zero because the
normal N-complement has vanishing edge. This is what makes Central constant on the
T-cocycle torsors.
The T-reduction of an M-lift: red_T f = piT ∘ f : Γ → B/T. Its fibres are the
T-cocycle torsors of Lemma 8.7.
Equations
- GQ2.SectionEight.AffineTLift.redT ρ f γ = ↑(↑f γ)
Instances For
M centralizes T (T ≤ M, M abelian) — makes the crossed condition rep-independent.
Extensionality for T-cocycles (only the underlying function matters).
The T-cocycle torsor (the Prop. 8.9 assembly, 2.4a): fixing an M-lift f₀, the fibre of red_T
through f₀ is a torsor under Z¹_{Γ,ρ}(T) — every M-lift with the same T-reduction is a
unique T-twist of f₀. (Combined with central_twist_iff, this is the constant μ
multiplicity of (132).)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lemma 8.7, count form (the Prop. 8.9 assembly, 2.4c): the central M-lifts sharing the T-reduction
of a fixed central lift f₀ number exactly #Z¹_{Γ,ρ}(T) — the multiplicity μ of (132),
constant over the V-coordinate. (Central is automatic on the torsor once f₀ is central,
by central_twist_iff.) d6 sums this over the liftable V-coordinates to reach zBC.
The phase covers: centralCoverOfCocycle #
The twisted product 𝔽₂ ×_δ C₀ of a normalized 𝔽₂-valued 2-cocycle δ on a finite
group C₀ — a central double cover of C₀. This is the (133)/(134) phase-cover
constructor: d6's prop_8_9 phase family is ζ ↦ centralCoverOfCocycle (Δ_{χ,κ}), with the
scalar Δ produced by prop_8_8_target/DeltaScalar. Multiplicative analog of the Lemma 6.21 proof's
additive Transgression.Twisted.
The phase cover (the Prop. 8.9 assembly): the central double cover 𝔽₂ ×_δ C₀ ↠ C₀ of a normalized
𝔽₂-2-cocycle δ — multiplication (s,c)(t,d) = (s+t+δ(c,d), cd), kernel ⟨z⟩ with
z = (1,1). d6 instantiates δ := DeltaScalar … (the (134) total phase).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The phase family (the Prop. 8.9 assembly): the prop_8_9-shaped phase-cover family
DT → CentralCover C₀ from a family of normalized 2-cocycles. d6 supplies
Δ ζ := DeltaScalar … (the (134) total phase Δ_{χ,κ}), giving prop_8_9's phase
component directly; the shared (μ, G⁰, DT) are lemma_8_7_count's #Z¹(T), gaussSum
of the enrichment form, and the (T^∨)^C index.
Equations
- GQ2.SectionEight.AffineTLift.phaseFamily Δ hcoc hl hr ζ = GQ2.SectionEight.AffineTLift.centralCoverOfCocycle (Δ ζ) ⋯ ⋯ ⋯
Instances For
The canonical section of the twisted-product cover (the Prop. 8.9 assembly export): the phase cover
𝔽₂ ×_δ C₀ admits a normalized set-section s with multiplication defect exactly δ
(s c · s d = z^{δ(c,d)} · s(cd)). This is the (only) internals fact the phase-obstruction
layer needs: a lift of ρ through the cover exists iff ρ^*δ is a continuous coboundary
(GQ2/PhaseObstruction.lean).
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- cor 5.17 = ⟦cor-adjointboundary⟧
- Lemma 6.1 = ⟦lem-extraspecialconnecting⟧
- Lemma 6.21 = ⟦lem-transgression⟧
- Lemma 8.7 = ⟦lem-affinelifting⟧
- Prop 8.8 = ⟦prop-phaseidentity⟧