Generic counting and Fox-calculus helpers

theorem Q2Presentation.Induction.eval_mul_mem {Yt : BoundaryFramedTarget} (H : Subgroup Yt.Y) [H.Normal] (q : Marking Yt.Y) (m : Gen → Yt.Y) (hm : ∀ (a : Gen), m a ∈ H) (w : GExpr) : ∃ h ∈ H, (w.eval fun (a : Gen) => q a * m a) = w.eval q * h

Words evaluated at an H-translated marking differ by an H-element (GExpr.eval_map through the H-quotient; no induction needed).

theorem Q2Presentation.Induction.foxShadow_mul_fix {Yt : BoundaryFramedTarget} (E : Lifting.ElementaryKernel Yt) (H : Subgroup Yt.Y) [H.Normal] (hfix : ∀ h ∈ H, Lifting.conjEndN E h = 1) (q : Marking Yt.Y) (m : Gen → Yt.Y) (hm : ∀ (a : Gen), m a ∈ H) (n : Gen → Lifting.NAdd E) (w : GExpr) : Lifting.foxShadow E (fun (a : Gen) => q a * m a) n w = Lifting.foxShadow E q n w

Shadow invariance under conjugation-trivial translations: if every H-element acts trivially on the kernel module, translating the marking by an H-tuple leaves every Fox shadow unchanged (the foxShadow_perturb_eq induction, at a translating subgroup instead of the kernel itself).

The T̃-kernel of the cover and the operator trivialities

def Q2Presentation.Induction.tCoverKernel {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) : Lifting.ElementaryKernel (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv)

T̃ ≤ B_λ as an elementary kernel (lem:radicaledge step 1 packaged): normal, wild, θ-dead, abelian of exponent 2 — the carrier of the twist calculus at the cover.

Equations

