The involution-orbit Shapiro ledger

The compatible transversal, position identity, and final involution coboundary chain.

See GQ2.Shapiro.Ledger for the paper-facing overview, source citations, and deviations.

Lemma 6.15, involution orbits (105) — foundations

The involution case compares graphPullback(invOrbitDatum_{N,ḡ}) with cor_{U₀→G} of the two-point Evens cocycle evensNormFun_{N≤U₀} (paper (107)–(109)), where U₀ = ⟨N, ĝ⟩ is the index-2-over-N subgroup (fixed field K₀ = K^{⟨ḡ⟩}) and ḡ = mk ĝ is an involution of G/N. These are the setup lemmas: ḡ is an involution, G/U₀ is finite, and the two index sets G/U₀ and (G/N)/⟨ḡ⟩ correspond (U₀ maps onto ⟨ḡ⟩ under G ↠ G/N).

theorem GQ2.ShapiroLedger.ghatQuot_sq {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg2 : ghat * ghat ∈ N) : (QuotientGroup.mk' N) ghat * (QuotientGroup.mk' N) ghat = 1

ḡ = mk ĝ is an involution of G/N when ĝ² ∈ N.

theorem GQ2.ShapiroLedger.map_U0_eq_zpowers {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : Subgroup.map (QuotientGroup.mk' N) U₀ = Subgroup.zpowers ((QuotientGroup.mk' N) ghat)

The image of U₀ = ⟨N, ĝ⟩ under G ↠ G/N is ⟨ḡ⟩ (N dies, ĝ ↦ ḡ).

theorem GQ2.ShapiroLedger.finite_quot_U0 {G : Type u_1} [Group G] (N : Subgroup G) [Finite (G ⧸ N)] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : Finite (G ⧸ U₀)

G/U₀ is finite (U₀ ⊇ N has index dividing the finite N.index).

