Frame facts for the T̃-family at a cover marking

theorem Q2Presentation.Induction.conjEndN_tCover_eq_one_of_central {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) (hy : y ∈ Subgroup.center (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : Lifting.conjEndN (tCoverKernel chief K lam hinv hne) y = 1

Central elements of the cover act trivially on the T̃-kernel.

theorem Q2Presentation.Induction.tCover_relator_op_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) (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) : Lifting.conjEndN (tCoverKernel chief K lam hinv hne) (w.eval q) = 1

Relator operators are trivial on T̃: relator values of a cover marking are deck elements, and the deck kernel is central.

theorem Q2Presentation.Induction.cover_tame_relation {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) : rconj ((Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).piY (q Gen.tau)) ((Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).piY (q Gen.sigma)) = (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).piY (q Gen.tau) ^ 2

The tame relation at the cover's tame quotient (mirror of mChild_tame_relation): the tame relator defect lies in relN ≤ L_{B_λ}, hence dies under π̃.

theorem Q2Presentation.Induction.cover_card_four {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) : 4 ∣ Nat.card (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

4 divides the cover order: |B_λ| = |B| · 2 (kernel–quotient count at ker p_λ = relN) and 4 ∣ |B| (mChild_card_Y_four).

theorem Q2Presentation.Induction.tCover_marking_covers {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) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯) (TorsorProgram.quotientFrame (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ (XRZero.xrChild chief K).snd)) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mChildKernel chief K).N) (fMarking chief K f₀ a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (y : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : ∃ c ∈ Subgroup.closure (Set.range q), y * c⁻¹ ∈ mCover chief K lam hinv

The cover marking covers B_λ modulo M̃ (mChild_marking_covers pushed through p_λ; the closure transfers by MonoidHom.map_closure).

theorem Q2Presentation.Induction.tCover_dual_invariant_of_kills {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) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯) (TorsorProgram.quotientFrame (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ (XRZero.xrChild chief K).snd)) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mChildKernel chief K).N) (fMarking chief K f₀ a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (θ : Module.Dual (ZMod 2) (Lifting.NAdd (tCoverKernel chief K lam hinv hne))) (hkill : ∀ x ∈ Lifting.markedAug (Lifting.conjFamily (tCoverKernel chief K lam hinv hne)) q, θ x = 0) (y : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (v : Lifting.NAdd (tCoverKernel chief K lam hinv hne)) : θ ((Lifting.conjEndN (tCoverKernel chief K lam hinv hne) y) v) = θ v

Killing the marked window upgrades to full conjugation-invariance: every operator agrees with a marked-closure operator (M̃ acts trivially, and the marking covers B_λ modulo M̃).

The dichotomy half: a separating invariant functional yields ZeroEdge

def Q2Presentation.Induction.thetaComplement {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) (θ : Module.Dual (ZMod 2) (Lifting.NAdd (tCoverKernel chief K lam hinv hne))) : Subgroup (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

The kernel of a T̃-functional, as a subgroup of the cover.

Equations

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

theorem Q2Presentation.Induction.zeroEdge_of_separating_dual {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) (θ : Module.Dual (ZMod 2) (Lifting.NAdd (tCoverKernel chief K lam hinv hne))) (hinvθ : ∀ (y : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (v : Lifting.NAdd (tCoverKernel chief K lam hinv hne)), θ ((Lifting.conjEndN (tCoverKernel chief K lam hinv hne) y) v) = θ v) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hzrel : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hzθ : θ (Additive.ofMul ⟨z, ⋯⟩) = 1) : ZeroEdge chief K lam hinv

A conjugation-invariant functional separating the deck generator yields a NORMAL edge complement (lem:radicaledge step 3, dual form): its kernel inside T̃ is conjugation-stable, meets relN trivially, and fills T̃ together with relN.

The diamond hits the anti-diagonal deck pair

theorem Q2Presentation.Induction.deck_shadow_witness {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) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯) (TorsorProgram.quotientFrame (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ (XRZero.xrChild chief K).snd)) (f₀ : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GammaA (XRZero.xrChild chief K).snd) (hf₀ : TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA (XRZero.xrChild chief K).snd f₀ = g) (hedge : ¬ZeroEdge chief K lam hinv) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hzrel : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) : ∃ (t : Gen → Lifting.NAdd (tCoverKernel chief K lam hinv hne)), Lifting.foxShadow (tCoverKernel chief K lam hinv hne) (coverMarkingOf chief K lam hinv f₀) t Q2Word.tameRelator = Additive.ofMul ⟨z, ⋯⟩ ∧ Lifting.foxShadow (tCoverKernel chief K lam hinv hne) (coverMarkingOf chief K lam hinv f₀) t Q2Word.wildRelator = 0

The deck-shadow witness: at a nonzero edge, some T̃-tuple has relator rows exactly (z, 0) at the canonical cover marking of a fibre point. Step 1 (dichotomy): ¬ ZeroEdge forces the deck generator into the marked augmentation window — else a separating functional builds a normal complement (zeroEdge_of_separating_dual). Step 2: diamondAtW_all at the top window (faithfulness from hfaithNT_of_frame) converts the membership into a row preimage.

Deck-valued shadows give relator cocycles of pairing 1

theorem Q2Presentation.Induction.pushed_eval_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) (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) (tt : Gen → ↥(tCover chief K lam hinv)) (w : GExpr) (hw : (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom ↑f₀) (gammaGen a)) = 1) (hsmem : ↑(Additive.toMul (Lifting.foxShadow (tCoverKernel chief K lam hinv hne) q (fun (a : Gen) => Additive.ofMul (tt a)) w)) ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) : w.eval (Lifting.perturb (mChildKernel chief K) (fMarking chief K f₀) (tPushTuple chief K lam hinv tt)) = 1

