The twist datum and the twisted fibre point

def Q2Presentation.Induction.IsTwistCocycle {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) : Prop

A T'-twist datum at a weak M-lift: T'-valued, continuous, twisted cocycle for the lift's conjugation (the ETLC localTwist hypothesis triple, packaged).

Equations

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

noncomputable def Q2Presentation.Induction.twistPoint {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd

The twisted fibre point (ETLC localTwist, packaged at the twist datum).

Equations

• Q2Presentation.Induction.twistPoint chief K f v hv = Q2Presentation.Induction.localTwist chief K f v ⋯ ⋯ ⋯

theorem Q2Presentation.Induction.twistPoint_val {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) (γ : ↑GQ2Profinite.toProfinite.toTop) : (ProfiniteGrp.Hom.hom ↑(twistPoint chief K f v hv)) γ = (ProfiniteGrp.Hom.hom ↑f) γ * v γ

theorem Q2Presentation.Induction.twistPoint_base {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) : TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 (XRZero.xrChild chief K).snd (twistPoint chief K f v hv) = TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 (XRZero.xrChild chief K).snd f

theorem Q2Presentation.Induction.isTwistCocycle_of_fibre {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f f' : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (hbase : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) γ) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f') γ)) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) : IsTwistCocycle chief K f' v

(t1-package) The twist-datum condition is fibre-uniform (pointwise-M'-related lifts induce the same conjugation on T'; delegates to the ETLC transport).

theorem Q2Presentation.Induction.isTwistCocycle_twistPoint {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) : IsTwistCocycle chief K (twistPoint chief K f v hv) v

The twist datum survives its own twist (the twisted point is pointwise-M'-related to the original).

theorem Q2Presentation.Induction.twistPoint_twistPoint {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) (hv' : IsTwistCocycle chief K (twistPoint chief K f v hv) v) : twistPoint chief K (twistPoint chief K f v hv) v hv' = f

The twist is an involution on fibre points.

Cocycle algebra: products and pushes

theorem Q2Presentation.Induction.isTwistCocycle_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v w : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K f v) (hw : IsTwistCocycle chief K f w) : IsTwistCocycle chief K f fun (γ : ↑GQ2Profinite.toProfinite.toTop) => v γ * w γ

Twist data multiply (pointwise; T' is abelian).

noncomputable def Q2Presentation.Induction.coverTwist {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) (z : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)).toProfinite.toTop) (hmem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), z γ ∈ tCover chief K lam hinv) (hcont : Continuous z) (hcoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), z (γ * γ') = ((ProfiniteGrp.Hom.hom ft₀) γ')⁻¹ * z γ * (ProfiniteGrp.Hom.hom ft₀) γ' * z γ') : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)

The generic cover twist: a cover hom times a T̃-valued cocycle is a cover hom (the localTwist construction at the cover target).

Equations

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

theorem Q2Presentation.Induction.coverTwist_val {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) (z : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)).toProfinite.toTop) (hmem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), z γ ∈ tCover chief K lam hinv) (hcont : Continuous z) (hcoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), z (γ * γ') = ((ProfiniteGrp.Hom.hom ft₀) γ')⁻¹ * z γ * (ProfiniteGrp.Hom.hom ft₀) γ' * z γ') (γ : ↑GQ2Profinite.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (coverTwist chief K lam hinv ft₀ z hmem hcont hcoc)) γ = (ProfiniteGrp.Hom.hom ft₀) γ * z γ

theorem Q2Presentation.Induction.relN_proj_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (w : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hw : w ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) : (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) w = 1

Deck-kernel members project to 1 (motive-safe projection-level form of ker_scalarCoverProj).

theorem Q2Presentation.Induction.isTwistCocycle_push {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) (hbase : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (mChildKernel chief K).N) ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) ((ProfiniteGrp.Hom.hom ft₀) γ)) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) γ)) (z : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)).toProfinite.toTop) (hmem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), z γ ∈ tCover chief K lam hinv) (hcont : Continuous z) (hcoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), z (γ * γ') = ((ProfiniteGrp.Hom.hom ft₀) γ')⁻¹ * z γ * (ProfiniteGrp.Hom.hom ft₀) γ' * z γ') : IsTwistCocycle chief K f fun (γ : ↑GQ2Profinite.toProfinite.toTop) => (ProfiniteGrp.Hom.hom (scalarCoverProjHom chief K lam hinv)) (z γ)

The pushed cover cocycle is a twist datum downstairs: pushing a T̃-valued ft₀-cocycle along p_λ yields a T'-twist datum at any fibre point pointwise-M'-related to π ∘ ft₀.

The intrinsic invariant-dual bridges and the G1 counts

theorem Q2Presentation.Induction.conjEndN_tChild_eq_one_of_mChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (d : (XRZero.xrChild chief K).fst.Y) (hd : d ∈ (mChildKernel chief K).N) : Lifting.conjEndN (tChildKernel chief K) d = 1

M' centralizes T', operator form.

theorem Q2Presentation.Induction.mapInvDuals_tChild_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) : mapInvDuals (tChildKernel chief K) ↑f = Lifting.conjInvDuals (tChildKernel chief K)

The intrinsic bridge at the child: a fibre point acts through all of B on T' (its values cover B mod M', and M' acts trivially), so its intrinsic invariant duals are the target-level ones.

theorem Q2Presentation.Induction.twistCocycle_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) : Nat.card { v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop // IsTwistCocycle chief K f v } = Nat.card (Lifting.NAdd (tChildKernel chief K)) ^ 2 * Nat.card ↥(Lifting.conjInvDuals (tChildKernel chief K))

The G1 count at the child T'-kernel in target-level form.

theorem Q2Presentation.Induction.mapInvDuals_tCover_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) (hbase : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (mChildKernel chief K).N) ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) ((ProfiniteGrp.Hom.hom ft₀) γ)) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) γ)) : mapInvDuals (tCoverKernel chief K lam hinv hne) ft₀ = Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne)