def GQ2.ShapiroLedger.invIndexEquiv {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : G ⧸ U₀ ≃ (G ⧸ N) ⧸ Subgroup.zpowers ((QuotientGroup.mk' N) ghat)

The index correspondence G/U₀ ≃ (G/N)/⟨ḡ⟩: both are the coset space of the index-2-over-N subgroup U₀ = ⟨N, ĝ⟩ (whose image in G/N is ⟨ḡ⟩). This bijects the two orbit index sets of the involution comparison.

Equations

• GQ2.ShapiroLedger.invIndexEquiv N ghat U₀ hU₀ = { toFun := Quotient.lift (fun (g : G) => ↑↑g) ⋯, invFun := Quotient.lift (Quotient.lift (fun (g : G) => ↑g) ⋯) ⋯, left_inv := ⋯, right_inv := ⋯ }

noncomputable def GQ2.ShapiroLedger.orbOut {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (z : G ⧸ N) : G ⧸ N

The ⟨ḡ⟩-orbit canonical representative of a G/N-element z.

Equations

• GQ2.ShapiroLedger.orbOut N ghat z = Quotient.out ↑z

theorem GQ2.ShapiroLedger.phi_inv_eq {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat γ η : G) : graphPullback (invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (Corestriction.shapiroFun N ↑α) (γ, η) = ∑ᶠ (u : (G ⧸ N) ⧸ Subgroup.zpowers ((QuotientGroup.mk' N) ghat)), ↑α (Corestriction.lTrans N (Quotient.out u) γ) * ↑α (Corestriction.lTrans N (((QuotientGroup.mk' N) γ)⁻¹ * (Quotient.out u * (QuotientGroup.mk' N) ghat)) η) + ∑ᶠ (u : (G ⧸ N) ⧸ Subgroup.zpowers ((QuotientGroup.mk' N) ghat)), (if ((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out u = orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out u) then 0 else 1) * (↑α (Corestriction.lTrans N (orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out u)) η) * ↑α (Corestriction.lTrans N (orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out u) * (QuotientGroup.mk' N) ghat) η))

The involution graph pullback, unfolded to the two explicit sums of paper eq. (107) (the oriented factor-set term + the orientation-reversal correction).

theorem GQ2.ShapiroLedger.orderOf_ghatQuot {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) : orderOf ((QuotientGroup.mk' N) ghat) = 2

ḡ = mk ĝ has order exactly 2 in G/N (ĝ ∉ N, ĝ² ∈ N).

theorem GQ2.ShapiroLedger.subgroupOf_index_two {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : (N.subgroupOf U₀).index = 2

N has index 2 in U₀ = ⟨N, ĝ⟩: the map U₀ → G/N has kernel N.subgroupOf U₀ and range ⟨ḡ⟩ (order 2), so U₀/(N.subgroupOf U₀) ≅ ⟨ḡ⟩.

Involution assembly — setup

theorem GQ2.ShapiroLedger.subgroupOf_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) (hNo : IsOpen ↑N) (U₀ : Subgroup G) : IsOpen ↑(N.subgroupOf U₀)

N.subgroupOf U₀ is open in U₀ (preimage of the open N under U₀ ↪ G).

noncomputable def GQ2.ShapiroLedger.alphaOn {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (U₀ : Subgroup G) : ↥(N.subgroupOf U₀) → ZMod 2

The restriction of α to N.subgroupOf U₀ (reading α at the underlying N-element).

Equations

• GQ2.ShapiroLedger.alphaOn N α U₀ u = ↑α ⟨↑↑u, ⋯⟩

theorem GQ2.ShapiroLedger.alphaOn_hom {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (U₀ : Subgroup G) (x y : ↥(N.subgroupOf U₀)) : alphaOn N α U₀ (x * y) = alphaOn N α U₀ x + alphaOn N α U₀ y

alphaOn is additive (inherited from α, a hom on N).

theorem GQ2.ShapiroLedger.alphaOn_continuous {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (U₀ : Subgroup G) : Continuous (alphaOn N α U₀)

alphaOn is continuous.

Step 2 — the Evens-norm building blocks as explicit α-values

evensAux/bS on U₀ (relative to N.subgroupOf U₀, shift ĝ) read α at the underlying N-element, using the index-2 side bookkeeping (ĝ ∉ N; x·ĝ ∈ N ⟺ x ∉ N).

Step 3 — the transversal reconciliation

Both sides are now sums over O = (G/N)/⟨ḡ⟩ (phi_inv_eq, psi_inv_reindex). The pieces below bridge the U₀-transversal words (ℓ^{U₀}, used by psi) and the N-transversal words (ℓ^N, used by phi), and the orientation.

theorem GQ2.ShapiroLedger.orbit_equiv {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) : ↑((QuotientGroup.mk' N) (Quotient.out (γ⁻¹ • v))) = ↑(((QuotientGroup.mk' N) γ)⁻¹ * (QuotientGroup.mk' N) (Quotient.out v))

Orbit equivariance: the ⟨ḡ⟩-orbit of mk((γ⁻¹•v).out) equals that of γ̄⁻¹·mk(v.out) (both are N-images of U₀-lifts of γ⁻¹•v).

theorem GQ2.ShapiroLedger.mem_zpowers_sq_one {H : Type u_2} [Group H] {g t : H} (hg2 : g * g = 1) (ht : t ∈ Subgroup.zpowers g) : t = 1 ∨ t = g

In ⟨g⟩ with g² = 1, every element is 1 or g.

theorem GQ2.ShapiroLedger.out_ghat_shift {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (k : G ⧸ N) : Quotient.out (k * ↑ghat) = Quotient.out k * ghat * shiftCorr N ghat k

The .out shift: (k·ḡ).out = k.out · ĝ · shiftCorr(k) (rearranged shiftCorr).

The compatible transversal invLift (Step 2)

invLift v := ((invIndexEquiv v).out).out lifts each U₀-coset through the orbit-canonical G/N-base point z_u — the same base point phi_inv_eq reads. Along it the ℓ^T-words are based exactly at phi's indices and the aligned/flipped discriminant is literally phi's ε-condition.

theorem GQ2.ShapiroLedger.invIndexEquiv_mk {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (g : G) : (invIndexEquiv N ghat U₀ hU₀) ↑g = ↑↑g

invIndexEquiv computes on mk-classes (definitional).

noncomputable def GQ2.ShapiroLedger.invLift {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : G ⧸ U₀ → G

The compatible transversal: lift each U₀-coset through the orbit-canonical G/N-representative.

Equations

• GQ2.ShapiroLedger.invLift N ghat U₀ hU₀ v = Quotient.out (Quotient.out ((GQ2.ShapiroLedger.invIndexEquiv N ghat U₀ hU₀) v))

theorem GQ2.ShapiroLedger.mk_invLift {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) : ↑(invLift N ghat U₀ hU₀ v) = Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)

The G/N-image of invLift v is the orbit-canonical base point z_u.

theorem GQ2.ShapiroLedger.invLift_spec {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) : ↑(invLift N ghat U₀ hU₀ v) = v

invLift is a genuine transversal: it lifts v to v.

theorem GQ2.ShapiroLedger.invIndexEquiv_smul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) : (invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v) = ↑(((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v))

The γ-shifted index in orbit form: invIndexEquiv (γ⁻¹ • v) = mk_O (γ̄⁻¹ · z_u).

theorem GQ2.ShapiroLedger.invIndexEquiv_smul_out {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) : Quotient.out ((invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v)) = orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v))

The γ-shifted base point is the orbit-canonical rep of γ̄⁻¹ · z_u.

theorem GQ2.ShapiroLedger.mk_lWordT_invLift {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) : ↑(lWordT U₀ (invLift N ghat U₀ hU₀) v γ) = (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v))⁻¹ * (QuotientGroup.mk' N) γ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v))

The G/N-image of the compatible-transversal word: z_u⁻¹ · γ̄ · z_{u'}.

theorem GQ2.ShapiroLedger.lWordT_invLift_mem_N_iff {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∈ N ↔ ((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v) = orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v))

Alignment discriminant: the compatible-transversal word lies in N iff γ̄⁻¹ · z_u is its own orbit-canonical rep — literally phi_inv_eq's ε-condition.

Word identities and α-reads along invLift (Step 3)

On the compatible transversal the aligned reads are on the nose and every flipped or bS-read carries only shiftCorr-corrections, collapsed to the single correction read dRead via the duality sc(m·ḡ) = (ĝ·sc(m)·ĝ)⁻¹.

theorem GQ2.ShapiroLedger.invIndexEquiv_out_aligned {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) (hx : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∈ N) : Quotient.out ((invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v)) = γ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)

Aligned z'-characterization: if the compatible word lies in N, the shifted base point is the plain γ-shift of the base point.

theorem GQ2.ShapiroLedger.invIndexEquiv_out_flipped {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) : ghat ∉ N → ∀ (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) (hx : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∉ N), Quotient.out ((invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v)) = γ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v) * (QuotientGroup.mk' N) ghat

Flipped z'-characterization: if the compatible word is not in N, the shifted base point is the γ-shift times ḡ.

theorem GQ2.ShapiroLedger.lWordT_invLift_aligned {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) (hx : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∈ N) : lWordT U₀ (invLift N ghat U₀ hU₀) v γ = Corestriction.lWord N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) γ

W1 (aligned word identity): on the aligned locus the compatible word IS the canonical N-transversal word at the base point — on the nose.

theorem GQ2.ShapiroLedger.lWordT_invLift_flipped {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (γ : G) (hx : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∉ N) : lWordT U₀ (invLift N ghat U₀ hU₀) v γ = Corestriction.lWord N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) γ * ghat * shiftCorr N ghat (γ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v))

W2 (flipped word identity): on the flipped locus the compatible word is the canonical word times ĝ times a shiftCorr correction.

theorem GQ2.ShapiroLedger.shiftCorr_ghat_mul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg2 : ghat * ghat ∈ N) (m : G ⧸ N) : shiftCorr N ghat (m * ↑ghat) = (ghat * shiftCorr N ghat m * ghat)⁻¹

shiftCorr duality: sc(m·ḡ) = (ĝ · sc(m) · ĝ)⁻¹ (from shifting twice, ḡ² = 1).

theorem GQ2.ShapiroLedger.ghat_conj_lWord {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (k : G ⧸ N) (η : G) : ghat⁻¹ * Corestriction.lWord N k η * ghat = shiftCorr N ghat k * Corestriction.lWord N (k * ↑ghat) η * (shiftCorr N ghat (η⁻¹ • k))⁻¹

The ĝ-conjugated canonical word (rearranged lWord_shift): ĝ⁻¹·ℓ_k(η)·ĝ = sc(k) · ℓ_{kḡ}(η) · sc(η⁻¹•k)⁻¹.

theorem GQ2.ShapiroLedger.mk_eq_ghat_of_notMem {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) : ghat ∉ N → ∀ (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (x : G) (hxU : x ∈ U₀) (hx : x ∉ N), ↑x = (QuotientGroup.mk' N) ghat

x ∈ U₀ \ N has G/N-image exactly ḡ.

noncomputable def GQ2.ShapiroLedger.scEl {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (m : G ⧸ N) : ↥N

shiftCorr as an element of ↥N.

Equations

• GQ2.ShapiroLedger.scEl N ghat m = ⟨GQ2.ShapiroLedger.shiftCorr N ghat m, ⋯⟩

noncomputable def GQ2.ShapiroLedger.dRead {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (m : G ⧸ N) : ZMod 2

The correction read D(m) = α(sc(m)).

Equations

• GQ2.ShapiroLedger.dRead N α ghat m = ↑α (GQ2.ShapiroLedger.scEl N ghat m)

theorem GQ2.ShapiroLedger.evensAux_lTransT_aligned {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hgU : ghat ∈ U₀) (v : G ⧸ U₀) (γ : G) (hx : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∈ N) : evensAux (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (lTransT U₀ (invLift N ghat U₀ hU₀) ⋯ v γ) = ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) γ)

R1 (aligned evensAux-read): on the aligned locus, the evensAux-read of the compatible word is the canonical α-read at the base point — no corrections.

theorem GQ2.ShapiroLedger.evensAux_lTransT_flipped {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) (v : G ⧸ U₀) (γ : G) (hx : lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∉ N) : evensAux (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (lTransT U₀ (invLift N ghat U₀ hU₀) ⋯ v γ) = ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) γ) + dRead N α ghat (γ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v) * ↑ghat)

R2 (flipped evensAux-read): on the flipped locus, the read is the canonical α-read plus the correction D((γ⁻¹•z)·ḡ).

theorem GQ2.ShapiroLedger.bS_lTransT_aligned {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : ghat ∉ N → ghat * ghat ∈ N → ∀ (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) (w : G ⧸ U₀) (η : G) (hy : lWordT U₀ (invLift N ghat U₀ hU₀) w η ∈ N), bS (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (lTransT U₀ (invLift N ghat U₀ hU₀) ⋯ w η) = dRead N α ghat (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) w)) + ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) w) * ↑ghat) η) + dRead N α ghat (η⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) w))

R5 (aligned bS-read): for an aligned η-slot at base z', the bS-read is the canonical α-read at z'·ḡ plus corrections D(z') + D(η⁻¹•z').

theorem GQ2.ShapiroLedger.bS_lTransT_flipped {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) (w : G ⧸ U₀) (η : G) (hy : lWordT U₀ (invLift N ghat U₀ hU₀) w η ∉ N) : bS (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (lTransT U₀ (invLift N ghat U₀ hU₀) ⋯ w η) = dRead N α ghat (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) w)) + ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) w) * ↑ghat) η)

R6 (flipped bS-read): for a flipped η-slot at base z', the bS-read is D(z') plus the canonical α-read at z'·ḡ.

The position identity (Step 4a)

Per orbit position, the compatible-transversal evensNormFun-read equals phi_inv_eq's two summands plus the three coboundary terms of the aligned-locus Λ(σ) = Σ_{u aligned-for-σ} α(ℓ_{z_u}σ)·D(σ̄⁻¹•z_u) — verified cell-by-cell over the four aligned/flipped combinations.

theorem GQ2.ShapiroLedger.quot_mul_ghat_sq {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg2 : ghat * ghat ∈ N) (m : G ⧸ N) : m * ↑ghat * ↑ghat = m

ḡ²-collapse on G/N.

theorem GQ2.ShapiroLedger.smul_mul_ghat {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat σ : G) (m : G ⧸ N) : σ⁻¹ • (m * ↑ghat) = σ⁻¹ • m * ↑ghat

The σ-action commutes with right-ḡ: σ⁻¹•(m·ḡ) = (σ⁻¹•m)·ḡ.

theorem GQ2.ShapiroLedger.mk'_inv_mul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (σ : G) (m : G ⧸ N) : ((QuotientGroup.mk' N) σ)⁻¹ * m = σ⁻¹ • m

