**Lemma 5.2, core cancellation.**  If the commutator `k = [A,B]` (`commP` convention
`A⁻¹B⁻¹AB`) is central and satisfies `k² = 1`, and `B⁴ = 1`, then `A·B·B²·[A,B] = B⁻¹·A`.
This is display (32) after cancelling the common prefix `ϕ(X)·X` (with `A = ϕ(D)`, `B = D`).

The proof is the paper's: from `A·B = B·A·k` (`hcomm`), `k` central and `k² = 1` give that `A`
commutes with `B²`, and `B³ = B⁻¹`; then `A·B·B²·k = B·A·B² = B³·A = B⁻¹·A`.  The associativity
bookkeeping is discharged by right-normalising with `simp only [mul_assoc, …]`, feeding the
commutator relation in the right-associated form `A·(B·x) = B·(A·(k·x))` so it fires under the
normal form. 

**Lemma 5.2, display (32)**: `h_ϕ(X,D) = ϕ(X)·X·ϕ(D)·D·D²·[ϕ(D),D] = ϕ(X)·X·D⁻¹·ϕ(D)`,
whenever `[ϕ(D),D]` is central of order ≤ 2 and `D⁴ = 1`.  (`ϕ` need not be a homomorphism for the
identity; the paper's `ϕ` is a `Z`-fixing automorphism, which is what makes the hypotheses hold for
the actual `h₀`.) 

**Lemma 5.2(ii)**: when `ϕ = id`, `h_ϕ(X,D) = X²` for every `D` (`[D,D] = 1`).  Used in the
split (`P = 1`) branch of the `h₀`-shadow, where `g₀ = σ₂²` acts trivially. 

**Lemma 5.6 (strict coefficient naturality)**, in the traced form Prop 5.10 uses: for an
equivariant `f : A → A'`, `B_{A'}(f∗x, y') = B_A(x, f^∨ y')`.