The intrinsic bridge at the cover: a cover hom over a fibre point acts through all of B_λ on T̃ (M̃ acts trivially).

theorem Q2Presentation.Induction.coverZ1_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) (hbase : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (mChildKernel chief K).N) ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) ((ProfiniteGrp.Hom.hom ft₀) γ)) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) γ)) : Nat.card (weakZ1 (tCoverKernel chief K lam hinv hne) ft₀) = Nat.card (Lifting.NAdd (tCoverKernel chief K lam hinv hne)) ^ 2 * Nat.card ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne))

The G1 count at the cover T̃-kernel in target-level form.

theorem Q2Presentation.Induction.mapInvDuals_relN_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) : Nat.card ↥(mapInvDuals (Lifting.scalarRelKernel (xrKernel chief K) lam hinv) ft₀) = 2

Every dual is intrinsically invariant on the central deck kernel.

theorem Q2Presentation.Induction.weakZ1_relN_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (ft₀ : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) : Nat.card (weakZ1 (Lifting.scalarRelKernel (xrKernel chief K) lam hinv) ft₀) = 8

The 8 — the weak-base deck-cocycle count at any cover hom.

theorem Q2Presentation.Induction.card_NAdd_tCover {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) : Nat.card (Lifting.NAdd (tCoverKernel chief K lam hinv hne)) = 2 * Nat.card (Lifting.NAdd (tChildKernel chief K))

The deck-line index: |NAdd T̃| = 2 · |NAdd T'| (rank–nullity of the ETLC projection, whose kernel is the two-element deck line).

The lift set of a twisted point and its 8-count

def Q2Presentation.Induction.LiftSetV {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) : Type

The framed cover-lift set over the (value-level) v-twist of x.

Equations

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

theorem Q2Presentation.Induction.liftSetV_nonempty_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K x v) : Nonempty (LiftSetV chief K lam hinv x v) ↔ coverLiftableWeak chief K lam hinv boundaryPackage_GQ2 (twistPoint chief K x v hv)

Liftability of the twisted point is nonemptiness of the lift set.

theorem Q2Presentation.Induction.liftSetV_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (ft₀ : LiftSetV chief K lam hinv x v) : Nat.card (LiftSetV chief K lam hinv x v) = 8

The anchored 8-count of the lift set (the deck torsor + clause (d) at the deck kernel).

The twist–lift pair space and its anchored cover-torsor count

def Q2Presentation.Induction.WCPairs {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) : Type

Pairs (twist datum, framed cover lift of the twisted point).

Equations

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

theorem Q2Presentation.Induction.wcPairs_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (v₀ : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv₀ : IsTwistCocycle chief K x v₀) (ft₀ : LiftSetV chief K lam hinv x v₀) : Nat.card (WCPairs chief K lam hinv x) = Nat.card (Lifting.NAdd (tCoverKernel chief K lam hinv hne)) ^ 2 * Nat.card ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne))

The anchored cover-torsor count of the pair space: with one reach witness (v₀, ft₀), the pairs biject with the T̃-cocycles at ft₀, so their number is |T̃|²·|X_{T̃}| (clause (d) at the cover + the intrinsic bridge).

Finiteness and the per-point counting identity

theorem Q2Presentation.Induction.finite_twistCocycleSubtype {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (P : (↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) → Prop) (hP : ∀ (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop), P v → IsTwistCocycle chief K x v) : Finite { v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop // P v }

theorem Q2Presentation.Induction.wcPairs_card_eq_eight_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) : Nat.card (WCPairs chief K lam hinv x) = 8 * Nat.card { v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop // ∃ (hv : IsTwistCocycle chief K x v), coverLiftableWeak chief K lam hinv boundaryPackage_GQ2 (twistPoint chief K x v hv) }

The pair space fibres over the liftable twist data with the 8-element lift sets.

theorem Q2Presentation.Induction.twLift_card_eight {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (x : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd) (hx : ∃ (v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (hv : IsTwistCocycle chief K x v), coverLiftableWeak chief K lam hinv boundaryPackage_GQ2 (twistPoint chief K x v hv)) : 8 * Nat.card { v : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop // ∃ (hv : IsTwistCocycle chief K x v), coverLiftableWeak chief K lam hinv boundaryPackage_GQ2 (twistPoint chief K x v hv) } = Nat.card (Lifting.NAdd (tCoverKernel chief K lam hinv hne)) ^ 2 * Nat.card ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne))

The per-point master identity (needs one reach witness): eight times the liftable-twist count is the cover-cocycle count.

The reach Prop and the halving exit

def Q2Presentation.Induction.EdgeTwistReachGQ2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : Prop

The twist-reach clause (the §13-P8WL/§14-S8 minimal keep shape): every weak M-lift admits SOME λ-liftable T'-twist. This is the irreducible variation-onto residue of prop:localduality-perfectness (wall (W2)); everything else in the local R4a halving is counting.

Equations

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

theorem Q2Presentation.Induction.edgeHalvingGQ2_of_twistReach {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hedge : ¬ZeroEdge chief K lam hinv) (hreach : EdgeTwistReachGQ2 chief K lam hinv) : EdgeHalvingGQ2 chief K lam hinv

Keep 2 dissolved modulo the reach clause (§14-S8.2): the R4a per-fibre halving on the local side, by the Im-index count — G1 (clause (d)) at the cover/child/deck kernels, the intrinsic bridges, the |T̃| = 2·|T'| deck index, and the (t6) dichotomy; the twist involution exchanges the pair spaces; direction-2/variation content enters ONLY through hreach.