• Q2Presentation.Induction.tCoverKernel chief K lam hinv hne = { N := Q2Presentation.Induction.tCover chief K lam hinv, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

theorem Q2Presentation.Induction.conjEndN_relKernel_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)) (hne : lam ≠ 0) (y : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : Lifting.conjEndN (Lifting.scalarRelKernel (xrKernel chief K) lam hinv) y = 1

The deck kernel is central, so every conjugation operator on it is trivial.

theorem Q2Presentation.Induction.conjEndN_tCover_eq_one_of_mCover {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) (h : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hh : h ∈ mCover chief K lam hinv) : Lifting.conjEndN (tCoverKernel chief K lam hinv hne) h = 1

M̃-conjugation is trivial on the T̃-kernel (mCover_conj_fix, operator form) — the fibre-uniformity input.

theorem Q2Presentation.Induction.cover_omega2_odd {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) : Odd (omega2Mod (Nat.card (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)).val

The ω₂-residue at the cover order is odd (the deck kernel has order 2, so 2 ∣ |B_λ|).

The deck-kernel Fox collapse

theorem Q2Presentation.Induction.foxShadow_relKernel_collapse {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) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (n : Gen → Lifting.NAdd (Lifting.scalarRelKernel (xrKernel chief K) lam hinv)) (w : GExpr) : Lifting.foxShadow (Lifting.scalarRelKernel (xrKernel chief K) lam hinv) q n w = ∑ g : Gen, Lifting.expSum g w • n g

Central-kernel Fox collapse: all operators on the deck kernel are trivial, so any shadow is the exponent-sum diagonal (the relative fixed-shadow lemma at W := ⊤, floor ⊥).

theorem Q2Presentation.Induction.foxShadow_relKernel_relator {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) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (n : Gen → Lifting.NAdd (Lifting.scalarRelKernel (xrKernel chief K) lam hinv)) (w : GExpr) (hτ : Lifting.expSum Gen.tau w = 1) (hσ : Lifting.expSum Gen.sigma w = 0) (h0 : Lifting.expSum Gen.x0 w = 0) (h1 : Lifting.expSum Gen.x1 w = 0) : Lifting.foxShadow (Lifting.scalarRelKernel (xrKernel chief K) lam hinv) q n w = n Gen.tau

The deck-kernel shadow of either relator is the τ-slot.

theorem Q2Presentation.Induction.eval_perturb_relKernel {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) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (n : Gen → ↥(Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (w : GExpr) (hτ : Lifting.expSum Gen.tau w = 1) (hσ : Lifting.expSum Gen.sigma w = 0) (h0 : Lifting.expSum Gen.x0 w = 0) (h1 : Lifting.expSum Gen.x1 w = 0) : w.eval (Lifting.perturb (Lifting.scalarRelKernel (xrKernel chief K) lam hinv) q n) = w.eval q * ↑(n Gen.tau)

Deck-kernel perturbations shift a relator value by exactly the τ-slot.

theorem Q2Presentation.Induction.relRead_inj {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) {z z' : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y} (hz : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hz' : z' ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (h : relRead chief K lam hinv z = relRead chief K lam hinv z') : z = z'

The two-element deck kernel is read injectively by relRead.

Cover markings and the obstruction bit

theorem Q2Presentation.Induction.quotient_qYMap_mk {Yt : BoundaryFramedTarget} (N : Subgroup Yt.Y) [N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (y : Yt.Y) : (TorsorProgram.quotientFramedTarget Yt N hNLY hNθ).qYMap ((QuotientGroup.mk' N) y) = Yt.qYMap y

Framing readout of a quotient framed target on a projected element.

def Q2Presentation.Induction.CoverMarking {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_GammaA (XRZero.xrChild chief K).snd) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : Prop

A cover marking over a weak M-lift: generator values in B_λ projecting to the lift's marking, framed by the parent frame.

Equations

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

theorem Q2Presentation.Induction.scalarCover_qYMap {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 : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).qYMap x = (XRZero.xrChild chief K).fst.qYMap ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) x)

Cover framing is the child framing of the projection.

noncomputable def Q2Presentation.Induction.coverMarkingOf {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_GammaA (XRZero.xrChild chief K).snd) : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

Every weak M-lift carries a cover marking (choice of p_λ-preimages; framing descends).

Equations

• Q2Presentation.Induction.coverMarkingOf chief K lam hinv f a = Classical.choose ⋯

theorem Q2Presentation.Induction.coverMarkingOf_spec {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_GammaA (XRZero.xrChild chief K).snd) : CoverMarking chief K lam hinv f (coverMarkingOf chief K lam hinv f)

theorem Q2Presentation.Induction.coverMarking_mem_LY {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_GammaA (XRZero.xrChild chief K).snd) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) (a : Gen) (ha : (ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen a) = 1) : q a ∈ (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).LY

Wild generator values of a cover marking land in the cover's L_Y (the frame pins the tame coordinate).

theorem Q2Presentation.Induction.coverMarking_eval_mem {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_GammaA (XRZero.xrChild chief K).snd) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) (w : GExpr) (hw : (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom ↑f) (gammaGen a)) = 1) : w.eval q ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N

Relator values of a cover marking lie in the deck kernel.

def Q2Presentation.Induction.scalarCoverProjHom {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)) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)

The cover projection as a hom of finite discrete profinite groups (the stratumInclHom idiom).

Equations

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

noncomputable def Q2Presentation.Induction.obRead {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)) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : ZMod 2

