The r_R Fox spine: the Roe word complex and the traced mixed coordinate (Roe note §4) #
The Γ_R counterparts of the Γ_A spine objects of GQ2.FoxHeisenberg.Basic (the word complex
(30)/(31) built on the wild relator) and GQ2.FoxHeisenberg.Heisenberg (the traced mixed central
coordinate mixedB), for the Roe candidate presentation
Γ_R = ⟨σ, τ, x₀, x₁ ∣ τ^σ = τ², r_R = (x₀^σ)⁻¹ · (x₀⁻³τ)^{ω₂} · x₁² · [x₁, x₁^{σ₂}]⟩
(note eq. (1.2) ⟦eq:relators⟧, GQ2.Roe.Words). The tame relator is shared with Γ_A, so
the tame component of every object below is definitionally the Γ_A one (d1FunR_fst,
d1FunR_tame — reused, never re-proved); only the wild component changes,
Marking.wildValue → Marking.wildValueR.
Provided here, mirroring Basic.lean's names with an R suffix:
d1FunR/d1R— the note §4 differential "obtained by differentiating the two relators" (Proposition 4.1 ⟦prop:jacobian⟧, display ⟦eq:jacobian⟧):d1FunR t x = ((liftMarking t x).tameValue.u, (liftMarking t x).wildValueR.u). Additivity (d1FunR_add) is proved by functoriality fromMarking.map_tameValue/map_wildValueRexactly asd1Fun_add; the complex identityd1FunR_comp_d0forwards the twoΓ_Rrelations through the inner-automorphism coboundary lift exactly asd1Fun_comp_d0.- the
R-word complexH0wR/Z1wR/B1wR/H1wR/H2wRwith the chain inclusionB1wR_le_Z1wR(H0wR/B1wRare definitionally the sharedH0w/B1w—d⁰does not see the relator;H0wR_eq_H0w,B1wR_eq_B1w). mixedB_R— the traced mixed central coordinate at the Heisenberg lift,tameValue.z + wildValueR.z(mirroringmixedB,GQ2/FoxHeisenberg/Heisenberg.lean:312), with its free-word bridgebridge_wildR(the naturality route:wildValueExpRcarries noω₂, so it pushes throughstokesEvalunconditionally — theΓ_Rtwin ofbridge_wild) and the bilinearitymixedB_R_add_left/right,mixedB_R_zero_left/rightported fromGQ2.MixedBilinear. The cocycle closed form (the note's scalar Gram⟨(a,c,d),(a',c',d')⟩ = ac' + ca' + dd', ⟦eq:scalarform⟧) is ticket R25's, not here.
The evaluated closed forms of the wild row (⟦prop:jacobian⟧'s L_w = Pb + (P + S⁻¹)c) are in
GQ2.Roe.WildRow.
The R-word complex (the (30)/(31) clone on the Roe wild relator) #
d¹_R, function level (note §4, the differential of display ⟦eq:jacobian⟧): the pair of
A-coordinates of the evaluated tame and Roe wild relators at the lifted marking — the
Γ_R counterpart of d1Fun. The tame component is identical to Γ_A's (d1FunR_fst).
Equations
- GQ2.FoxH.d1FunR t x = ((GQ2.FoxH.liftMarking t x).tameValue.u, (GQ2.FoxH.liftMarking t x).wildValueR.u)
Instances For
Stress test (shared tame row). The tame component of d1FunR is definitionally the
Γ_A one — the tame relator is shared, so the Γ_A tame-row lemmas (d1Fun_tame,
d1Fun_tame_split) apply verbatim through this equation.
The wild component of d1FunR, in relator form (the input to GQ2.Roe.WildRow's rows).
The tame row of d¹_R, in closed form — Γ_A's d1Fun_tame, reused (not re-proved):
the note's "The tame row is unchanged from [RT (5.5)]", L_t = S⁻¹(1+T)a + (S⁻¹+1+T)b.
d¹_R is additive in the lift variables — the finite Fox rules for the Roe word, proved
by functoriality exactly as d1Fun_add: evaluate the relators over the coefficient module
A × A, then push through the three C-equivariant maps fst, snd, fst + snd : A × A →+ A
(Marking.map_tameValue/Marking.map_wildValueR + WordLift.map).
d¹_R bundled on d1FunR_add (finite coefficients, per d1FunR_add).
Equations
- GQ2.FoxH.d1R t = AddMonoidHom.mk' (GQ2.FoxH.d1FunR t) ⋯
Instances For
The Roe complex is a complex: d¹_R ∘ d⁰ = 0 at a marking satisfying the two Γ_R
relations. Proof exactly as d1Fun_comp_d0: liftMarking t (d0 t v) is t pushed through
g ↦ ⟨g•v − v, g⟩ = ⟨v,1⟩⁻¹⟨0,g⟩⟨v,1⟩, so its relator values are conjugates of t's — which
are 1 by TameRel/WildRelR — hence have zero A-coordinate.
H⁰_{R,ρ}(A) = ker d⁰. The relator does not enter d⁰, so this is the shared H0w
(H0wR_eq_H0w); the R-name exists for the Roe complex's uniform API.
Equations
- GQ2.FoxH.H0wR t = (GQ2.FoxH.d0 t).ker
Instances For
Z¹_{R,ρ}(A) = ker d¹_R (the Roe degree-one cocycles).
Equations
- GQ2.FoxH.Z1wR t = (GQ2.FoxH.d1R t).ker
Instances For
B¹_{R,ρ}(A) = im d⁰ — again relator-free, = B1w (B1wR_eq_B1w).
Equations
- GQ2.FoxH.B1wR t = (GQ2.FoxH.d0 t).range
Instances For
The chain inclusion B¹ ≤ Z¹_R under the Γ_R relations (mirrors B1w_le_Z1w,
GQ2/Devissage/Naturality.lean).
H¹_{R,ρ}(A) (as for H1w: the addSubgroupOf-quotient is total — the chain inclusion
B¹ ≤ Z¹_R is B1wR_le_Z1wR, needed only for lemmas).
Equations
- GQ2.FoxH.H1wR t = (↥(GQ2.FoxH.Z1wR t) ⧸ (GQ2.FoxH.B1wR t).addSubgroupOf (GQ2.FoxH.Z1wR t))
Instances For
The class of a degree-one Roe cocycle in H¹_{R,ρ}.
Equations
- GQ2.FoxH.h1wMkR t x = ↑x
Instances For
H²_{R,ρ}(A) = A² ⧸ im d¹_R.
Equations
- GQ2.FoxH.H2wR t = ((A × A) ⧸ (GQ2.FoxH.d1R t).range)
Instances For
B_{R,ρ,A}: the traced mixed central coordinate of the Γ_R word — the sum of the
central coordinates of the two evaluated relators (not the central coordinate of their product),
mirroring mixedB (GQ2/FoxHeisenberg/Heisenberg.lean:312) with wildValue → wildValueR.
Its cocycle closed form — the note's scalar Gram ⟦eq:scalarform⟧, with the honest diagonal dd'
in place of Γ_A's opaque ω₂-scalar — is ticket R25's mixedB_cocycle_R.
Equations
- GQ2.FoxH.mixedB_R t x y = (GQ2.FoxH.heisMarking t x y).tameValue.z + (GQ2.FoxH.heisMarking t x y).wildValueR.z
Instances For
Wild bridge for the Roe word: the Roe wild relator value at heisMarking equals the
free-word evaluation stokesEval … (wildValueExpR freeMarking e) at the target-dependent
exponent e = omega2Exp (exponent H(A)⋊C) — the Γ_R analogue of bridge_wild. Proof:
wildValueExpR_eq_wildValueR trades the two ω₂-powers for the explicit exponent inside the
finite group H(A)⋊C, and wildValueExpR_map (no ω₂, hence no finiteness) pulls the word
back along the classifying hom stokesEval (markVec t) x y. This is the naturality lemma
feeding the Stokes rows (ticket R23) and the bilinearity below.
mixedB_R is additive in the primal offsets x (ported from mixedB_add_left,
GQ2/MixedBilinear.lean, with bridge_wild → bridge_wildR).
Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained) #
- Proposition 4.1 (Evaluated Jacobian) = ⟦prop:jacobian⟧ — this file supplies the differential
d1FunR/d1Rand the complexH0wR/Z1wR/B1wR/H1wR/H2wR; the evaluated rows are inGQ2.Roe.WildRow(display ⟦eq:jacobian⟧). - Lemma 4.3 (Trivial coefficient) = ⟦lem:trivial⟧ — the scalar Gram ⟦eq:scalarform⟧ on
mixedB_Ris ticket R25 (mixedB_cocycle_R); this file has only the definition, the free-word bridgebridge_wildR, and the bilinearity. - Lemma 5.1 = ⟦lem:stokes⟧ — the endpoint computation on
bridge_wildR's free word isexpMod2_wildValueExpR(GQ2/Roe/Stokes.lean, ticket R23); the traced Stokes rows (mixedB_wildRow_R,prop_5_8_*_R) should consumebridge_wildRfrom here.