The χ-twisted crossed-derivation calculus for r₂ (Roe note §3.2, ⟦prop:orientation⟧)

Statements final (ticket R7); proofs filled (ticket R9) — sorry-free. The last piece, isLabuteOrientation_ext, uses R8's dr_hom_ext (GQ2/Roe/DRAbelianization.lean); its density step was stitched in by the orchestrator once R8 landed (R9 had recorded the finished proof at the former sorry).

Labute's characterization of the canonical Demushkin orientation ([Labute], Théorème 4; note Prop. 3.3 ⟦prop:orientation⟧): for a character χ of the free pro-2 group, a crossed derivation into the rank-one module ℤ₂(χ) satisfies

D(gh) = Dg + χ(g)·Dh, D(g⁻¹) = −χ(g)⁻¹·Dg,

and such derivations descend through the relation precisely when D(r₂) = 0 for arbitrary values of Ds, Dx, Dy. The canonical orientation is the unique χ with this property.

Realization: WordLift ℤ₂ ℤ₂ˣ

A pair (character value, derivation value) is a point of the lift group ℤ₂(χ) ⋊ ℤ₂ˣ = FoxH.WordLift ℤ_[2] ℤ_[2]ˣ (GQ2/FoxHeisenberg/Basic.lean:76, with A = ℤ₂ a C = ℤ₂ˣ-module via unit multiplication — Mathlib's Units scalar action), whose multiplication (u, g)(v, h) = (u + g•v, gh) is the crossed-derivation product rule and whose inverse is the inverse rule. Assigning the generators s, x, y ↦ (Ds, S), (Dx, X), (Dy, Y) therefore extends (uniquely) to the free group, and the value of the extension on r₂ is literally drWord ⟨Ds, S⟩ ⟨Dx, X⟩ ⟨Dy, Y⟩: its .u-component is D(r₂) and its .g-component is χ(r₂). "Every crossed derivation kills r₂, and χ kills r₂" is the single equation

∀ Ds Dx Dy, drWord ⟨Ds, S⟩ ⟨Dx, X⟩ ⟨Dy, Y⟩ = 1 (IsLabuteOrientationDatum).

The four equations

Evaluating (drWord_wordLift) and collecting coefficients produces the note's ⟦eq:charrelation⟧/⟦eq:Cx⟧/⟦eq:Cs⟧/⟦eq:Cy⟧: the base component gives the character relation Y² = X⁴ (3.9), and the offset component is csR·Ds + cxR·Dx + cyR·Dy with the coefficient functions below. cxR is the note's (3.10) verbatim; csR/cyR are the raw (pre-descent) forms, which reduce to the note's (3.11)/(3.12) after substituting Y² = X⁴ (X⁻⁴(Y−1)² = (Y−1)²/Y² and X⁻⁴(Y−1) = Y⁻¹(1−Y⁻¹)); the raw forms are what the word evaluation literally produces, so they are the right statement-final normal forms here.

Solution ⟦eq:orientationvalues⟧

Branch Y = X² is excluded ((X−1)(X²−X−1) = 0 with the second factor odd forces X = 1, then Cy = 2 ≠ 0); on Y = −X² the system reduces to the cubic X³ + 2X² + 1 = 0 with S·(X²+X+1) = −X³, and Cy becomes automatic (Cy = (X+1)(X³+2X²+1)/X⁷). The Hensel root X ≡ 5 (mod 16), S ≡ 13 (mod 16) and the induced im χ_R = {±1}×(1+4ℤ₂) are ticket R10/R11 content (GQ2/Roe/OrientationRoot.lean); the existence/uniqueness statements here consume the root facts as hypotheses whose shapes match R10's planned rootX_spec/Sval_spec exactly, so no import of the (parallel) R10 file is needed.

All numerics were independently re-derived and 2-adically checked in the R2 spike (docs/orchestration/roe-r2-spike.md §2): symbolic descent system, branch exclusion, X ≡ 2997 (mod 2¹²), and Cx = Cs = Cy = 0 exactly at the root.

The crossed-derivation evaluation of the atomic factors

theorem GQ2.conjP_wordLift (S X : ℤ_[2]ˣ) (Ds Dx : ℤ_[2]) : conjP { u := Dx, g := X } { u := Ds, g := S } = { u := ↑S⁻¹ * Dx + ↑S⁻¹ * (↑X - 1) * Ds, g := conjP X S }

Conjugation rule (note §3.2, first display): in the lift group ℤ₂(χ) ⋊ ℤ₂ˣ, x^s at the lifts (Dx, X), (Ds, S) has derivation component D(x^s) = S⁻¹·Dx + S⁻¹(X−1)·Ds.

theorem GQ2.commP_wordLift (Gv Hv : ℤ_[2]ˣ) (Dg Dh : ℤ_[2]) : commP { u := Dg, g := Gv } { u := Dh, g := Hv } = { u := ↑Gv⁻¹ * (↑Hv⁻¹ - 1) * Dg + ↑Hv⁻¹ * (1 - ↑Gv⁻¹) * Dh, g := commP Gv Hv }

Commutator rule ⟦eq:commderivative⟧ (note (3.8)): for lifts with character values G, H, D[g,h] = G⁻¹(H⁻¹−1)·Dg + H⁻¹(1−G⁻¹)·Dh.

The three coefficient functions

noncomputable def GQ2.cxR (S X : ℤ_[2]ˣ) : ℤ_[2]

The Dx-coefficient of D(r₂) — note ⟦eq:Cx⟧ (3.10), verbatim: −(X⁻¹S⁻¹ + X⁻² + X⁻³ + X⁻⁴).

Equations

• GQ2.cxR S X = -(↑X⁻¹ * ↑S⁻¹ + ↑X⁻¹ ^ 2 + ↑X⁻¹ ^ 3 + ↑X⁻¹ ^ 4)

noncomputable def GQ2.csR (S X Y : ℤ_[2]ˣ) : ℤ_[2]

The Ds-coefficient of D(r₂) — note ⟦eq:Cs⟧ (3.11) in raw (pre-descent) form: S⁻¹·(−X⁻¹(X−1) + X⁻⁴(Y−1)²). The note displays (Y−1)²/Y² for the second summand, which is this expression after the character relation Y² = X⁴ ⟦eq:charrelation⟧; the raw form is what the word evaluation (drWord_wordLift) literally produces.

Equations

• GQ2.csR S X Y = ↑S⁻¹ * (-(↑X⁻¹ * (↑X - 1)) + ↑X⁻¹ ^ 4 * (↑Y - 1) ^ 2)

noncomputable def GQ2.cyR (S X Y : ℤ_[2]ˣ) : ℤ_[2]

The Dy-coefficient of D(r₂) — note ⟦eq:Cy⟧ (3.12) in raw (pre-descent) form: X⁻⁴·((1+Y) + (Y−1)(S⁻¹−1)). The note displays the second summand as Y⁻¹(1−Y⁻¹)(S⁻¹−1) (no X⁻⁴), which is this expression after Y² = X⁴ ⟦eq:charrelation⟧.

Equations

• GQ2.cyR S X Y = ↑X⁻¹ ^ 4 * (1 + ↑Y + (↑Y - 1) * (↑S⁻¹ - 1))

The r₂-evaluation identity

theorem GQ2.drWord_wordLift (S X Y : ℤ_[2]ˣ) (Ds Dx Dy : ℤ_[2]) : drWord { u := Ds, g := S } { u := Dx, g := X } { u := Dy, g := Y } = { u := csR S X Y * Ds + cxR S X * Dx + cyR S X Y * Dy, g := (X ^ 4)⁻¹ * Y ^ 2 }

The r₂-evaluation identity (note §3.2, "collecting the three free coefficients") — the master computation from which ⟦eq:charrelation⟧/⟦eq:Cx⟧/⟦eq:Cs⟧/⟦eq:Cy⟧ are read off: evaluating the Roe relator word at the crossed-derivation lifts s ↦ (Ds, S), x ↦ (Dx, X), y ↦ (Dy, Y) in ℤ₂(χ) ⋊ ℤ₂ˣ gives derivation component csR·Ds + cxR·Dx + cyR·Dy and character component X⁻⁴Y².

Fill (R9): expand via conjP_wordLift/commP_wordLift, WordLift.mul_u/pow_u, then ring; the base component is drWord_comm in ℤ₂ˣ.

The Labute descent condition

def GQ2.IsLabuteOrientationDatum (S X Y : ℤ_[2]ˣ) : Prop

The Labute descent condition on character values ⟦prop:orientation⟧: (S, X, Y) is a Labute orientation datum for the Roe relator if the lifted word dies for every choice of derivation generator-values — equivalently (isLabuteOrientationDatum_iff): the character kills r₂ (base component, ⟦eq:charrelation⟧) and every crossed derivation into ℤ₂(χ) kills r₂ (offset component, ⟦eq:Cx⟧/⟦eq:Cs⟧/⟦eq:Cy⟧). This is Labute's characterization of the descent of crossed derivations through the relation ([Labute], Théorème 4; note Prop. 3.3).

Equations

• GQ2.IsLabuteOrientationDatum S X Y = ∀ (Ds Dx Dy : ℤ_[2]), GQ2.drWord { u := Ds, g := S } { u := Dx, g := X } { u := Dy, g := Y } = 1

def GQ2.IsLabuteOrientation (χ : ↑DR.toProfinite.toTop →* ℤ_[2]ˣ) : Prop

A Labute orientation of D_R ⟦prop:orientation⟧: a character χ : D_R → ℤ₂ˣ whose generator values form a Labute orientation datum. (House style for ℤ₂ˣ-valued characters — MonoidHom plus a separate continuity hypothesis where needed — follows DyadicOrientation.chiTwo and prop_3_8_classification.) The note's χ_R is the unique such character (isLabuteOrientation_ext); its construction from the Hensel root is ticket R11.

Equations

• GQ2.IsLabuteOrientation χ = GQ2.IsLabuteOrientationDatum (χ GQ2.drS) (χ GQ2.drX) (χ GQ2.drY)

theorem GQ2.isLabuteOrientationDatum_iff (S X Y : ℤ_[2]ˣ) : IsLabuteOrientationDatum S X Y ↔ Y ^ 2 = X ^ 4 ∧ cxR S X = 0 ∧ csR S X Y = 0 ∧ cyR S X Y = 0

Extraction of the four equations ⟦eq:charrelation⟧/⟦eq:Cx⟧/⟦eq:Cs⟧/⟦eq:Cy⟧: the Labute descent condition holds iff the character relation Y² = X⁴ holds and the three coefficients vanish.

Fill (R9): rewrite by drWord_wordLift; forward direction plugs the three coordinate vectors (1,0,0), (0,1,0), (0,0,1) into the derivation values; backward is linearity.

Existence and uniqueness of the solution ⟦eq:orientationvalues⟧

The root facts are consumed as hypotheses whose shapes match ticket R10's planned GQ2/Roe/OrientationRoot.lean interface (rootX/rootX_spec, Sval/Sval_spec, uniqueness of the unit root) — see the R7 design memo §R10 for the name map.

theorem GQ2.isLabuteOrientationDatum_of_root (X S Y : ℤ_[2]ˣ) (rootX_spec : ↑X ^ 3 + 2 * ↑X ^ 2 + 1 = 0) (Sval_spec : ↑S * (↑X ^ 2 + ↑X + 1) = -↑X ^ 3) (hY : ↑Y = -↑X ^ 2) : IsLabuteOrientationDatum S X Y

Existence ⟦eq:orientationvalues⟧: given a unit root X of Z³ + 2Z² + 1 (R10's rootX_spec), the unit S with S·(X²+X+1) = −X³ (R10's Sval_spec; the denominator is a unit, note ⟦eq:SfromX⟧), and Y = −X², the triple (S, X, Y) is a Labute orientation datum.

Fill (R9, pure ring-level algebra from isLabuteOrientationDatum_iff): the character relation is (−X²)² = X⁴; Cx·(−S X⁴) = X³ + 2X² + 1 − (X³ + X² + X)·(1 + S⁻¹X⁻¹·…)-style clearing reduces Cx = 0 to Sval_spec, Cs = 0 to the cubic, and Cy to the identity Cy·X⁷ = (X+1)(X³+2X²+1) (automatic; R2 spike §2.1).

theorem GQ2.isLabuteOrientationDatum_solution {S X Y : ℤ_[2]ˣ} (h : IsLabuteOrientationDatum S X Y) : ↑X ^ 3 + 2 * ↑X ^ 2 + 1 = 0 ∧ ↑Y = -↑X ^ 2 ∧ ↑S * (↑X ^ 2 + ↑X + 1) = -↑X ^ 3

Solution extraction ⟦eq:orientationvalues⟧: any Labute orientation datum satisfies Y = −X², the cubic X³ + 2X² + 1 = 0, and S·(X²+X+1) = −X³ (the multiplicatively cleared form of ⟦eq:SfromX⟧ S = −X³/(X²+X+1)).

Fill (R9/R10): via isLabuteOrientationDatum_iff. Y = ±X² since ±1 are the only square roots of 1 in ℤ₂ˣ; the branch Y = X² is excluded — clearing denominators in Cs = 0 gives (X−1)(X²−X−1) = 0 with the second factor odd, so X = 1, and then Cy = 2 ≠ 0 (note Prop. 3.3, proof). On Y = −X² the equation Cs = 0 clears to the cubic.

theorem GQ2.isLabuteOrientationDatum_unique (rootX_unique : ∀ (a b : ℤ_[2]ˣ), ↑a ^ 3 + 2 * ↑a ^ 2 + 1 = 0 → ↑b ^ 3 + 2 * ↑b ^ 2 + 1 = 0 → a = b) {S X Y S' X' Y' : ℤ_[2]ˣ} (h : IsLabuteOrientationDatum S X Y) (h' : IsLabuteOrientationDatum S' X' Y') : S = S' ∧ X = X' ∧ Y = Y'

Uniqueness of the datum, relative to uniqueness of the unit root of the cubic (the Hensel-uniqueness fact supplied by R10; consumed here as the hypothesis rootX_unique): two Labute orientation data coincide.

Fill (R11): both satisfy isLabuteOrientationDatum_solution; rootX_unique forces X = X', then Y = −X² forces Y = Y' and S·(X²+X+1) = −X³ forces S = S' (the factor X²+X+1 is odd, hence a unit, and Units.ext applies).

theorem GQ2.isLabuteOrientation_ext (rootX_unique : ∀ (a b : ℤ_[2]ˣ), ↑a ^ 3 + 2 * ↑a ^ 2 + 1 = 0 → ↑b ^ 3 + 2 * ↑b ^ 2 + 1 = 0 → a = b) {χ χ' : ↑DR.toProfinite.toTop →* ℤ_[2]ˣ} (hχ : Continuous ⇑χ) (hχ' : Continuous ⇑χ') (h : IsLabuteOrientation χ) (h' : IsLabuteOrientation χ') : χ = χ'

Uniqueness at the character level: two Labute orientations of D_R agree — they agree on the generators by isLabuteOrientationDatum_unique, hence everywhere by topological generation of D_R by s, x, y (the generation lemma is ticket-R8 infrastructure; continuity of both characters is required for the density argument).

Stress test

theorem GQ2.not_isLabuteOrientationDatum_one : ¬IsLabuteOrientationDatum 1 1 1

Stress test (the trivial character is not a Labute orientation datum): at (S, X, Y) = (1, 1, 1) the derivation values (0, 0, 1) give D(r₂) = 2 ≠ 0 — the y²-factor contributes (1 + Y)·Dy = 2 and everything else vanishes. (This is the same Cy = 2 obstruction that kills the excluded branch at X = 1.)

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

• Prop 3.3 = ⟦prop:orientation⟧
• eq. (3.3)/(3.9) = ⟦eq:orientationvalues⟧/⟦eq:charrelation⟧
• eq. (3.8) = ⟦eq:commderivative⟧
• eq. (3.10)–(3.12) = ⟦eq:Cx⟧/⟦eq:Cs⟧/⟦eq:Cy⟧
• eq. (3.13) = ⟦eq:SfromX⟧