The obstruction bit of a cover marking: the relRead-sum of the two relator defects (eq:edgevariationobstruction's ob, in-tree form).

Equations

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

theorem Q2Presentation.Induction.obRead_eq_of_coverMarking {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_GammaA (XRZero.xrChild chief K).snd) (q q' : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) (hq' : CoverMarking chief K lam hinv f q') : obRead chief K lam hinv q = obRead chief K lam hinv q'

obRead is well-defined on the lift: any two cover markings over the same weak M-lift differ by a deck-kernel perturbation, which shifts both defects by the same τ-slot — the sum is invariant.

theorem Q2Presentation.Induction.coverLiftableWeak_iff_obRead_zero {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_GammaA (XRZero.xrChild chief K).snd) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) : coverLiftableWeak chief K lam hinv boundaryPackage_GammaA f ↔ obRead chief K lam hinv q = 0

The marking-level liftability criterion (lem:radicaledge's ob(f) = 0 ⟺ liftable, in-tree): a weak M-lift is λ-liftable iff the obstruction bit of any cover marking over it vanishes.

The variation formula and the edge pairing

noncomputable def Q2Presentation.Induction.edgePairing {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) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (t : Gen → ↥(tCover chief K lam hinv)) : ZMod 2

The edge pairing ⟨[u], ρ*[ε̄]⟩ of a T̃-tuple against the two relators at a cover marking: the relRead-sum of the two T̃-shadows (eq:edgevariationobstruction's correction term, ledger form).

Equations

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

theorem Q2Presentation.Induction.obRead_perturb_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) (f f' : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) (t : Gen → ↥(tCover chief K lam hinv)) (hq' : CoverMarking chief K lam hinv f' (Lifting.perturb (tCoverKernel chief K lam hinv hne) q t)) : obRead chief K lam hinv (Lifting.perturb (tCoverKernel chief K lam hinv hne) q t) = obRead chief K lam hinv q + edgePairing chief K lam hinv hne q t

The exact variation formula (eq:edgevariationobstruction, lem:radicaledge steps 5–6): perturbing a cover marking by a T̃-tuple shifts the obstruction bit by exactly the edge pairing. Both markings must lie over weak M-lifts (so all four defects live in the deck kernel).

Fibre-uniformity of the pairing

theorem Q2Presentation.Induction.mem_mCover_of_proj {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 : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hx : (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) x ∈ mChild chief K) : x ∈ mCover chief K lam hinv

Cover elements projecting into M' lie in M̃.

theorem Q2Presentation.Induction.edgePairing_eq_of_fibre {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 f' : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd) (q q' : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) (hq' : CoverMarking chief K lam hinv f' q') (hbase : ∀ (a : Gen), (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) (gammaGen a)) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f') (gammaGen a))) (t : Gen → ↥(tCover chief K lam hinv)) : edgePairing chief K lam hinv hne q' t = edgePairing chief K lam hinv hne q t

The pairing is fibre-uniform (lem:radicaledge step 4, ledger form): markings over lifts with the same child image differ by an M̃-tuple, and M̃-conjugation fixes T̃, so the two T̃-shadows — hence the pairing — agree. This is the C-factorization of the edge class.

The twist involution on the fibre

def Q2Presentation.Induction.fMarking {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd) : Marking (XRZero.xrChild chief K).fst.Y

The generator marking of a weak M-lift.

Equations

• Q2Presentation.Induction.fMarking chief K f a = (ProfiniteGrp.Hom.hom ↑f) (Q2Presentation.gammaGen a)

def Q2Presentation.Induction.tCoverPush {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)) (t : ↥(tCover chief K lam hinv)) : ↥(mChildKernel chief K).N

A T̃-element pushed down to the child M-kernel (T̃ ↠ T' ≤ M').

Equations

• Q2Presentation.Induction.tCoverPush chief K lam hinv t = ⟨(Q2Presentation.Lifting.scalarCoverProj (Q2Presentation.Induction.xrKernel chief K) lam hinv) ↑t, ⋯⟩

def Q2Presentation.Induction.tPushTuple {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)) (t : Gen → ↥(tCover chief K lam hinv)) : Gen → ↥(mChildKernel chief K).N

The pushed tuple of a T̃-tuple.

Equations

• Q2Presentation.Induction.tPushTuple chief K lam hinv t a = Q2Presentation.Induction.tCoverPush chief K lam hinv (t a)

def Q2Presentation.Induction.TwistCocycle {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) : Prop

A relator cocycle: a T̃-tuple whose pushed M'-shadow kills both relators at the lift's marking — exactly the twists preserving hom-ness (the marking form of Z¹_{Γ,ρ}(T)).

Equations

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