Proof (the paper's "evaluate in the mixed Heisenberg group"): the two markings live in
`H(A') ⋊ C` and `H(A) ⋊ C`, related by `f` on the `A`-slot and `f^∨` on the dual slot.  They both
sit inside the **mixed subgroup** `S ≤ H(A') ⋊ C × H(A) ⋊ C` cut out by "`f`-related `a`/`λ`,
equal `z`, equal `g`" — a subgroup precisely because `f` is `C`-equivariant.  The two projections
`π₁, π₂ : S →* …` carry the mixed marking to the two sides (`Marking.map_tameValue`/`map_wildValue`,
the latter needing `S` finite for the `ω₂`-powers), and `S`'s defining `z`-equation makes the two
relator `z`-coordinates agree — which is exactly the claim.

(Requires `A`, `A'`, `C` finite, the paper's finite setting: `map_wildValue`'s `ω₂` push needs the
source group finite.) 

**Lemma 5.7, display (38)**: for a word `r` with trivial lower value, evaluating at the
generic coboundary `x = d⁰a = ((cᵢ−1)a)ᵢ` gives
`β_r(d⁰a, y) = ⟨a, L^{A^∨}_r(y)⟩ + Σᵢ εᵢ(r)·yᵢ(cᵢa)`. 

**Lemma 5.7, display (39)**: the dual-variable form,
`β_r(x, d⁰λ) = ⟨L^A_r(x), λ⟩ + Σᵢ εᵢ(r)·λ(xᵢ)`.  (The lower-value hypothesis `hr` is recorded for
symmetry with the left form; the dual central defect is `g`-independent, so it is not needed
here.) 

**Prop 5.8, display (41)** (= chain identity (47) of Prop 5.10 under the canonical
identifications): `B_{ρ,A}(d⁰a, y) = ⟨a, L^{A^∨}_t(y) + L^{A^∨}_w(y)⟩`, where the dual
first relation differentials are `d1Fun` on `A^∨`.

The proof follows the paper's statement on p. 17.  The tame summand is
`mixedB_tameRow` — `⟨a, L^{A^∨}_t(y)⟩ + y_τ(τ·a)` (tame ε-vector `(0,1,0,0)`, `expMod2_fgTame`);
the wild summand comes from `bridge_wild` + `lemma_5_7_left` with ε-vector
`(0, e, 0, e+1) = (0,1,0,0)` at the odd `ω₂`-representative (`expMod2_wildValueExp`), i.e.
`⟨a, L^{A^∨}_w(y)⟩ + y_τ(τ·a)`; the two `y_τ(τ·a)` corrections cancel (char 2), which is exactly
condition (40) for the `(1,1)` trace.  (An earlier apparent inconsistency here was a repo-side
`h₀` transcription bug, resolved — see `docs/erratum-h0-transcription.md`.) 

**Prop 5.8, display (42)** (= chain identity (48)): `B_{ρ,A}(x, d⁰λ) = ⟨L_t(x)+L_w(x), λ⟩`.
Proved as stated: `mixedB = tameRow + wildRow`, and the two `λ(x_τ)` corrections cancel (char 2). 

**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`. 

**Lemma 5.11, word-internal form (exact-cone dévissage)**: two-out-of-three for
`IsSelfDualW` along the module SES.  Proof: translate each `IsSelfDualW` into
`χ`-bijectivities (`isSelfDualW_iff`, `chi_bij_of_selfdualW`), then chase the duality ladder —
nine four-lemma windows across the two LESs (word complex of the SES, and of its dualization)
tied by the `lemma_5_6`-squares, the evaluation squares and the δ-squares. 

**Lemma 5.12 (simple characteristic-two modules are tame)**: a normal 2-subgroup `L ◁ C`
acts trivially on every simple `𝔽₂[C]`-module.  Proof: the `L`-fixed subspace is nonzero (the
`p`-group congruence `#V ≡ #Vᴸ (mod 2)` with `#V` even) and `C`-stable (`L` normal), so
simplicity forces it to be all of `V`.  (Proved for the §5 proof layer, as part of the Heisenberg
word-evaluation core — `d1Fun_add`, `d1Fun_comp_d0`, Lemma 5.6, Lemma 5.7 both forms, and the
tame row of Prop 5.8; the *wild row* (Prop 5.8/Lemma 5.13, needing the target-dependent
integer-`ω₂` representative of the wild word) and the mapping-cone dévissage Lemma 5.11
followed later in the §5 proof layer and are also proved.) 

**Lemma 5.13, split case (i), cocycle shape**: if `T = 1` (trivial `τ`-action on a
nontrivial simple module), `Z¹ = {(a, 0, c, 0)}` and `B¹ = {((S−1)v, 0, 0, 0)}`.

Hypotheses (per `docs/orchestration/p13-normal-form-hypothesis-gap.md`): `hcore` supplies trivial wild action
(`wild_acts_trivially`); `hVS` is `V^S = 0`, i.e. `1 + S⁻¹` invertible — it excludes the trivial
module `𝔽₂` (where `1 + S⁻¹ = 0` and the `x 3 = 0` clause would fail; that module is handled
separately in `prop_5_15`).  `hU` is the σ-tameness (`σ₂ = U` acts trivially).  Both `hVS` and `hU`
are *derivable* in the split case — with `τ, x₀, x₁` acting trivially the `C`-action factors through
the cyclic `⟨σ̄⟩`, so a nontrivial simple `V` is a simple `𝔽₂[⟨σ⟩]`-module: `V^S = V^C = 0` and `σ`
has odd order (⇒ `σ₂ = 1`).  Those derivations need `t.Generates` and simple-cyclic rep theory, so
they are factored out as hypotheses here, keeping the normal-form proof pure finite-Fox calculus.
See `docs/orchestration/p13-normal-form-hypothesis-gap.md` §7.

Proved (the §5 proof layer): `B¹` half from `b1w_split_shape`; `Z¹` half from the tame row `d1Fun_tame_split`
(`= S⁻¹·x₁`) and the wild row `liftMarking_wildValue_u` (`= x₁ + (1+S⁻¹)·x₃`), with `x 1 = 0` from
`S⁻¹` injective and `x 3 = 0` from `hVS`. 

**Lemma 5.13, ramified case (ii), unique normal form**: if `V^T = 0`, every degree-one
class has a unique representative supported on `x₀` (display (53)).

Hypothesis `hcore` supplies trivial wild action (`wild_acts_trivially`); the ramified condition
`V^T = 0` (`htau`) gives `1 + T` invertible.

**Hypothesis `hTodd`**: `τ`'s 2-primary part `powOmega2 t.τ` acts
trivially on `V`, i.e. `τ` acts with *odd* order on `V`.  This is the ramified analogue of the
split case's `hU : ∀ v, t.sigma2 • v = v` (`sigma2 = powOmega2 t.σ`), and is the arithmetic fact
that `τ = ` tame inertia is prime-to-2, so acts through an odd quotient on the `𝔽₂`-module `V`.
It is **required** (not implied by `V^T = 0`, which admits even-order fixed-point-free actions):
the wild-row aux offset `(powOmega2 p).u` is a geometric sum whose length is the `ω₂`-exponent,
and it collapses to `0` (via the `P = 0` norm ledger `WordLift.norm_eq_zero_of_fixedPointFree`)
exactly because the odd action-period divides that length.  Like `hU`/`hVS` in the split case,
this is factored out as an explicit hypothesis, supplied by the simple-factor analysis.
See `docs/orchestration/p13-normal-form-hypothesis-gap.md` for the counterexample and rationale.

**Signature note**: the trivial wild action is taken as hypotheses
`hx0`/`hx1` rather than derived from `(hsimple, hcore)` via `wild_acts_trivially` — so the lemma
applies to the contragredient dual `A∨` (whose wild-triviality transfers from `A`'s) without a
"dual of simple is simple" detour, mirroring the split-side `split_shapes_of_wild`.

No `hU` hypothesis is needed: the σ-tameness `∀ v, σ₂ • v = v` is *not derivable from
admissibility* (`S₃` on its 2-dim simple module and `C₅⋊C₄` on `𝔽₁₆`, markings `x₀=x₁=1`,
are admissible ramified counterexamples), and it is not needed: the `h₀`-row `x₂`-cancellation
happens in `g₀`-conjugate pairs (`liftMarking_h0_u_ramified`, via `conjP_u_of_base_trivial`). 

**Lemma 5.13, pairing display (54), split case**: on `x₀`-supported representatives the
degree-one pairing is `(c, λ) ↦ λ(c)` when `T = 1`.

The proof uses the mixed Hessian ledger, Lemma 5.14 — `h₀ ↦ λ(c)` via
`classTwoIdentity` [needs `g₀ = σ₂²` trivial, i.e. `hU`], and the `[d₀,z₀]` term vanishes since
`P + 1 = 0` in char 2 for `T = 1`.  `hsimple`/`hcore` give the trivial wild action
(`wild_acts_trivially`); `hU` is the σ-tameness (derivable in split; see `lemma_5_13_split`). 

**Lemma 5.13, pairing display (54), ramified case**: when `V^T = 0` the pairing on
`x₀`-supported representatives is `(c, λ) ↦ λ((1 + U + U⁻¹)c)` for `U = S₂^ω`
(`Marking.sigma2`).

The tame relator's central coordinate vanishes on the x₀-supported rep
(`heisMarking_tameValue_z_eq_zero`), so the pairing is carried entirely by the wild relator
(`heisMarking_wildValue_z_ramified`): `h₀ ↦ λ(c)` (the shadow) plus the `[d₀,z₀]` symplectic term
`λ(Uc) + λ(U⁻¹c)` (nonzero here because `Dd₀ = c ≠ 0`, unlike the split `P + 1 = 0` collapse).

**Hypothesis `hTodd`** (added the §5 proof layer, mirroring the §5 proof layer's `lemma_5_13_ramified`): `τ`'s 2-primary part
acts trivially on `V` (tame inertia is prime-to-2), needed for the ramified `Dd₀ = c` via the
`P = 0` ledger.  Supplied per simple factor by the tame representation-theory proof.  The trivial wild action is taken as
hypotheses `hx0`/`hx1` (the Prop. 5.15 proof signature note on `lemma_5_13_ramified`).