The zBC ↔ MLifts bridge and the (139) half count

The nonzero-radical-edge display (139), 2·Z_{Γ,λ}(B/C) = 2^{2·dim M}·e_Γ(C), in the RecursionInputs.half139 shape 2·zBC = |M_B|²·e_Γ(C).

Strategy (source-generic; the source's Lemma 8.6 and the 2^{2·dim M} M-lift count enter as hypotheses, so d6 plugs in lemma_8_6_local/lemma_8_6_gammaA and the props 5.15/5.16 numerics per source):

1. zBC fibres over the lower exact-image map ρ : Γ ↠ C (BoundaryLifts b F T_C); the fibre is the set of λ-compatible B-lifts over ρ, whose IsBoundaryLift clause is redundant (RecursionFrame.isBoundaryLift_of_over, the Prop. 8.9 assembly).
2. Via the iso B/M ≅ C (piBCiso, from ker π_{BC} = M_B), that fibre is exactly the central M-lifts {f : MLifts (E.radData l h) ρ' // f.Central} of the central-obstruction framework/d1 (Central = lifts through the scalar cover).
3. Lemma 8.6 halves it (2·#central = #MLifts); the props 5.15/5.16 count gives #MLifts = |M_B|². Summing over ρ and clearing the 2 yields (139).

half139_of is the assembled bridge; d6 discharges the two per-source hypotheses. All std-3; the axiom budget (B6, B7) enters only through the consumed Lemma 8.6.

noncomputable def GQ2.SectionEight.RecursionFrame.piBCiso {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) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) : RF.YB ⧸ D.M ≃* RF.YC

The connecting iso B/M ≅ C induced by π_{BC} : B ↠ C with ker = M_B. Stated over a RadicalCoverData datum D with D.M = M_B so the quotient uses D.M's normality instance — matching MLifts (E.radData l h) on the nose (avoids the RF.MB vs (E.radData l h).M instance-diamond in the transport proofs).

Equations

• RF.piBCiso D hD = (QuotientGroup.quotientMulEquivOfEq ⋯).trans (QuotientGroup.quotientKerEquivOfSurjective RF.piBC ⋯)

@[simp]

theorem GQ2.SectionEight.RecursionFrame.piBCiso_mk {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) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (bb : RF.YB) : (RF.piBCiso D hD) ↑bb = RF.piBC bb

def GQ2.SectionEight.RecursionFrame.LiftsOver {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Type

All B-lifts over a lower exact-image map ρ : Γ ↠ C: continuous homs Γ → B whose π_{BC}-image is ρ. (The paper's M-lifts over ρ; IsBoundaryLift is automatic by isBoundaryLift_of_over.)

Equations

• RF.LiftsOver b F ρ = { m : Γ →ₜ* RF.YB // ∀ (γ : Γ), RF.piBC (m γ) = ↑↑ρ γ }

def GQ2.SectionEight.RecursionFrame.CentralOver {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) : Type

The λ-compatible (central) B-lifts over ρ: those lifting through the scalar cover p_λ — the Central relation of the central-obstruction framework.

Equations

• RF.CentralOver b F l h ρ = { m : RF.LiftsOver b F ρ // ∃ (g : Γ →ₜ* (RF.scalarCover l h).cover), ∀ (γ : Γ), (RF.scalarCover l h).p (g γ) = (↑m).toMonoidHom γ }

noncomputable def GQ2.SectionEight.RecursionFrame.zBCfibreEquiv {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) : { x : { pr : BoundaryLifts b F RF.TC × (Γ →ₜ* RF.YB) // (∀ (γ : Γ), RF.piBC (pr.2 γ) = ↑↑pr.1 γ) ∧ IsBoundaryLift b F RF.TB pr.2 ∧ ∃ (g : Γ →ₜ* (RF.scalarCover l h).cover), ∀ (γ : Γ), (RF.scalarCover l h).p (g γ) = pr.2 γ } // (↑x).1 = ρ } ≃ RF.CentralOver b F l h ρ

The zBC fibre over ρ is CentralOver ρ: eliminating the pair, a zBC-datum with C-component ρ is exactly a λ-compatible B-lift over ρ (the IsBoundaryLift clause is redundant, isBoundaryLift_of_over).

Equations

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

theorem GQ2.SectionEight.RecursionFrame.half139_of {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (l : RF.DR) (h : l ≠ RF.zeroDR) (hlem86 : ∀ (ρ : BoundaryLifts b F RF.TC), 2 * Nat.card (RF.CentralOver b F l h ρ) = Nat.card (RF.LiftsOver b F ρ)) (hMcount : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (RF.LiftsOver b F ρ) = Nat.card ↥RF.MB ^ 2) : 2 * RF.zBC b F l h = Nat.card ↥RF.MB ^ 2 * exactImageCount b F RF.TC

The (139) half count (the Prop. 8.9 assembly): 2·zBC = |M_B|²·e_Γ(C) when the radical edge is nonzero. Source-generic: the two per-source inputs enter as hypotheses —

• hlem86 = the source's Lemma 8.6 half-torsor count (lemma_8_6_local/gammaA after the CentralOver ρ ↔ MLifts.Central transport), and
• hMcount = the 2^{2·dim M} M-lift count over each lower map (props 5.15/5.16).

The bridge fibres zBC over the lower exact-image map ρ and sums; d6 discharges hlem86 and hMcount per source.

The MLifts transport

LiftsOver ρ and CentralOver ρ (bridge vocabulary, over π_{BC}) are the central-obstruction framework MLifts and their central relation for the datum E.radData l h, over the transported lower map ρ' := piBCiso⁻¹ ∘ ρ. These equivalences let d6 discharge half139_of's hlem86/hMcount directly from the source's lemma_8_6 and the 5.15/5.16 M-lift count.

noncomputable def GQ2.SectionEight.RecursionFrame.piBCisoSymm {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) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) : RF.YC →ₜ* RF.YB ⧸ D.M

piBCiso.symm : C → B/M as a continuous hom (finite discrete ⟹ continuous).

Equations

• RF.piBCisoSymm D hD = { toMonoidHom := (RF.piBCiso D hD).symm.toMonoidHom, continuous_toFun := ⋯ }

noncomputable def GQ2.SectionEight.RecursionFrame.rhoPrime {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (ρ : BoundaryLifts b F RF.TC) : Γ →ₜ* RF.YB ⧸ D.M

The transport ρ' := piBCiso⁻¹ ∘ ρ of a C-exact-image map to a B/M-valued lower map.

Equations

• RF.rhoPrime b F D hD ρ = (RF.piBCisoSymm D hD).comp ↑↑ρ

theorem GQ2.SectionEight.RecursionFrame.rhoPrime_apply {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (ρ : BoundaryLifts b F RF.TC) (γ : Γ) : (RF.rhoPrime b F D hD ρ) γ = (RF.piBCiso D hD).symm (↑↑ρ γ)

def GQ2.SectionEight.RecursionFrame.liftsOver_equiv {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (ρ : BoundaryLifts b F RF.TC) : RF.LiftsOver b F ρ ≃ MLifts D (RF.rhoPrime b F D hD ρ)

The LiftsOver ↔ MLifts bridge: B-lifts over ρ are the unrestricted M-lifts of the transported lower map ρ' (ker π_{BC} = M_B). Stated for any RadicalCoverData D with D.M = M_B (d6 uses D := E.radData l h, hD := rfl).

Equations

• RF.liftsOver_equiv b F D hD ρ = Equiv.subtypeEquivRight ⋯

def GQ2.SectionEight.RecursionFrame.centralOver_equiv {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) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (hC : D.C = RF.scalarCover l h) (ρ : BoundaryLifts b F RF.TC) : RF.CentralOver b F l h ρ ≃ { f : MLifts D (RF.rhoPrime b F D hD ρ) // MLifts.Central D f }

**The CentralOver ↔ central MLifts** bridge**: the λ-compatible lifts over ρare the centralM-lifts of ρ'(the scalar cover ofD). With D := E.radData l hthe scalar cover isRF.scalarCover l h`, so the predicates match on the nose.

Equations

• RF.centralOver_equiv b F l h D hD hC ρ = (RF.liftsOver_equiv b F D hD ρ).subtypeEquiv ⋯

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

• Lemma 8.6 = ⟦lem-radicaledge⟧