The mk'-form of the plain shift.

theorem GQ2.ShapiroLedger.lWordT_mul_mem_of_notMem {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (T : G ⧸ U₀ → G) (hT : ∀ (v : G ⧸ U₀), ↑(T v) = v) (v : G ⧸ U₀) (γ η : G) (hx : lWordT U₀ T v γ ∉ N) (hy : lWordT U₀ T (γ⁻¹ • v) η ∉ N) : lWordT U₀ T v (γ * η) ∈ N

(F,F) product membership: two flipped words multiply into N (ḡ² = 1).

theorem GQ2.ShapiroLedger.invPositionEval {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) (v : G ⧸ U₀) (γ η : G) : evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (lTransT U₀ (invLift N ghat U₀ hU₀) ⋯ v γ, lTransT U₀ (invLift N ghat U₀ hU₀) ⋯ (γ⁻¹ • v) η) = ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) γ) * ↑α (Corestriction.lTrans N (((QuotientGroup.mk' N) γ)⁻¹ * (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v) * (QuotientGroup.mk' N) ghat)) η) + (if ((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v) = orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) then 0 else 1) * (↑α (Corestriction.lTrans N (orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v))) η) * ↑α (Corestriction.lTrans N (orbOut N ghat (((QuotientGroup.mk' N) γ)⁻¹ * Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) * (QuotientGroup.mk' N) ghat) η)) + (((if lWordT U₀ (invLift N ghat U₀ hU₀) v γ ∈ N then ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) γ) * dRead N α ghat (γ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) else 0) + if lWordT U₀ (invLift N ghat U₀ hU₀) (γ⁻¹ • v) η ∈ N then ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v))) η) * dRead N α ghat (η⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) (γ⁻¹ • v))) else 0) + if lWordT U₀ (invLift N ghat U₀ hU₀) v (γ * η) ∈ N then ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) (γ * η)) * dRead N α ghat ((γ * η)⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) else 0)