theorem Q2Presentation.Induction.twistMarking_relator_eval {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (w : GExpr) (hsh : Lifting.foxShadow (mChildKernel chief K) (fMarking chief K f) (fun (a : Gen) => Additive.ofMul (tPushTuple chief K lam hinv t a)) w = 0) (hw : w.eval (fMarking chief K f) = 1) : w.eval (Lifting.perturb (mChildKernel chief K) (fMarking chief K f) (tPushTuple chief K lam hinv t)) = 1

The twisted marking kills a relator the lift kills, when the shadow vanishes.

theorem Q2Presentation.Induction.twistMarking_admissible {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) : Admissible (Lifting.anyMarking (Lifting.perturb (mChildKernel chief K) (fMarking chief K f) (tPushTuple chief K lam hinv t)))

The twisted marking is admissible.

noncomputable def Q2Presentation.Induction.twistLift {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd

The twist of a weak M-lift by a relator cocycle — again a weak M-lift (the f ↦ f_u of lem:radicaledge step 5, marking form).

Equations

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

theorem Q2Presentation.Induction.twistLift_val_gammaGen {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) (a : Gen) : (ProfiniteGrp.Hom.hom ↑(twistLift chief K lam hinv f t hcoc)) (gammaGen a) = fMarking chief K f a * ↑(tPushTuple chief K lam hinv t a)

theorem Q2Presentation.Induction.twistLift_mk_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)) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) (γ : ↑GammaA.toProfinite.toTop) : (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑(twistLift chief K lam hinv f t hcoc)) γ) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) γ)

The twist does not move the child image.

theorem Q2Presentation.Induction.twistLift_base {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) : TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA (XRZero.xrChild chief K).snd (twistLift chief K lam hinv f t hcoc) = TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA (XRZero.xrChild chief K).snd f

The twist preserves the fibration base.

theorem Q2Presentation.Induction.twistLift_twistLift {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_GammaA (XRZero.xrChild chief K).snd) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) (hcoc' : TwistCocycle chief K lam hinv (twistLift chief K lam hinv f t hcoc) t) : twistLift chief K lam hinv (twistLift chief K lam hinv f t hcoc) t hcoc' = f

The twist is an involution (T'-values square to 1).

theorem Q2Presentation.Induction.coverMarking_twist {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_GammaA (XRZero.xrChild chief K).snd) (q : Marking (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hq : CoverMarking chief K lam hinv f q) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) : CoverMarking chief K lam hinv (twistLift chief K lam hinv f t hcoc) (Lifting.perturb (tCoverKernel chief K lam hinv hne) q t)

Perturbing a cover marking by a T̃-tuple yields a cover marking of the twisted lift.

theorem Q2Presentation.Induction.twistCocycle_of_fibre {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 f' : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd) (hbase : ∀ (a : Gen), (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) (gammaGen a)) = (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f') (gammaGen a))) (t : Gen → ↥(tCover chief K lam hinv)) (hcoc : TwistCocycle chief K lam hinv f t) : TwistCocycle chief K lam hinv f' t

The cocycle condition is fibre-uniform (rowMap_perturb_eq): lifts with the same child image share their relator cocycles.

The conditional halving exit

def Q2Presentation.Induction.EdgeTwistFlip {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) : Prop

The isolated nonvanishing residue (lem:radicaledge step 6's [ε̄] ≠ 0 ⟹ perfect-degree-one-duality clause): over every child surjection, SOME weak M-lift carries a relator cocycle of nonzero edge pairing. This — not the halving itself — is the remaining content of sec7_edgeHalving_gammaA; dissolution program in audit/BLOCKR_P8_DESIGN.md §10-P8D.

Equations

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

theorem Q2Presentation.Induction.edgeHalvingGammaA_of_twistFlip {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) (hflip : EdgeTwistFlip chief K lam hinv hne) : EdgeHalvingGammaA chief K lam hinv

The per-g halving from a flipping twist (lem:radicaledge step 6 + prop:nonzeroedge's per-fibre clause): a relator cocycle with nonzero pairing twists the fibre involutively and flips the obstruction bit, so exactly half of each fibre is λ-liftable. This dissolves the halving content of sec7_edgeHalving_gammaA down to EdgeTwistFlip.