Pushed perturbed relator evaluation: if a relator's T̃-shadow at a cover marking is deck-valued, the corresponding perturbation of the CHILD marking still kills the relator (push eval_perturb through p_λ, whose kernel is exactly the deck kernel).

theorem Q2Presentation.Induction.twistCocycle_of_deck {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) (tt : Gen → ↥(tCover chief K lam hinv)) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hzrel : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hst : ↑(Additive.toMul (Lifting.foxShadow (tCoverKernel chief K lam hinv hne) q (fun (a : Gen) => Additive.ofMul (tt a)) Q2Word.tameRelator)) = z) (hsw : ↑(Additive.toMul (Lifting.foxShadow (tCoverKernel chief K lam hinv hne) q (fun (a : Gen) => Additive.ofMul (tt a)) Q2Word.wildRelator)) = 1) : TwistCocycle chief K lam hinv f₀ tt

A tuple with deck-valued relator shadows is a relator cocycle: the pushed M'-shadows vanish (foxShadow_eq_zero_of_eval_eq downstairs).

theorem Q2Presentation.Induction.edgePairing_eq_one_of_deck {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) (tt : Gen → ↥(tCover chief K lam hinv)) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hz1 : z ≠ 1) (hst : ↑(Additive.toMul (Lifting.foxShadow (tCoverKernel chief K lam hinv hne) q (fun (a : Gen) => Additive.ofMul (tt a)) Q2Word.tameRelator)) = z) (hsw : ↑(Additive.toMul (Lifting.foxShadow (tCoverKernel chief K lam hinv hne) q (fun (a : Gen) => Additive.ofMul (tt a)) Q2Word.wildRelator)) = 1) : edgePairing chief K lam hinv hne q tt = 1

The pairing of a deck-shadow tuple is 1: relRead z + relRead 1 with z the nontrivial deck element.

The exit: keep 1 as a theorem

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

EdgeTwistFlip from ¬ ZeroEdge — the statement of the interim keep sec7_edgeTwistFlip_gammaA, proven: over every child surjection some weak M-lift carries a relator cocycle of edge pairing 1. The manuscript's [ε̄] ≠ 0 ⟹ degree-one-duality nonvanishing (lem:radicaledge step 6, l.4006–4019) is realized by the (♦)-dévissage: ¬ ZeroEdge places the deck generator in the marked augmentation window (else a separating invariant functional's kernel is a normal complement), and the diamond produces a T̃-tuple with relator rows (z, 0) — a TwistCocycle of pairing relRead z = 1.