The position identity: at each orbit position, the compatible-transversal Evens-norm read equals the two phi_inv_eq summands plus the three coboundary terms of the aligned-locus Λ.

The involution coboundary invLambda and the δ-assembly (Step 4b)

noncomputable def GQ2.ShapiroLedger.invLambda {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : G → ZMod 2

The involution transversal-change 1-cochain: the aligned-locus sum Λ(σ) = Σ_{v aligned-for-σ} α(ℓ_{z_v}σ)·D(σ⁻¹•z_v).

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.ShapiroLedger.invLambda_summand_eq {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (v : G ⧸ U₀) (σ : G) : (if lWordT U₀ (invLift N ghat U₀ hU₀) v σ ∈ N then ↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) σ) * dRead N α ghat (σ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) else 0) = (if ↑(lWordT U₀ (invLift N ghat U₀ hU₀) v σ) = 1 then 1 else 0) * (↑α (Corestriction.lTrans N (Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)) σ) * dRead N α ghat (σ⁻¹ • Quotient.out ((invIndexEquiv N ghat U₀ hU₀) v)))

The aligned-indicator summand in indicator-product form (for continuity).

theorem GQ2.ShapiroLedger.invLambda_continuous {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) : Continuous (invLambda N α ghat U₀ hU₀)

invLambda is continuous (U₀ ⊇ N is open; the alignment indicator factors through the discrete G/N).

