Documentation

GQ2.Roe.Devissage

§5.11 dévissage on the r_R spine: two-out-of-three for IsSelfDual_R #

Mechanical R-spine clone hub, mirroring GQ2/Devissage.lean (campaign decision, docs/orchestration/roe-r20-recon.md). lemma_5_11_R (bottom of GQ2/Roe/Devissage/GeneratesBridge.lean) is the two-out-of-three property of IsSelfDual_R along a short exact sequence of finite elementary 𝔽₂[C]-modules, proved via the long exact cohomology sequence of the Roe word complex C_R(A) : A --d⁰--> A⁴ --d¹_R--> A² exactly as the Γ_A capstone.

The proofs port verbatim onto the r_R spine (they only forward hw : t.WildRelR and use d¹_R∘d⁰ = 0, functoriality, the LES, and finite linear algebra — never unfolding the aux words); the elementary-dual pack (GQ2.Devissage.ElemDualPack) and every (A)-classified helper are reused from GQ2.Devissage.*, never cloned. The traced-row seams prop_5_8_*_R/lemma_5_6_R (nominally ticket R23) are provided in GQ2.Roe.Devissage.TracedRows.