The concrete R-stage obstruction datum + (136) for blockFrame

Builds RObstructionData (blockFrameImpl T Blk hE2) — the (136) stageR136 datum — against the concrete §7-block frame (the §9 induction ✓, blockFrameImpl), and wires it into stageR136_ofRSepData to produce the (136) identity blockStageR136.

Concrete covers (blockFrameImpl): YB = Y/R, piB = mk' R, scalarCover l h = the cover Y/l ↠ Y/R (cover = Y/l.1, p = map l.1 R id, z = mk' l.1 r₀). So coverMap l h = mk' l.1 and coverMap_lifts is map ∘ mk' = mk'.

a-DRmod / a-assemble (std-3): blockRObstructionData — the full (R^∨)^C character duality.

a-residues (blockStageR136): hE2 is discharged from the frame argument; the source residues htriv/hcard/hfg/hZcount/hsep_hom are threaded as hypotheses (supplied by the Prop. 8.9 assembly assembly / the §9 induction, where Γ = GammaA/AbsGalQ2 carry the concrete trivial action and the 5.15/5.16 numerics). hZcount (the z_R = #R²·#D_R torsor count) and hsep_hom (the (R^∨)^C-separation) are the two irreducible source cores — see the notes on blockStageR136.

noncomputable def GQ2.blockRCoverData {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : SectionEight.RCoverData (blockFrameImpl T Blk hE2)

The R-stage compat covers of the concrete block frame: coverMap l h = mk' l.1.

Equations

• One or more equations did not get rendered due to their size.

A-DRmod: D_Rmod as the Y-invariant 𝔽₂-characters of R

def GQ2.RCharSub {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) : Submodule (ZMod 2) (Additive ↥Blk.frattiniK →+ ZMod 2)

Y-invariant 𝔽₂-characters of R = Blk.frattiniK = Φ(K) ((R^∨)^C): additive homs R → 𝔽₂ fixed by Y-conjugation. Their kernels are exactly the index-≤2 Y-normal subgroups of R, i.e. D_R; this submodule is the 𝔽₂-realization D_Rmod.

Equations

• One or more equations did not get rendered due to their size.

instance GQ2.instFiniteSubtypeAddMonoidHomAdditiveMemSubgroupFrattiniKZModOfNatNatSubmoduleRCharSub {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) : Finite ↥(RCharSub Blk)

D_Rmod is finite.

def GQ2.RCharKerSub {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (χ : ↥(RCharSub Blk)) : Subgroup ↥Blk.frattiniK

The kernel of a character χ, as a subgroup of ↥Blk.frattiniK.

Equations

• GQ2.RCharKerSub Blk χ = { carrier := {r : ↥Blk.frattiniK | ↑χ (Additive.ofMul r) = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def GQ2.RCharMulHom {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (χ : ↥(RCharSub Blk)) : ↥Blk.frattiniK →* Multiplicative (ZMod 2)

χ as a MonoidHom ↥R →* Multiplicative 𝔽₂ (for the kernel/index calculus).

Equations

• GQ2.RCharMulHom Blk χ = { toFun := fun (r : ↥Blk.frattiniK) => Multiplicative.ofAdd (↑χ (Additive.ofMul r)), map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.RCharKerSub_eq_ker {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (χ : ↥(RCharSub Blk)) : RCharKerSub Blk χ = (RCharMulHom Blk χ).ker

def GQ2.RCharKer {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (χ : ↥(RCharSub Blk)) : Subgroup Y

The kernel of χ, pushed to a subgroup of Y.

Equations

• GQ2.RCharKer Blk χ = Subgroup.map Blk.frattiniK.subtype (GQ2.RCharKerSub Blk χ)

@[reducible, inline]

abbrev GQ2.BlockDRsub {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) : Type

The D_R index type of the concrete frame blockFrameImpl (defeq to its .DR).

Equations

• GQ2.BlockDRsub Blk = { R' : Subgroup Y // R'.Normal ∧ R' ≤ Blk.frattiniK ∧ R'.relIndex Blk.frattiniK ≤ 2 }

noncomputable def GQ2.RCharOfHom {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (R' : BlockDRsub Blk) : Additive ↥Blk.frattiniK →+ ZMod 2

The inverse direction: the index-≤2 indicator character r ↦ [r ∉ R'] of a D_R element, as an additive hom (additive by mul_mem_iff_of_index_two, with the index ≤ 2 case-split covering R' = R — the zero character).

Equations

• GQ2.RCharOfHom Blk R' = { toFun := fun (r : Additive ↥Blk.frattiniK) => if ↑(Additive.toMul r) ∈ ↑R' then 0 else 1, map_zero' := ⋯, map_add' := ⋯ }

theorem GQ2.RCharOf_mem {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (R' : BlockDRsub Blk) : RCharOfHom Blk R' ∈ RCharSub Blk

RCharOfHom R' is Y-invariant, hence a member of RCharSub — from R'.Normal.

noncomputable def GQ2.RCharOf {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (R' : BlockDRsub Blk) : ↥(RCharSub Blk)

The inverse map D_R → D_Rmod: R' ↦ its index-≤2 indicator character.

Equations

• GQ2.RCharOf Blk R' = ⟨GQ2.RCharOfHom Blk R', ⋯⟩

theorem GQ2.RChar_eq_ind {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (χ : ↥(RCharSub Blk)) (r : ↥Blk.frattiniK) : ↑χ (Additive.ofMul r) = if r ∈ RCharKerSub Blk χ then 0 else 1

A character is the indicator of its own kernel (𝔽₂-valued).

theorem GQ2.RCharKer_RCharOf {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) (R' : BlockDRsub Blk) : RCharKer Blk (RCharOf Blk R') = ↑R'

Right inverse: the kernel of the indicator character of R' is R'.

theorem GQ2.RCharKer_inj {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) : Function.Injective fun (χ : ↥(RCharSub Blk)) => RCharKer Blk χ

Injectivity of χ ↦ ker χ: a character is determined by its kernel.

A-DRmod: assembling the (R^∨)^C bijection and pair

noncomputable def GQ2.blockToDR {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : ↥(RCharSub Blk) ≃ (blockFrameImpl T Blk hE2).DR

The (R^∨)^C bijection D_Rmod ≃ D_R: χ ↦ ker χ (inverse R' ↦ its indicator). Codomain is the concrete frame's .DR (so the assembly's pair_coverMap types align).

Equations

• GQ2.blockToDR T Blk hE2 = Equiv.ofBijective (fun (χ : ↥(GQ2.RCharSub Blk)) => ⟨GQ2.RCharKer Blk χ, ⋯⟩) ⋯

theorem GQ2.RCharKer_zero {Y : Type} [Group Y] {L : Subgroup Y} (Blk : SectionSeven.MinimalBlock L) : RCharKer Blk 0 = Blk.frattiniK

The zero character's kernel is all of R (= zeroDR).

A-assemble: the concrete R-stage obstruction datum blockRObstructionData

noncomputable def GQ2.blockRObstructionData {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : SectionEight.RObstructionData (blockFrameImpl T Blk hE2)

The concrete R-stage obstruction datum for the §7-block frame (the Prop. 8.9 assembly): assembles blockRCoverData with the (R^∨)^C module D_Rmod = RCharSub, the bijection blockToDR, and pair = the submodule inclusion, whose pair_coverMap matches the cover kernel-sign zsign (= [r ∉ ker d]). This is the RObstructionData input to stageR136_ofRSepData.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.blockRChar_card {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : Nat.card ↥(RCharSub Blk) = Nat.card (blockFrameImpl T Blk hE2).DR

The (R^∨)^C = D_R cardinality bridge. The Y-invariant 𝔽₂-characters of R (RCharSub = D_Rmod = (R^∨)^C) are equinumerous with the R-stage index type D_R of the concrete frame, since blockToDR is a bijection. So the z_R = #R²·#D_R torsor count's #D_R factor is the intrinsic invariant-character count #(R^∨)^C — the shape the 5.15/5.16 Euler characteristic #Z¹(Γ,R) = #R²·#(R^∨)^C produces, which is what a hZcount discharge targets.

A-residues → (136): wiring blockRObstructionData into stageR136_ofRSepData

theorem GQ2.blockStageR136 {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hsep_hom : ∀ (g : BoundaryLifts b F (blockFrameImpl T Blk hE2).TB), SectionEight.obs (blockFrameImpl T Blk hE2) (blockRObstructionData T Blk hE2) htriv hcard ↑↑g = 0 → ∃ (φ : Γ →ₜ* Y), ∀ (γ : Γ), (blockFrameImpl T Blk hE2).piB (φ γ) = ↑↑g γ) (hZcount : ∀ (f₀ : BoundaryLifts b F T), Nat.card (SectionEight.RCocycle (blockFrameImpl T Blk hE2) ↑↑f₀) = (blockFrameImpl T Blk hE2).zR) : ↑(Nat.card (blockFrameImpl T Blk hE2).DR) * ↑(exactImageCount b F T) = ↑(blockFrameImpl T Blk hE2).zR * ∑ᶠ (l : (blockFrameImpl T Blk hE2).DR), (2 * ↑((blockFrameImpl T Blk hE2).mB b F l) - ↑(exactImageCount b F (blockFrameImpl T Blk hE2).TB))

the Prop. 8.9 assembly (136) for the concrete §7-block frame. Instantiates the abstract R-stage finish line stageR136_ofRSepData at the concrete frame blockFrameImpl with the concrete obstruction datum blockRObstructionData (the full (R^∨)^C character duality, std-3). hE2 is discharged from the frame's own argument; the remaining inputs are the source residues threaded by the the Prop. 8.9 assembly:

• htriv — the trivial Γ-action on 𝔽₂ (fun _ _ => rfl once Γ = GammaA/AbsGalQ2);
• hcard — #H²(Γ,𝔽₂) = 2 (props 5.15/5.16);
• hfg — Γ topologically finitely generated (GammaA via the finite-generation proof; AbsGalQ2 via B1, reserved to the §9 induction — kept hypothesis-side);
• hsep_hom — the (R^∨)^C-separation obs g = 0 ⟹ g has a homomorphism lift to Y. This is the Γ-specific arithmetic duality D_R = (R^∨)^C ≅ H²_{Γ,ρ}(R)^∨ — the R-instance of the duality the paper displays for the phase module T (p. 42 top), used implicitly by Prop 8.9 (the z_R display and the Fourier inversion over D_R): obs g d = ⟨d, ob(g)⟩ pairs d with the full R-obstruction, and the perfect pairing forces ob(g) = 0 (hence a lift) once every d kills it. Props 5.15/5.16, NOT abstract; discharged per-Γ at assembly alongside hZcount. Prefer consuming via blockStageR136_ofSplitCriterion below, which pre-discharges all the frame plumbing and leaves only the cochain-level split criterion.
• hZcount — the z_R torsor count #RCocycle = z_R = #R²·#D_R = |Z¹_{Γ,ρ}(R)| (the 5.15/5.16 numeric for the R-extension, the (139)-hMcount analogue).

The conclusion is the stageR136 field of RecursionInputs verbatim (for the Prop. 8.9 assembly).

The per-Γ residue interface: the split criterion

hsep_hom_of_splitCriterion strips the last frame-generic layer off hsep_hom: the obstruction functional and its H²(Γ,𝔽₂) classes (obs_zero_iff_pairClass_zero), the degenerate d = 0 character, and the split-cochain → hom-lift assembly (homLift_of_split) are all discharged here, so a source supplies only the split criterion — the (R^∨)^C-separation at the cochain level: if every invariant character d sends the R-valued section defect of g to a coboundary class in H²(Γ,𝔽₂), then the defect splits by a continuous R-cochain. On the local source this is prop_5_16 clause 6 (cup20 bijectivity, i.e. pushforward-injectivity H²(Γ,R_ρ) ↪ ((R^∨)^C)^∨, since cup20 c φ = [φ ∘ c] for invariant φ) plus B²-extraction at the compHom action (the slift-conjugation action on R factors through C = Y/K by lemma_7_2's K-centrality); on the candidate source it is the §5 word-complex route (docs/orchestration/p16d6a-handoff.md §3).

theorem GQ2.hsep_hom_of_splitCriterion {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : SectionEight.RecursionFrame T Blk) (D : SectionEight.RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hsplit : ∀ (g : Γ →ₜ* RF.YB), (∀ (d : D.DRmod), (ContCoh.H2mk Γ (ZMod 2)) ⟨fun (gd : Γ × Γ) => (D.pair d) (Additive.ofMul (SectionEight.rDefect RF g gd.1 gd.2)), ⋯⟩ = 0) → ∃ (c : Γ → ↥Blk.frattiniK), (Continuous fun (γ : Γ) => ↑(c γ)) ∧ ∀ (γ δ : Γ), ↑(c (γ * δ)) = ↑(c γ) * (SectionEight.slift RF (g γ) * ↑(c δ) * (SectionEight.slift RF (g γ))⁻¹) * ↑(SectionEight.rDefect RF g γ δ)) (g : BoundaryLifts b F RF.TB) : SectionEight.obs RF D htriv hcard ↑↑g = 0 → ∃ (φ : Γ →ₜ* Y), ∀ (γ : Γ), RF.piB (φ γ) = ↑↑g γ

theorem GQ2.blockStageR136_ofSplitCriterion {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hsplit : ∀ (g : Γ →ₜ* (blockFrameImpl T Blk hE2).YB), (∀ (d : (blockRObstructionData T Blk hE2).DRmod), (ContCoh.H2mk Γ (ZMod 2)) ⟨fun (gd : Γ × Γ) => ((blockRObstructionData T Blk hE2).pair d) (Additive.ofMul (SectionEight.rDefect (blockFrameImpl T Blk hE2) g gd.1 gd.2)), ⋯⟩ = 0) → ∃ (c : Γ → ↥Blk.frattiniK), (Continuous fun (γ : Γ) => ↑(c γ)) ∧ ∀ (γ δ : Γ), ↑(c (γ * δ)) = ↑(c γ) * (SectionEight.slift (blockFrameImpl T Blk hE2) (g γ) * ↑(c δ) * (SectionEight.slift (blockFrameImpl T Blk hE2) (g γ))⁻¹) * ↑(SectionEight.rDefect (blockFrameImpl T Blk hE2) g γ δ)) (hZcount : ∀ (f₀ : BoundaryLifts b F T), Nat.card (SectionEight.RCocycle (blockFrameImpl T Blk hE2) ↑↑f₀) = (blockFrameImpl T Blk hE2).zR) : ↑(Nat.card (blockFrameImpl T Blk hE2).DR) * ↑(exactImageCount b F T) = ↑(blockFrameImpl T Blk hE2).zR * ∑ᶠ (l : (blockFrameImpl T Blk hE2).DR), (2 * ↑((blockFrameImpl T Blk hE2).mB b F l) - ↑(exactImageCount b F (blockFrameImpl T Blk hE2).TB))

(136) for the block frame, from the split criterion — blockStageR136 with hsep_hom pre-discharged by hsep_hom_of_splitCriterion. The per-Γ inputs are now exactly the source's 5.15/5.16 duality package: the numerics hcard/hfg, the split criterion hsplit (the (R^∨)^C-separation at the cochain level), and the torsor count hZcount.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Prop 8.9 = ⟦thm-closedrecursion⟧ (= theorem 8.17 in current tex)