Assembling prop_5_15_R (candidate deformation duality) on the r_R spine (⟦prop:duality⟧)

prop_5_15_R : IsSelfDual_R t A for every finite elementary 𝔽₂[C]-module — the Roe note's Candidate deformation duality ⟦prop:duality⟧, the Γ_R twin of GQ2/DualityAssembly.lean. Route exactly as Γ_A: the simple modules are self-dual (selfDual_of_simple_R — trivial module via R25's trivialSelfDual_R; nontrivial simples via the ⟦lem:normalforms⟧ normal forms + the ⟦prop:hessian⟧ degree-one pairing), then the dévissage strong induction prop_5_15_of_simple_R (GQ2/Roe/DevissageInduction.lean, two-out-of-three lemma_5_11_R along a composition series).

The x₀ ↔ x₁ wild-column swap

The tame relator is shared with Γ_A, but the two wild columns are interchanged (GQ2.Roe.WildRow): the split Z¹_R shape is x 1 = 0 ∧ x 2 = 0 (Γ_A: x 1 = 0 ∧ x 3 = 0) and the normal form is x₁-supported (0,0,0,d) (x1Supported, slot x 3; Γ_A: x0Supported, slot x 2). Two signature deltas against the Γ_A twins, both from GQ2.Roe.NormalForms/GQ2.Roe.Hessian:

