The κ⁰ ledger for the Γ_R Gauss residue #
The Γ_R twin of GQ2/GaussZ/FinalGammaA/Kappa.lean (obligation ii.7, supply layer): the
x₁-supported section of H¹_{R,word} and the split and ramified Roe wild-value
calculations in the concrete κ⁰-extension CentExt (kappa0Cocycle dat hdat).
The gauge swap (docs/orchestration/roe-r31-survey-gaussz.md): the Γ_A normal form is
x₀-supported (![0,0,c,0], slot 2; Z¹_w-shape x 1 = x 3 = 0), while the Γ_R normal
form is x₁-supported (![0,0,0,d], slot 3; Z¹_{R}-shape x 1 = 0 ∧ x 2 = 0,
GQ2/Roe/NormalForms.lean). Accordingly the structural pack here zeroes the x₀-slot
(hx0v) where Γ_A zeroed the x₁-slot.
The word collapse. The Roe wild relator r_R = (x₀^σ)⁻¹ · a · x₁² · c (note
eq. (1.2) ⟦eq:relators⟧) is much softer than Γ_A's r_A on the x₁-supported gauge:
with x₀ ↦ 1 in the extension (zero V-part + trivial head), the first factor dies, the
ω₂-word a = (x₀⁻³τ)^{ω₂} collapses to powOmega2 τ = 1 (τ of odd tame-inertia
order), and what remains is x₁² · [x₁, x₁^{σ₂}] — the diagonal q(d) plus the V-slice
commutator polar b_q(d, σ₂⁻¹d). There is no d₀/h₀ telescope: the ramified
evaluation liftMark_kappa0_wildValueR_fib_ramified is the unconditional Wall shape
q(d) + b_q(d, σ₂⁻¹·d) — exactly FoxH.QZeroR (GQ2/Roe/Gauss.lean, ⟦eq:QR⟧) — with no
ramified hypothesis at all (the Γ_A twin needed htauf/hqg0); the split evaluation is
the corollary killing the polar term by the split σ₂-triviality hU.
The generic toolkit (sdSec, liftMark_kappa0_tameValue_fib, sdToWL/sdBaseMarking/
sdOffsets, the m-calculus, kappa0_cc_one, commP_fib_cc_one, …) is imported from
GQ2/GaussZ/FinalGammaA/Kappa.lean and reused verbatim, never cloned; only the tame
first-component peel is restated at relZPairR (relZPairR_kappa0_fst_eq_zero, a
definitional retype of liftMark_kappa0_tameValue_fib — the tame relator is shared).
All std-3; no axioms, no sorries.
The x₁-supported section of H¹_{R,word} (generic marking level) #
The note's "only x₁ varies" gauge (Lemma 4.2's normal forms, ⟦lem:normalforms⟧), as a
bijective parametrization V ≃ H¹_{R,word}: membership and bijectivity fall out of the
banked shape characterizations (lemma_5_13_split_R / lemma_5_13_ramified_R,
GQ2/Roe/NormalForms.lean; normalForm_of_shapes_R / x1Supported_mem_Z1wR_ramified,
GQ2/Roe/DualityAssembly.lean). Both regimes provide a unique x₁-supported normal form,
so one ∃!-kernel serves both — unlike the Γ_A split case, whose surjectivity had to
normalize the σ-row by hand.
The x₁-supported tuples are Roe word cocycles (split regime): immediate from the
lemma_5_13_split_R Z¹_R-shape (x 1 = 0 ∧ x 2 = 0). No σ₂-tameness hU is needed
(one fewer hypothesis than Γ_A's x0Supported_mem_Z1w_split): the Roe wild row carries no
σ₂-dependency.
The H¹_{R,word}-class equality criterion in h1wMkR vocabulary (H1wR is a
semireducible def, so the quotient lemmas do not elaborate against it directly — the
GaussZLocal.H1mk_eq_iff idiom, as for Γ_A's h1wMk_eq_iff).
The x₁-supported section of H¹_{R,word} is bijective (split regime): the unique
normal form comes from the split shapes (normalForm_of_shapes_R at lemma_5_13_split_R).
Γ_R twin of x0Section_bijective_split, minus the σ₂-tameness hU.
The x₁-supported section of H¹_{R,word} is bijective (ramified regime): the unique
normal form is lemma_5_13_ramified_R directly. Γ_R twin of
x0Section_bijective_ramified.
The κ⁰-ledger: the tame peel and the Roe wild values #
The tame relator is shared with Γ_A, so the first-component peel is the imported
liftMark_kappa0_tameValue_fib retyped at relZPairR. The Roe wild value collapses on the
x₁-supported structural pack with no telescope: see the file docstring.
The A-3 interface form at the Roe relator pair: the FIRST relator-z component
vanishes on base-slice σ/τ-slots (the tame relator is shared with Γ_A, so this is the
imported liftMark_kappa0_tameValue_fib on the nose).
The ramified Roe wild κ⁰-value is the Wall double — unconditionally (note
⟦prop:quadratic⟧/⟦eq:QR⟧): with the x₁-supported structural pack (σ/τ/x₀-slots of
zero V-part, wild cc-slots 1, τ.cc of odd order), the lifted Roe wild relator value
has fibre
q(x₁.v) + polar q x₁.v (σ₂⁻¹ • x₁.v) (σ₂ = Marking.sigma2 (sdBaseMarking tS)),
i.e. exactly FoxH.QZeroR q σ₂ (x₁.v). Unlike the Γ_A twin
(liftMark_kappa0_wildValue_fib_ramified) no ramified hypothesis enters: the word
r_R = (x₀^σ)⁻¹ · a · x₁² · c has no d₀/h₀ telescope — x₀ lifts to 1 (killing the
first factor and collapsing a to powOmega2 τ = 1 by hτodd), x₁² deposits the diagonal
q (one kappa0_cc_one step), and c = [x₁, x₁^{σ₂}] is a V-slice commutator whose fibre
is the polar form (commP_fib_cc_one).
The split Roe wild κ⁰-value is the diagonal q (note ⟦prop:quadratic⟧/⟦eq:QR⟧,
T = 1 case): the Wall double of the unconditional evaluation collapses because the split
σ₂-triviality hU kills the polar term (b_q(d, d) = 0, the alternating law from
f_polar in characteristic 2). Γ_R twin of liftMark_kappa0_wildValue_fib_split — with
the whole htau/hU-telescope pack reduced to the single hU.
Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained) #
- eq. (1.2) = ⟦eq:relators⟧ — the Roe wild relator
r_Rwhose κ⁰-fibre is evaluated here. - Lemma 4.2 = ⟦lem:normalforms⟧ — the
x₁-supported normal forms behind the section bijectionsx1Section_bijective_{split,ramified}_R. - Proposition 6.1 = ⟦prop:quadratic⟧/⟦eq:QR⟧ — the evaluated fibre is
FoxH.QZeroR's two-term shapeq(d) + b_q(d, σ₂⁻¹d)(liftMark_kappa0_wildValueR_fib_ramified), collapsing toq(d)in the split regime (liftMark_kappa0_wildValueR_fib_split).