The (136) R-stage for Γ = Γ_A #
Mirror of GQ2/RStageLocal.lean at the candidate source Γ_A, per docs/orchestration/p16d6e5-plan.md.
The local file counts Z¹(G_ℚ₂, R) with prop_5_16's card_Z1_eq (B6/B7); here the same
counts come from the candidate duality prop_5_15 (IsSelfDual) through the word-complex
bridge z1Equiv : Z1 GA A ≃+ Z1w (markC ρ) (WordCohBridge) — no B-axioms on the word side.
Main results (route of record: docs/orchestration/p16d6e5-plan.md):
htriv_gammaA— the trivialΓ_A-action on𝔽₂(registered here as the canonical trivialDistribMulAction GammaA (ZMod 2);γ • m = mis thenrfl);hZcount_gammaA—#RCocycle = z_Rviaz1Equiv+prop_5_15clause 2 +blockRChar_card;hsep_hom_gammaA— the(R^∨)^C-separation via the marking-level lifting argument (L1–L5 of the plan; the trace-span package isprop_5_8_right-based, NOH²(Γ_A,R));stageR136_gammaA_of_hcard— the (136) identity, threadinghcard_A(the Prop. 8.9 assembly'scard_H2_gammaA_eq_two) so e5 is decoupled from e6.
Standing plumbing note (the GA/GammaA bridge). GammaA := profiniteQuotient NA is
defeq to GA := FreeProfiniteGroup (Fin 4) ⧸ NA, but their instances do not cross-resolve
(distinct head symbols): GammaA carries TotallyDisconnectedSpace (a ProfiniteGrp) while
GA does not auto-synthesise it, and a DistribMulAction GammaA (ZMod 2) is not found when a
DistribMulAction GA (ZMod 2) is requested. The theorems are stated over Γ := GammaA (so the
blockStageR136/RecursionInputs instances resolve and the conclusion matches the Prop. 8.9 assembly
RecursionInputs RF B.bA F … bundle); the word-machinery calls (over GA) are bridged inside
each proof by inferInstanceAs/show-transports across the defeq (gammaA_eq_GA below). This
is the main mechanical cost of the candidate side and is isolated to the proof interiors.
Γ_A's underlying type is the raw quotient GA against which the marking machinery
(z1Equiv, markC, prop_5_15) is stated.
The canonical trivial Γ_A-action on 𝔽₂ #
The trivial Γ_A-action on 𝔽₂ (Aut(𝔽₂) = 1, so every action is this one).
Equations
- One or more equations did not get rendered due to their size.
The Γ_A-action on 𝔽₂ is trivial (the Prop. 8.9 assembly residue): definitional, from the
registered trivial action.
Shared C = Y/K-module helpers (used by hZcount and hsep_hom) #
hZcount: the z_R torsor count at the candidate source #
The candidate mirror of RStageLocal.hZcount_local: RCocycle ≃ Z¹(Γ_A, R_{f₀}) (identical
conjugation-action setup, reusing RStageLocal's ConjAction section), then the count via
z1Equiv + prop_5_15 clause 2 (#Z1w = #R²·#fixedPts C (R^∨)) instead of the local
card_Z1_eq, and the same fixedPts ≃ RCharSub bridge + blockRChar_card.
L2 — d1Fun naturality (word-complex helper for the separation's L4/L5) #
L3 — the trace-span package: (R^∨)^C perfectly pairs H2w (plan §2, gap (i)) #
The trace functional Φ_λ : H2w(A) →+ 𝔽₂, [v] ↦ λ(v.1 + v.2) (docs/orchestration/p16d6e5-plan.md
§2, L3). Well-defined on the quotient H2w = (A×A) ⧸ im d¹ because for an invariant λ
(d⁰λ = 0), prop_5_8_right gives λ((d¹x).1 + (d¹x).2) = mixedB t x (d⁰λ) = mixedB t x 0 = 0.
This is the (2,0)-pairing the candidate IsSelfDual omits — supplied by prop_5_8 directly.
Equations
- GQ2.RStageGammaA.wTrace t ht hw lam hlam = QuotientAddGroup.lift (GQ2.FoxH.d1 t).range (AddMonoidHom.comp lam (AddMonoidHom.fst A A + AddMonoidHom.snd A A)) ⋯
Instances For
L3b: λ ↦ Φ_λ is injective — Φ_λ at [⟨a,0⟩] is λ a, so the functional determines
λ. (With the counting #{invariant λ} = #H2w, this makes λ ↦ Φ_λ a bijection onto
H2w →+ 𝔽₂ — the perfect (2,0)-pairing.)
L3c: λ ↦ Φ_λ is surjective onto H2w →+ 𝔽₂ — the counting half of the perfect
(2,0)-pairing (docs/orchestration/p16d6e5-plan.md §2, L3). The invariant characters, #H2w, and
#(H2w →+ 𝔽₂) are all equinumerous:
#{λ : d⁰λ = 0} = #fixedPts C (A^∨) = #H2w = #(H2w →+ 𝔽₂) — by H0w_eq_fixedPts (needs
Generates), IsSelfDual clause 1, and card_addHom_zmod2. A finite injection
(wTrace_injective) between equinumerous finite sets is bijective
(Fintype.bijective_iff_injective_and_card), hence surjective.
L3d: sep_word — the separation (docs/orchestration/p16d6e5-plan.md §2, L3). If v.1 + v.2 is
killed by every invariant character λ (d⁰λ = 0), then v ∈ im d¹. Proof: if [v] ≠ 0 in
H2w, then exists_addHom_ne_zero (finite 𝔽₂-space) produces a functional Ψ with
Ψ [v] ≠ 0; by wTrace_surjective, Ψ = Φ_λ for some invariant λ, and
Φ_λ [v] = λ(v.1 + v.2) = 0 by hypothesis — contradiction. So [v] = 0, i.e. v ∈ im d¹.
L3e — the trivial-coefficient trace: im d¹ lands in the sum-zero locus (feeds L4) #
L1 — the relator correction at a central 2-torsion kernel (the per-cover algebra of L4) #
powOmega2 under a central-involution correction — the crux of the wild relator
correction (docs/orchestration/p16d6e5-plan.md §2, L1-wild). For a central involution s, the 2-primary
projection satisfies powOmega2 (s * a) = s * powOmega2 a: s is its own 2-part, and powOmega2
is multiplicative on the abelian subgroup ⟨s, a⟩. The orderOf (s*a)-shift (which breaks the
naive powOmega2_pow_eq at a's own order) is dissolved by evaluating all three ω₂-powers at a
common modulus M = 2·|a|·|s*a| (divisible by |s|, |a|, |s*a|), à la powOmega2_prod;
powOmega2 s = s because |s| ∣ 2 is a 2-power.
L1 tame row, central 2-torsion (docs/orchestration/p16d6e5-plan.md §2, L1): correcting a marking's
generators by central involutions shifts the tame relator value by exactly the τ-correction —
tameValue⟨r₀σ, r₁τ, x₀, x₁⟩ = r₁ · tameValue⟨σ, τ, x₀, x₁⟩. The σ-correction r₀ cancels
(σ⁻¹r₀⁻¹(r₁τ)r₀σ, r₀ central), and the τ-square kills r₁². This is the group-level Fox tame
derivative — matching d1Fun_tame_trivial's x 1. At L4's cover Y/l the kernel R/l ≅ 𝔽₂ is
central 2-torsion, so this applies with r⃗ := the set-lift-vs-hom corrections.
Conjugation under central corrections (docs/orchestration/p16d6e5-plan.md §2, L1-wild building block):
conjP (rₐ·x) (r_g·g) = rₐ · conjP x g for central rₐ, r_g — the conjugating correction r_g
cancels (g⁻¹r_g⁻¹…r_g g), the conjugated correction rₐ survives. Used for z0 = conjP x₀ σ₂,
x₁^σ, dg = conjP d₀ g₀, and the x₀^g₀ factor of h₀.
Commutators are insensitive to central corrections (docs/orchestration/p16d6e5-plan.md §2, L1-wild
building block): commP (rₐ·a) (r_b·b) = commP a b for central rₐ, r_b — both corrections cancel
in the commutator (a⁻¹rₐ⁻¹ b⁻¹r_b⁻¹ rₐa r_bb, all central factors pair off). Used for
c0 = commP d₀ z₀ and h_c = commP dg d₀ — these two auxiliary words are correction-free.
L1-wild — the auxiliary-word correction chain (mechanical, from the building blocks) #
The marking with each generator corrected by a central involution (docs/orchestration/p16d6e5-plan.md
§2, L1). The wild relator value shifts by exactly r₁ — proved word-by-word below.
Equations
Instances For
u₀ = powOmega2 (x₀τ) picks up r₂r₁ (the x₀- and τ-corrections combine centrally).
u₁ = powOmega2 (x₁τ) picks up r₃r₁.
z₀ = x₀^σ₂ = conjP x₀ σ₂ picks up r₂ (the conjugating σ₂-correction r₀ cancels).
d₀ = u₀ x₀⁻¹ picks up r₁ (the r₂ from u₀ meets r₂⁻¹ from x₀⁻¹).
Conjugation by a correction-free element (the rg = 1 case of conjP_central_correction):
conjP (rₐ·x) g = rₐ · conjP x g. Used for dg = conjP d₀ g₀ and h₀'s x₀^g₀ factor.
c₀ = commP d₀ z₀ is correction-free (commP kills the r₁, r₂ corrections).
dg = d₀^g₀ = conjP d₀ g₀ picks up r₁ (from d₀; g₀ is correction-free).
h_c = commP dg d₀ is correction-free (commP kills the two r₁ corrections).
h₀ = x₀^g₀·x₀·dg·d₀·d₀²·h_c is correction-free — the six factors pair into three
correction-free central_pairs: (r₂·,r₂·), (r₁·,r₁·), and (d₀², h_c) (already free).
L1 wild row, central 2-torsion (docs/orchestration/p16d6e5-plan.md §2, L1-wild): the wild relator value
shifts by exactly the τ-correction r₁ — wildValue(r⃗·ŷ) = r₁ · wildValue ŷ. h₀ and c₀ are
correction-free; u₁⁻¹ contributes (r₃r₁)⁻¹ and x₁^σ contributes r₃, whose r₃'s cancel,
leaving r₁⁻¹ = r₁. Matches d1Fun_wild_trivial's x 1.
Relator death along any continuous hom from Γ_A; marking extensionality (L4/L5) #
Relators die along any continuous hom from Γ_A, tame (docs/orchestration/p16d6e5-plan.md §2, L4 —
NO surjectivity, unlike markC_admissible): the pushed marking of any f : Γ_A →ₜ* G' satisfies
the tame relation, because the tame relator word lies in N_A (tameRelator_mem_NA).
Relators die along any continuous hom from Γ_A, wild (wildRelator_mem_NA).
The WordLift multiplication/base-change calculus — the general relator correction #
The proved L1 (tameValue_correction/wildValue_correction) handles corrections by central
involutions — the per-cover algebra of L4. L5 additionally needs the general correction at
Y itself (corrections in the non-central R), which factors through the lift group
A ⋊ Y = WordLift: evaluating the relators at liftMarking t x and pushing through the
multiplication homomorphism (u, g) ↦ j u · g (a hom exactly because the action is realized
by conjugation) yields value(j(x)·t) = j(d¹-row) · value(t) — the group-level Fox rows, with
no new word expansion. d1Fun_base_change transports the d¹-row between the Y-conjugation
action and the C = Y/K-action of the word complex (sep_word lives at markC θ : Marking C).
The base projection A ⋊ G →* G of the lift group.
Equations
- GQ2.RStageGammaA.projW = { toFun := fun (p : GQ2.FoxH.WordLift A G) => p.g, map_one' := ⋯, map_mul' := ⋯ }
Instances For
liftMarking projects back onto the base marking (structure eta).
The base coordinate of the evaluated tame relator is the base tame relator value.
The base coordinate of the evaluated wild relator (finite: the ω₂-push).
The multiplication homomorphism A ⋊ G →* G of a conjugation-realized coefficient
module: (u, g) ↦ j u · g, for j : A → G multiplicative with j (g • a) = g · (j a) · g⁻¹.
Equations
- GQ2.RStageGammaA.mulW j hjmul hjconj = { toFun := fun (p : GQ2.FoxH.WordLift A G) => j p.u * p.g, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The general relator correction, tame: left-multiplying a marking's generators by the
j-realizations of coefficients x multiplies the tame relator value by j of the tame
d¹-row. (Evaluate the relator in A ⋊ G and push through mulW.)
The general relator correction, wild.
Base change of the lift group along f : G →* C when the G-action is the f-pullback.
Equations
- GQ2.RStageGammaA.baseW f hcompat = { toFun := fun (p : GQ2.FoxH.WordLift A G) => { u := p.u, g := f p.g }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
d¹ base change: the word differential only sees the action, so it is computed by the
pushed marking — d1Fun (t.map f) x = d1Fun t x when the G-action is pulled back along f.
L4 core: a cover lift forces equal reduced relator values #
The per-cover L4 core (docs/orchestration/p16d6e5-plan.md §2, L4), abstractly over a bare central
cover: if g_B lifts through Q (via gc), then any set-lift marking tY of g_B has equal
tame and wild relator values after reduction along red. Both tY.map red and the lift's
pushed marking cover g_B's marking, so they differ by corrections in the central 2-torsion
kernel (CentralCover.central/z_sq); the proved L1 (tameValue_correction/
wildValue_correction) evaluates both reduced relator values to the same r̄₁. (Un-privated
for the Prop. 8.9 assembly's hsep_gammaA, which runs the same extraction at the T-stage covers.)
L5 descent: a relator-free covering marking of Y descends from Γ_A #
hsep_hom: the (R^∨)^C separation at the candidate source (L1–L5, the main work) #
The (R^∨)^C-separation at Γ_A (the Prop. 8.9 assembly residue): if the obstruction functional of a
boundary lift g vanishes, g lifts to a continuous homomorphism into Y. Route
(docs/orchestration/p16d6e5-plan.md §2): obs g = 0 gives, per invariant character, a concrete lift through
the scalar cover (obs_zero_iff_lifts); the relator-value corrections of a set-lift are d1Fun
rows (L1); the trace-span package (L3, prop_5_8_right) forces full word-solvability; the
corrected marking descends by markC_admissible + NA_le_ker + quotientLift (L5). hcard_A
is threaded (proof-irrelevant Prop; supplied by the Prop. 8.9 assembly's card_H2_gammaA_eq_two).
stageR136: the (136) identity, assembled #
(136) for the block frame at the candidate source (the Prop. 8.9 assembly, threading hcard_A):
htriv/hZcount/hsep_hom are the residues discharged here; hcard_A (the Prop. 8.9 assembly) and the
lemma_7_2 structural facts hRK/hR2 thread hypothesis-side. hfg is
gammaA_topologicallyFinitelyGenerated (the finite-generation proof ✓ — dischargeable here, unlike the local B1
reservation). The conclusion is the stageR136 field of the candidate RecursionInputs
bundle (the Prop. 8.9 assembly), verbatim.