Proposition 8.9 at the concrete block frame

Proposition 8.9 (closed exact-image recursion), relocated here from SectionEight.lean (which cannot name blockFrameImpl — it sits above BlockFrameImpl.lean in the import order). Two interface choices are important:

• Per-λ phase family — the paper's (134) classes Δ_{χ,κ} carry the scalar-pushout class κ = κ_λ of the λ-cover, so the family is phase : (l : DR) → l ≠ zeroDR → DT → CentralCover YC (the shared-family draft form was a transcription deviation; it would force an unproven zBC-l-independence).
• Concrete block frame + hypothesis ledger — the statement is at RF := blockFrameImpl T Blk hE2 (the only intended consumer: SectionNine's inductive branch at blockFrame/blockEnrichment; general-RF (136) is not provable — no axioms tie a bare frame's DR/zR/mB to obstruction theory). The hypotheses are explicit: hE2, hfgF (B1), hheadA/hheadF (§9 boundary data), hsimple/hVne/hnt (the block's chief-factor structure; hnt = SectionNine.blockHnt; faithfulness is NOT block-derivable, and only hnt was consumed), hG0indep (c3-G0's gaussSum_qbar_l_indep_* at the block's tame package).
• The conclusion includes 0 < Nat.card DT, witnessed by 0 ∈ (T^∨)^C.

Assembly

The witness assembly: the hex-split (¬hex: DT := PUnit, vacuous (137)–(140), only the two (136) stages live), the shared DT := (T^∨)^C at a reference λ₀ (definitionally λ-independent — radData's T/hT are the literal frame fields), the dite-phase family with its dif_pos-reduction (phaseFamily_pos), the shared μ = #V·μ₀ value (muZero, read at λ₀ and transported per-λ by tcocycle_card_l_indep), and the two prop_8_9_aux splices. hRK/hR2 are discharged internally (lemma_7_2 at π := T.piY, cH := F.alpha — the plan-doc ledger), hfgA/hscalar internally (gammaA_topologicallyFinitelyGenerated, lemma_8_2_*); hnt is a hypothesis (the block's nontrivial_action, via SectionNine.blockHnt).

Input bundles: local = RStageLocal.stageR136_local + half139_local + phase140_local; Γ_A = CardH2GammaA.stageR136_gammaA + half139_gammaA (below: lemma_8_6_gammaA + liftsOver_card_gammaA through half139_via_radData) + the four residues (hsep_gammaA / hpartial_gammaA / hZcard_gammaA / tcocycle_card_gammaA) through the source-generic phase140_from_residues.

#print axioms prop_8_9 is the standard three axioms plus B6 tateDualityAt and B7 absGalQ2_localEulerCharacteristic, leaner than the App. D budget because B9 never enters this proof. One elaboration detail is worth preserving: simpa … using fails the cross-λ TCharC definitional-equality close, while simp only […] followed by a bare exact works.

The shared witness data: descent unpacking, phase family, μ₀

noncomputable def GQ2.SectionEight.descentOf {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (hN : ∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) : AffineTLift.Descent (En.radData l h)

The (140) zero-edge unpacking: the RecursionInputs.phase140 hypothesis is the descent condition of the assembled per-λ datum (Enrichment.radData_noDescent_iff is Iff.rfl), so it unpacks verbatim to an AffineTLift.Descent.

Equations

• GQ2.SectionEight.descentOf En l h hN = { N := hN.choose, hN := ⋯, hNT := ⋯, hNz := ⋯ }

noncomputable def GQ2.SectionEight.trivialPhaseCover (C0 : Type) [Group C0] [Finite C0] : CentralCover C0

The zero-cocycle (split) double cover 𝔽₂ × C₀: the junk value of the phase family off the zero-edge locus. (140)'s hypothesis restricts attention to the locus, so this value is never inspected.

Equations

• GQ2.SectionEight.trivialPhaseCover C0 = GQ2.SectionEight.AffineTLift.centralCoverOfCocycle (fun (x : C0 × C0) => 0) ⋯ ⋯ ⋯

noncomputable def GQ2.SectionEight.phaseFamily {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l₀ : RF.DR) (h₀ : l₀ ≠ RF.zeroDR) (l : RF.DR) (h : l ≠ RF.zeroDR) (ζ : ↥(AffineTLift.TCharC (En.radData l₀ h₀))) : CentralCover RF.YC

The shared per-λ phase family (the paper's Δ_{ζ,κ_λ}-covers, (134)): on the zero-edge locus, the phaseChi-cover through the unpacked descent; off it, the trivial cover. The phase index ζ is typed at a reference (l₀, h₀): TCharC (En.radData l h) is definitionally (l,h)-independent (radData's T/hT are the literal frame fields RF.TBsub/RF.TBsub_normal — plan §1A), so the same ζ is accepted at every λ.

Equations

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

theorem GQ2.SectionEight.phaseFamily_pos {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l₀ : RF.DR) (h₀ : l₀ ≠ RF.zeroDR) (l : RF.DR) (h : l ≠ RF.zeroDR) (hN : ∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) (ζ : ↥(AffineTLift.TCharC (En.radData l₀ h₀))) : phaseFamily En l₀ h₀ l h ζ = phaseChi En l h (descentOf En l h hN) ζ

The dif_pos-reduction of the phase family on the zero-edge locus (the pre-analyzed elaboration risk (b) of the row: the rewrite is proof-irrelevant in the stored descent witness, since descentOf consumes whichever proof the caller holds).

noncomputable def GQ2.SectionEight.muZero {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l₀ : RF.DR) (h₀ : l₀ ≠ RF.zeroDR) : ℕ

The shared T-cocycle count μ₀ (the paper's #Z¹(T_B), (132)), read at the reference (l₀, h₀). Frame-level (radData's T/M are the literal RF.TBsub/RF.MB), hence (l,h)-independent by tcocycle_card_l_indep; its per-ρ constancy and value are the sources' tcocycle_card_* theorems (local ✓ e3; Γ_A = e6).

Equations

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

The Γ_A (139) half count

The half139_local twin: both deep inputs are already banked — lemma_8_6_gammaA (the Γ_A half-torsor proof, the word-side half-torsor count) and the §9 induction M-lift count liftsOver_card_gammaA (MStageCountGammaA), the latter transported through the LiftsOver ↔ MLifts bridge (RadicalEdgeBridge.liftsOver_equiv). Wired through the source-generic half139_via_radData.

theorem GQ2.SectionEight.hlem86M_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (hedge : ¬∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) (ρ : BoundaryLifts b F RF.TC) : 2 * Nat.card { f : MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ) // MLifts.Central (En.radData l h) f } = Nat.card (MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ))

hlem86M for Γ_A — the source's Lemma 8.6 half-torsor count over every boundary lift, for the radical datum En.radData l h, threading the NoDescent field hypothesis (the hlem86M_local mirror; no hfg needed — lemma_8_6_gammaA is word-side).

theorem GQ2.SectionEight.hMcountM_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) : Nat.card (MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card ↥RF.MB ^ 2

hMcountM for Γ_A — the unrestricted M-lift count #(M-lifts) = |M_B|²: the the §9 induction LiftsOver count transported through the LiftsOver ↔ MLifts bridge.

theorem GQ2.SectionEight.half139_gammaA {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] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (hfg : ∃ (s : Finset ↑GammaA.toProfinite.toTop), (Subgroup.closure ↑s).topologicalClosure = ⊤) (l : RF.DR) (h : l ≠ RF.zeroDR) (hedge : ¬∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) : 2 * RF.zBC b F l h = Nat.card ↥RF.MB ^ 2 * exactImageCount b F RF.TC

the Prop. 8.9 assembly result: the (139) half count for Γ_A, in the exact shape of the RecursionInputs.half139 field (the half139_local twin).

theorem GQ2.SectionEight.prop_8_9 {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] (B : BoundaryMaps) {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (En : (blockFrameImpl T Blk hE2).Enrichment) (F : BoundaryFrame H E) [CompactSpace ↑GammaA.toProfinite.toTop] [TotallyDisconnectedSpace ↑GammaA.toProfinite.toTop] [IsTopologicalGroup ↑GammaA.toProfinite.toTop] [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] [IsTopologicalGroup AbsGalQ2] (hfgF : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hheadA : Function.Surjective fun (γ : ↑GammaA.toProfinite.toTop) => (F.frameMap (B.bA γ)).1) (hheadF : Function.Surjective fun (γ : AbsGalQ2) => (F.frameMap (B.bF γ)).1) (hsimple : ∀ (W : AddSubgroup En.Vmod), (∀ (g : (blockFrameImpl T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : En.Vmod), v ≠ 0) (hnt : ∃ (g : (blockFrameImpl T Blk hE2).YC) (v : En.Vmod), g • v ≠ v) (G0 : ℤ) (hGaussZA : ∀ (l : (blockFrameImpl T Blk hE2).DR) (h : l ≠ (blockFrameImpl T Blk hE2).zeroDR), GaussZResidue B.bA F En l h G0) (hGaussZF : ∀ (l : (blockFrameImpl T Blk hE2).DR) (h : l ≠ (blockFrameImpl T Blk hE2).zeroDR), GaussZResidue B.bF F En l h G0) : ∃ (μ : ℕ) (G0' : ℤ) (DT : Type) (x : Fintype DT) (phase : (l : (blockFrameImpl T Blk hE2).DR) → l ≠ (blockFrameImpl T Blk hE2).zeroDR → DT → CentralCover (blockFrameImpl T Blk hE2).YC), 0 < Nat.card DT ∧ ClosedRecursion (blockFrameImpl T Blk hE2) B.bA F μ G0' DT phase ∧ ClosedRecursion (blockFrameImpl T Blk hE2) B.bF F μ G0' DT phase

Proposition 8.9 (closed exact-image recursion): for the concrete block frame of a boundary-framed target with a §7 simple-head block, there are shared data (μ, G⁰, D_T) and a per-λ phase family such that the boxed system (136)–(142) holds for both sources. Every count on the right sides concerns a target with strictly smaller marked 2-kernel, so the system is a closed deterministic recursion (paper, end of §8). [the §8 proof layer statement — relocated & amended at the Prop. 8.9 assembly, see the module docstring; proof = the Prop. 8.9 assembly. Verified axioms: std-3 + {B6, B7} (within the App. D ≤ {B6, B7, B9} budget; B9 never enters).]

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

• Lemma 8.6 = ⟦lem-radicaledge⟧
• Proposition 8.9 = ⟦thm-closedrecursion⟧ (= theorem 8.17 in current tex)