theorem GQ2.ShapiroLedger.graphPullback_sub_cor2FunT_mem_B2 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) : (graphPullback (invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (Corestriction.shapiroFun N ↑α) - cor2FunT U₀ (invLift N ghat U₀ hU₀) ⋯ fun (p : ↥U₀ × ↥U₀) => evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (p.1, p.2)) ∈ ContCoh.B2 G (ZMod 2)

The involution coboundary (Step 4b): the graph pullback differs from the compatible-transversal corestriction by δ¹(invLambda).

The final chain (Step 5): lemma_6_15_involution_aux

theorem GQ2.ShapiroLedger.alphaOn_one {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (U₀ : Subgroup G) : alphaOn N α U₀ 1 = 0

alphaOn kills the identity.

theorem GQ2.ShapiroLedger.evensNormFun_right_one {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (U₀ : Subgroup G) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) (z : ↥U₀) : evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (z, 1) = 0

The Evens-norm cochain is right-normalized: ν(z, 1) = 0.

theorem GQ2.ShapiroLedger.evensNormFun_cocForm {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (hNo : IsOpen ↑N) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (U₀ : Subgroup G) (hgU : ghat ∈ U₀) (hUi : (N.subgroupOf U₀).index = 2) (hs : ⟨ghat, hgU⟩ ∉ N.subgroupOf U₀) (a b c : ↥U₀) : evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (b, c) + evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (a * b, c) + evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (a, b * c) + evensNormFun (N.subgroupOf U₀) ⟨ghat, hgU⟩ (alphaOn N α U₀) (a, b) = 0

The Evens-norm cochain satisfies the char-2 four-term cocycle identity.

theorem GQ2.ShapiroLedger.lemma_6_15_involution_aux {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hs : ⟨ghat, ⋯⟩ ∉ N.subgroupOf U₀) : H2ofFun G (graphPullback (invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (Corestriction.shapiroFun N ↑α)) = H2ofFun G (Corestriction.cor2Fun U₀ fun (p : ↥U₀ × ↥U₀) => evensNormFun (N.subgroupOf U₀) ⟨ghat, ⋯⟩ (fun (u : ↥(N.subgroupOf U₀)) => ↑α ⟨↑↑u, ⋯⟩) (p.1, p.2))

Lemma 6.15, involution orbits (105) — the graph pullback of the involution orbit datum equals the corestriction of the index-two Evens norm, as H2ofFun-classes. Chains the compatible-transversal coboundary (graphPullback_sub_cor2FunT_mem_B2) with the transversal-change coboundary (cor2FunT_sub_cor2Fun_mem_B2).