Foundations for the Γ_A phase-140 residues #
The candidate-side count, per-character covers, and descent of covering markings.
See GQ2.Phase140.GammaA for the paper-facing overview and architectural notes.
hZcard for Γ_A — #Z¹_{Γ_A,ρ'}(V) = #V². Mirror of Phase140Local.hZcard_local with
the candidate count: the VCocycle ≃ Z¹_cont(Γ_A, V) bridge (structurally Γ-generic, copied
from the local file), then z1Equiv + prop_5_15 clause 2 (#Z1w = #V²·#fixedPts) instead of
card_Z1_eq, and the #fixedPts = 1 factor from the simple nontrivial Y_C-action
(card_fixedPts_elemDual_eq_one_of_nontrivial).
hnt (the nontrivial Y_C-action) is REQUIRED — in the #V = 2 ∧ Y_C = 1 corner
#(V^∨)^{Y_C} = 2 ≠ 1 and the identity is false; it is discharged at the capstone from the
block's chief-factor structure (same amendment as the local file).
hμ for Γ_A — the T-cocycle count #Z¹_{Γ_A,ρ'}(T) = #T²·#(T^∨)^{Y_B/M} in the
muZero closed form (Phase140Local.tcocycle_card_local's twin). Same module setup (the
global RadicalEdgeGammaA.cActT conjugation action replaces the proof-local one) and the
same TCocycle ≃ Z¹_cont(GA, Additive T) bridge; the count is z1Equiv + prop_5_15
clause 2 instead of card_Z1_eq — no B-axioms. The #fixedPts factor is NOT reduced: it
is part of the shared μ₀ value (the twin dualities produce the same closed form, which is
the source-independence prop_8_9 needs).
The per-character 𝔽₂-covers of Q = B/T (Γ-generic; the hsep_A L4 covers) #
The kernel of a C-invariant character, as a subgroup of ↥D.T.
Equations
- GQ2.Phase140GammaA.charKerSub χ = { carrier := {t : ↥D.T | ↑χ t = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
The kernel of χ, pushed to a subgroup of Bg.
Equations
- GQ2.Phase140GammaA.charKer χ = Subgroup.map D.T.subtype (GQ2.Phase140GammaA.charKerSub χ)
Instances For
A witness t₀ ∈ T with χ(t₀) = 1 (for χ ≠ 0) — the kernel generator's complement.
Equations
- GQ2.Phase140GammaA.charWitness χ hχ = ⋯.choose
Instances For
The χ-cover B ⧸ ker χ ↠ B ⧸ T: a central double cover with kernel
T/ker χ ≅ 𝔽₂, generated by the class of the witness t₀ (χ(t₀) = 1). The T-stage
mirror of blockFrameImpl.scalarCover; centrality of the kernel is the C-invariance
of χ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The reduction Bg →* (charCover χ hχ).cover — the coverMap of the χ-cover.
Equations
- GQ2.Phase140GammaA.charCoverMap χ hχ = QuotientGroup.mk' (GQ2.Phase140GammaA.charKer χ)
Instances For
The χ-cover covers π_T through its reduction.
T-elements reduce to the kernel sign z^{χ(t)} in the χ-cover — the
pair_coverMap of the T-stage.
β_χ(c) = 0 produces a lift through the χ-cover (the T-stage
obs_zero_iff_lifts, forward direction): a B²-witness ψ for χ_* tDef corrects the
pointwise lift fLift into a continuous homomorphism γ ↦ (fLift γ mod ker χ) · z^{ψγ}
covering g_c.
L5 descent at the T-stage: a relator-free covering marking of B descends from Γ_A #
The T-stage mirror of RStageGammaA.lift_of_relatorFree_marking, with one new twist: the
covered map g_Q : Γ_A → B/T is not surjective (its image is the graph-like subgroup of a
V-cocycle), so Marking.push_admissible does not apply directly. The fix is a
corestriction through the classified hom: the four B/T-generator images generate a
subgroup J̄, the F₄-hom classified by the J̄-marking kills N_A (compare with
g_Q ∘ quotientMk through toHom_hom_univMarking_map and transfer the kernel through the
injective subtype), so it descends to a surjective ḡ : Γ_A ↠ J̄ — whose pushed marking
is admissible, feeding the Pro2Core chase.
The T-stage descent (hsep_A L5): a marking of B that covers g_Q's marking
through π_T and kills both relators descends to a continuous f : Γ_A → B with
π_T ∘ f = g_Q.