• the split shapes need no σ₂-tameness hU (σ₂ is only a conjugator in r_R; split_shapes_of_wild_R drops Γ_A split_shapes_of_wild's hU) — the split pairing mixedB_R_pairing_split still consumes hU, derived as in Γ_A from sigma2_smul_trivial;
• the ramified pairing lemmas carry no ht/hw arguments (mixedB_R_pairing_ramified).

Word-free ingredients are reused unsuffixed from the Γ_A assembly, never cloned: card_H0w_eq_one_of_nontrivial, card_fixedPts_elemDual_eq_one_of_nontrivial, tau_split_or_ramified, elemDual_smul_trivial_of (GQ2.DualityAssembly), the tame representation-theory providers (GQ2.TameSimple), H0w_eq_fixedPts and elemDual_separates (GQ2.Devissage).

Card bookkeeping for the simple case

For a nontrivial simple module the invariants H⁰w(A) = A^C vanish, so the normal form H¹_R ≅ A forces #Z¹_R = #A² and #H²_R = 1 — clauses 1 and 2 of IsSelfDual_R (via the Euler characteristic card_H1w_eq_R / rank-nullity card_Z1w_eq_sq_mul_card_H2w_R).

Corollary 5.17 numerics (cor_5_17_card_R)

"Comparison with the local complex then uses local Tate duality as in [RT Prop. 5.16 and Cor. 5.17]" (⟦prop:duality⟧'s proof): the word-generic local half prop_5_16 (GQ2/LocalLiftingDuality.lean) is reused verbatim — it never mentions the marking word — so the corollary is a thin splice of prop_5_15_R (clauses 1–2) against prop_5_16's display-(57) numerics.

theorem GQ2.FoxH.card_H1wR_of_normalForm {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (hx1mem : ∀ (d : A), x1Supported d ∈ Z1wR t) (hnf : ∀ x ∈ Z1wR t, ∃! d : A, x - x1Supported d ∈ B1wR t) : Nat.card (H1wR t) = Nat.card A

H¹_R ≅ A from the normal form: when every x₁-supported tuple is a Roe cocycle and every cocycle is uniquely x₁-supported modulo coboundaries (⟦lem:normalforms⟧), the class map A → H¹_R, d ↦ [x1Supported d], is a bijection, so #H¹_R = #A. Γ_R twin of card_H1w_of_normalForm under the x₀ ↔ x₁ swap.

theorem GQ2.FoxH.card_H2wR_and_Z1wR_of_nontrivial_simple {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hsimple : IsSimpleModTwo C A) (hnt : ∃ (c : C) (a : A), c • a ≠ a) (hx1mem : ∀ (d : A), x1Supported d ∈ Z1wR t) (hnf : ∀ x ∈ Z1wR t, ∃! d : A, x - x1Supported d ∈ B1wR t) : Nat.card (H2wR t) = 1 ∧ Nat.card ↥(Z1wR t) = Nat.card A ^ 2

Card clauses for a nontrivial simple module (feeding IsSelfDual_R): #H²_R = 1 and #Z¹_R = #A², from #H¹_R = #A (card_H1wR_of_normalForm), #H⁰w = 1 (the word-free card_H0w_eq_one_of_nontrivial, reused from GQ2.DualityAssembly), and the Euler characteristic card_H1w_eq_R / rank-nullity card_Z1w_eq_sq_mul_card_H2w_R.

mixedB_R descends to H¹_R (the degree-one pairing)

theorem GQ2.FoxH.mixedB_R_left_congr {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (x x' : Fin 4 → A) (y : Fin 4 → ElemDual A) (hb : x - x' ∈ B1wR t) (hy : y ∈ Z1wR t) : mixedB_R t x y = mixedB_R t x' y

mixedB_R is invariant under changing the primal argument by a coboundary (against a cocycle dual): B_R(x + d⁰a, y) = B_R(x, y) since B_R(d⁰a, y) = ⟨a, L_R(y)⟩ = 0 (prop_5_8_left_R, y a Roe cocycle). Uses mixedB_R bilinearity.

theorem GQ2.FoxH.mixedB_R_right_congr {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (x : Fin 4 → A) (y y' : Fin 4 → ElemDual A) (hb : y - y' ∈ B1wR t) (hx : x ∈ Z1wR t) : mixedB_R t x y = mixedB_R t x y'

Dual version: B_R(x, y + d⁰λ) = B_R(x, y) (prop_5_8_right_R, x a Roe cocycle).

theorem GQ2.FoxH.clause3_of_normalForm_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hx1memA : ∀ (d : A), x1Supported d ∈ Z1wR t) (hnfA : ∀ x ∈ Z1wR t, ∃! d : A, x - x1Supported d ∈ B1wR t) (hx1memD : ∀ (lam : ElemDual A), x1Supported lam ∈ Z1wR t) (hnfD : ∀ y ∈ Z1wR t, ∃! lam : ElemDual A, y - x1Supported lam ∈ B1wR t) (hndL : ∀ (d : A), d ≠ 0 → ∃ (lam : ElemDual A), mixedB_R t (x1Supported d) (x1Supported lam) ≠ 0) (hndR : ∀ (lam : ElemDual A), lam ≠ 0 → ∃ (d : A), mixedB_R t (x1Supported d) (x1Supported lam) ≠ 0) : ∃ (P : H1wR t → H1wR t → ZMod 2), (∀ (x : ↥(Z1wR t)) (y : ↥(Z1wR t)), P (h1wMkR t x) (h1wMkR t y) = mixedB_R t ↑x ↑y) ∧ (∀ (h : H1wR t), h ≠ 0 → ∃ (h' : H1wR t), P h h' ≠ 0) ∧ ∀ (h' : H1wR t), h' ≠ 0 → ∃ (h : H1wR t), P h h' ≠ 0

Clause 3 (degree-one perfect pairing) from a normal form. Given that x₁-supported cochains x1Supported d are Roe cocycles and hit every H¹_R class uniquely (the normal form of ⟦lem:normalforms⟧, for both A and A∨), and that the induced pairing d, λ ↦ B_R(x1Supported d, x1Supported λ) is nondegenerate on both sides, mixedB_R descends to a perfect pairing H¹_R(A) × H¹_R(A∨) → 𝔽₂. Descent uses mixedB_R_left_congr / mixedB_R_right_congr; nondegeneracy transports through the normal-form identification H¹_R ≅ A.

Split simple case: Z¹_R/B¹_R shapes, normal form, x₁-support

These are phrased against the split shapes (rather than lemma_5_13_split_R directly) so they apply equally to A and its contragredient dual A∨: the dual is split with trivial wild action whenever A is, without needing "the dual of a simple module is simple".

theorem GQ2.FoxH.split_shapes_of_wild_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hV₂ : ∀ (v : A), v + v = 0) (hx0 : ∀ (v : A), t.x₀ • v = v) (hx1 : ∀ (v : A), t.x₁ • v = v) (htau : ∀ (v : A), t.τ • v = v) (hVS : ∀ (v : A), t.σ • v = v → v = 0) : (∀ (x : Fin 4 → A), x ∈ Z1wR t ↔ x 1 = 0 ∧ x 2 = 0) ∧ ∀ (y : Fin 4 → A), y ∈ B1wR t ↔ ∃ (v : A), y = ![t.σ • v - v, 0, 0, 0]

The split Z¹_R/B¹_R shapes from a trivial wild action (hx0, hx1) rather than from simplicity — the body of lemma_5_13_split_R with wild_acts_trivially factored out as hypotheses, so it is usable on A∨ (where wild-triviality comes from the contragredient of A's). Unlike Γ_A's split_shapes_of_wild there is no hU: the Roe wild row liftMarking_wildValueR_u carries no σ₂-tameness dependency.

theorem GQ2.FoxH.x1mem_of_Z1wRShape {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (hZ : ∀ (x : Fin 4 → A), x ∈ Z1wR t ↔ x 1 = 0 ∧ x 2 = 0) (d : A) : x1Supported d ∈ Z1wR t

The x₁-supported cochains are Roe cocycles, straight from the split Z¹_R shape.

theorem GQ2.FoxH.normalForm_of_shapes_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (hZ : ∀ (x : Fin 4 → A), x ∈ Z1wR t ↔ x 1 = 0 ∧ x 2 = 0) (hB : ∀ (y : Fin 4 → A), y ∈ B1wR t ↔ ∃ (v : A), y = ![t.σ • v - v, 0, 0, 0]) (hVS : ∀ (v : A), t.σ • v = v → v = 0) (x : Fin 4 → A) : x ∈ Z1wR t → ∃! d : A, x - x1Supported d ∈ B1wR t

Split normal form: from the Z¹_R/B¹_R shapes and surjectivity of σ − 1 (from V^S = 0, hVS), every degree-one class has a unique x₁-supported representative.

Split simple case: IsSelfDual_R

theorem GQ2.FoxH.selfDual_of_split_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hV₂ : ∀ (v : A), v + v = 0) (hsimple : IsSimpleModTwo C A) (hcore : t.Pro2Core) (htau : ∀ (v : A), t.τ • v = v) (hσ : ∃ (v : A), t.σ • v ≠ v) : IsSelfDual_R t A

⟦prop:duality⟧, split simple case. A nontrivial simple module on which τ acts trivially (htau) and σ acts nontrivially (hσ) is self-dual for the Roe complex. The fixed-point freeness hVS comes from the tame representation-theory proof (fixedPoints_sigma_eq_zero); the contragredient dual A∨ inherits split + trivial-wild action from A (via elemDual_smul_trivial_of), giving both normal forms; the cards close clauses 1–2 and clause3_of_normalForm_R (with the split pairing (d,λ) ↦ λ(d), mixedB_R_pairing_split — whose hU is sigma2_smul_trivial, needed only here, not in the shapes) closes clause 3.

theorem GQ2.FoxH.selfDual_of_trivial_action_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hV₂ : ∀ (v : A), v + v = 0) (hσ : ∀ (v : A), t.σ • v = v) (htau : ∀ (v : A), t.τ • v = v) (hx0 : ∀ (v : A), t.x₀ • v = v) (hx1 : ∀ (v : A), t.x₁ • v = v) : IsSelfDual_R t A

Trivial-action case. If all four generators act trivially then (by hgen) every element of C does, and the module is self-dual for the Roe complex by R25's trivialSelfDual_R. This is the split sub-case where σ also acts trivially.

Ramified simple case

theorem GQ2.FoxH.x1Supported_mem_Z1wR_ramified {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hV₂ : ∀ (v : A), v + v = 0) (hx0 : ∀ (v : A), t.x₀ • v = v) (hx1 : ∀ (v : A), t.x₁ • v = v) (htau : ∀ (v : A), t.τ • v = v → v = 0) (hTodd : ∀ (v : A), powOmega2 t.τ • v = v) (d : A) : x1Supported d ∈ Z1wR t

In the ramified case the x₁-supported cochains are Roe cocycles: the shared tame row (d1Fun_tame) involves only coordinates 0 and 1, the Roe wild row is S⁻¹x₂ (liftMarking_wildValueR_u_ramified), and all three coordinates vanish on x1Supported d.

theorem GQ2.FoxH.selfDual_of_ramified_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hV₂ : ∀ (v : A), v + v = 0) (hsimple : IsSimpleModTwo C A) (hcore : t.Pro2Core) (htau : ∀ (v : A), t.τ • v = v → v = 0) : IsSelfDual_R t A

⟦prop:duality⟧, ramified simple case. A simple module with V^T = 0 is self-dual for the Roe complex. hTodd (τ odd-order) is derived (tau_powOmega2_smul_trivial); the dual A∨ inherits wild-triviality and hTodd (contragredient) and τ-fixed-point-freeness ((τ⁻¹−1) surjective); the pairing λ((1+U+U⁻¹)d) (mixedB_R_pairing_ramified, ⟦eq:pairingoperator⟧) is perfect because the operator 1+U+U⁻¹ is unipotent, hence bijective (pairingR_operator_injective) — no σ-tameness hU anywhere in this branch.

theorem GQ2.FoxH.selfDual_of_split_case_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hV₂ : ∀ (v : A), v + v = 0) (hsimple : IsSimpleModTwo C A) (hcore : t.Pro2Core) (htau : ∀ (v : A), t.τ • v = v) : IsSelfDual_R t A

Split case of a simple module (complete). When τ acts trivially, the simple module is self-dual for the Roe complex — whether σ acts nontrivially (selfDual_of_split_R) or trivially (selfDual_of_trivial_action_R). This closes the entire V^T = V branch of the tau_split_or_ramified dichotomy.

theorem GQ2.FoxH.selfDual_of_simple_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hcore : t.Pro2Core) (hV₂ : ∀ (v : A), v + v = 0) (hsimple : IsSimpleModTwo C A) : IsSelfDual_R t A

The simple case of prop_5_15_R, unconditional (⟦prop:duality⟧, "the cone of the chain map is acyclic on all simple modules"): every finite simple char-2 module at an admissible-style marking is self-dual for the Roe complex. Dispatches on the word-free tau_split_or_ramified dichotomy (reused from GQ2.DualityAssembly) — selfDual_of_split_case_R for V^T = V, selfDual_of_ramified_R for V^T = 0. This is exactly the hsimp input the dévissage induction (prop_5_15_of_simple_R) consumes.

theorem GQ2.FoxH.prop_5_15_R {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hA₂ : ∀ (a : A), a + a = 0) (hcore : t.Pro2Core) : IsSelfDual_R t A

⟦prop:duality⟧ (Candidate deformation duality), word half: the Roe word complex is self-dual for every finite elementary module — packaged: the display-(56) numerics hold on the r_R complex and the descended B_R-pairing is perfect.

The composition: the dévissage strong induction prop_5_15_of_simple_R (GQ2/Roe/DevissageInduction.lean, via lemma_5_11_R along 0 → W → A → A/W → 0 for a proper C-stable W) reduces to the simple case, which selfDual_of_simple_R closes by the tau_split_or_ramified dichotomy — split (split_shapes_of_wild_R + the tame representation-theory providers) or ramified (lemma_5_13_ramified_R + hTodd derived + the unipotent pairing operator). Γ_R twin of GQ2.FoxH.prop_5_15.

§5.17 numerics on the r_R spine

The local half prop_5_16 (GQ2/LocalLiftingDuality.lean) is word-generic — its statement and proof never mention the marking word — so it is reused verbatim (campaign convention: never clone word-free infrastructure). The corollary is therefore a thin splice.

theorem GQ2.FoxH.cor_5_17_card_R {C : Type u_1} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hcore : t.Pro2Core) (ρ : AbsGalQ2 →ₜ* C) (hρ : Function.Surjective ⇑ρ) {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction AbsGalQ2 A] [ContinuousSMul AbsGalQ2 A] (hcomp : ∀ (γ : AbsGalQ2) (a : A), γ • a = ρ γ • a) (hA₂ : ∀ (a : A), a + a = 0) [TopologicalSpace (ElemDual A)] [DiscreteTopology (ElemDual A)] [DistribMulAction AbsGalQ2 (ElemDual A)] [ContinuousSMul AbsGalQ2 (ElemDual A)] (hcompD : ∀ (γ : AbsGalQ2) (lam : ElemDual A), γ • lam = ρ γ • lam) [TopologicalSpace (ZMod 2)] [DiscreteTopology (ZMod 2)] [DistribMulAction AbsGalQ2 (ZMod 2)] [ContinuousSMul AbsGalQ2 (ZMod 2)] (htriv : ∀ (γ : AbsGalQ2) (m : ZMod 2), γ • m = m) (hpair : ∀ (γ : AbsGalQ2) (a : A) (lam : ElemDual A), ((dualEval A) (γ • a)) (γ • lam) = γ • ((dualEval A) a) lam) : Nat.card ↥(Z1wR t) = Nat.card ↥(ContCoh.Z1 AbsGalQ2 A) ∧ Nat.card (H2wR t) = Nat.card (ContCoh.H2 AbsGalQ2 A)

Corollary 5.17, numerics half, on the r_R spine (⟦prop:duality⟧, "Comparison with the local complex then uses local Tate duality as in [RT Prop. 5.16 and Cor. 5.17]"): the obstruction-space and unobstructed-lift-multiplicity cardinalities agree between the Roe word complex and the local cochain complex of G_ℚ₂. Γ_R twin of cor_5_17_card: the word side is prop_5_15_R (clauses 1–2 of IsSelfDual_R), the local side is the word-generic prop_5_16 reused verbatim (this is where axioms B6/B7 enter, exactly as for Γ_A).

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• Proposition (Candidate deformation duality) = ⟦prop:duality⟧ — selfDual_of_simple_R (the simple case: ⟦lem:normalforms⟧ + ⟦prop:hessian⟧/⟦eq:pairingoperator⟧ + R25's ⟦lem:trivial⟧ base) and prop_5_15_R (the full assembly through the dévissage induction). The local comparison sentence of its proof ("Comparison with the local complex then uses local Tate duality as in [RT Prop. 5.16 and Cor. 5.17]") is cor_5_17_card_R, splicing the word-generic prop_5_16 (reused verbatim from GQ2/LocalLiftingDuality.lean, axioms B6/B7) against prop_5_15_R.