§5.11 dévissage: the Generates bridge and Lemma 5.11

Part of the §5.11 dévissage development (split from GQ2/Devissage.lean).

The Generates bridge: H⁰w = fixedPts and IsSelfDual ↔ IsSelfDualW

For a generating marking, ker d⁰ is exactly the C-fixed points, so the word-internal package coincides with IsSelfDual. This is the precise gap between lemma_5_11 as stated (no generation hypothesis) and the dévissage selfdualW_two_of_three: the two-out-of-three for the fixedPts-form follows wherever t.Generates is available.

theorem GQ2.FoxH.H0w_eq_fixedPts {C : Type u_1} [Group C] {M : Type u_2} [AddCommGroup M] [DistribMulAction C M] (t : Marking C) (hgen : t.Generates) : ↑(H0w t) = fixedPts C M

For a generating marking, the word-complex H⁰w is the set of C-fixed points.

theorem GQ2.FoxH.isSelfDual_iff_W {C : Type u_1} [Group C] {A : Type u_3} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (hgen : t.Generates) : IsSelfDual t A ↔ IsSelfDualW t A

For a generating marking, the two self-duality packages coincide.

Lemma 5.11, fixedPts-form

The theorem GQ2.FoxH.lemma_5_11 includes the hypothesis hgen : t.Generates. Generation identifies ker d⁰ with the C-fixed points (H0w_eq_fixedPts), bridging the word-internal dévissage selfdualW_two_of_three to the fixedPts-phrased IsSelfDual; the paper's setting (admissible markings) always provides it. It lives here rather than in FoxHeisenberg.lean because the proof needs this file's machinery and the import runs the other way.

theorem GQ2.FoxH.lemma_5_11 {C : Type u_1} [Group C] [Finite C] {A : Type u_2} {A' : Type u_3} {A'' : Type u_4} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup A'] [DistribMulAction C A'] [AddCommGroup A''] [DistribMulAction C A''] [Finite A'] [Finite A] [Finite A''] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (hgen : t.Generates) (hA₂ : ∀ (a : A), a + a = 0) (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) : (IsSelfDual t A' ∧ IsSelfDual t A'' → IsSelfDual t A) ∧ (IsSelfDual t A' ∧ IsSelfDual t A → IsSelfDual t A'') ∧ (IsSelfDual t A ∧ IsSelfDual t A'' → IsSelfDual t A')

Lemma 5.11 (exact cone dévissage), stated as its consequence: along a short exact sequence of finite elementary 𝔽₂[C]-modules over a generating marking, self-duality satisfies two-out-of-three. Proved via the word-internal dévissage selfdualW_two_of_three and the Generates bridge isSelfDual_iff_W.