The strata boundary and the cocycle-law transport

theorem Q2Presentation.Induction.fibre_covers_mod_mChild {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) (y : (XRZero.xrChild chief K).fst.Y) : ∃ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (mChildKernel chief K).N) ((ProfiniteGrp.Hom.hom ↑f) γ) = (QuotientGroup.mk' (mChildKernel chief K).N) y

The fibre covers B modulo M' (support, §13-P8WL): the composite-to-C' surjectivity of a total-space point says exactly that its values fill B up to M'-corrections — and nothing more (weak lifts are genuinely non-surjective in general; any statement placing values beyond im(f)·M' is (W1)-content and is NOT asserted here).

theorem Q2Presentation.Induction.z1_law_transport {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v₀ v₁ : ↑GQ2Profinite.toProfinite.toTop → (XRZero.xrChild chief K).fst.Y) (hbase : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (mChildKernel chief K).N) (v₀ γ) = (QuotientGroup.mk' (mChildKernel chief K).N) (v₁ γ)) (u : ↑GQ2Profinite.toProfinite.toTop → (XRZero.xrChild chief K).fst.Y) (humem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), u γ ∈ (mChildKernel chief K).N) (hucoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), u (γ * γ') = (v₀ γ')⁻¹ * u γ * v₀ γ' * u γ') (γ γ' : ↑GQ2Profinite.toProfinite.toTop) : u (γ * γ') = (v₁ γ')⁻¹ * u γ * v₁ γ' * u γ'

(t1) The twisted-cocycle law transports across the fibre: value-functions with the same M'-classes induce the same conjugation on M'-valued tuples (M' abelian), so a Z¹-law at one weak lift holds at every weak lift with the same base.

(t2) The hom-level twist

noncomputable def Q2Presentation.Induction.localTwist {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) (u : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (humem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), u γ ∈ (mChildKernel chief K).N) (hucont : Continuous u) (hucoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), u (γ * γ') = ((ProfiniteGrp.Hom.hom ↑f) γ')⁻¹ * u γ * (ProfiniteGrp.Hom.hom ↑f) γ' * u γ') : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N boundaryPackage_GQ2 (XRZero.xrChild chief K).snd

The hom-level twist of a weak M-lift by an M'-valued cocycle (the presentation-free twistLift; construction mirrors liftHom_equiv_Z1.invFun): γ ↦ f(γ)·u(γ) is again a framed weak lift.

Equations

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

theorem Q2Presentation.Induction.localTwist_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) (u : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (humem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), u γ ∈ (mChildKernel chief K).N) (hucont : Continuous u) (hucoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), u (γ * γ') = ((ProfiniteGrp.Hom.hom ↑f) γ')⁻¹ * u γ * (ProfiniteGrp.Hom.hom ↑f) γ' * u γ') (γ : ↑GQ2Profinite.toProfinite.toTop) : (ProfiniteGrp.Hom.hom ↑(localTwist chief K f u humem hucont hucoc)) γ = (ProfiniteGrp.Hom.hom ↑f) γ * u γ

theorem Q2Presentation.Induction.localTwist_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) (u : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (humem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), u γ ∈ (mChildKernel chief K).N) (hucont : Continuous u) (hucoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), u (γ * γ') = ((ProfiniteGrp.Hom.hom ↑f) γ')⁻¹ * u γ * (ProfiniteGrp.Hom.hom ↑f) γ' * u γ') : TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 (XRZero.xrChild chief K).snd (localTwist chief K f u humem hucont hucoc) = TorsorProgram.coverLiftBase (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 (XRZero.xrChild chief K).snd f

The twist preserves the fibration base.

theorem Q2Presentation.Induction.localTwist_localTwist {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) (u : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (humem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), u γ ∈ (mChildKernel chief K).N) (hucont : Continuous u) (hucoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), u (γ * γ') = ((ProfiniteGrp.Hom.hom ↑f) γ')⁻¹ * u γ * (ProfiniteGrp.Hom.hom ↑f) γ' * u γ') (hucoc' : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), u (γ * γ') = ((ProfiniteGrp.Hom.hom ↑(localTwist chief K f u humem hucont hucoc)) γ')⁻¹ * u γ * (ProfiniteGrp.Hom.hom ↑(localTwist chief K f u humem hucont hucoc)) γ' * u γ') : localTwist chief K (localTwist chief K f u humem hucont hucoc) u humem hucont hucoc' = f

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

The flip Prop and the halving exit

def Q2Presentation.Induction.EdgeTwistFlipGQ2 {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 GQ2 twist-flip (hom-level; the §13-P8WL candidate-keep Prop): over every child surjection there is a T'-valued continuous tuple, a twisted cocycle at every weak lift of the fibre (transport by z1_law_transport), whose twist flips λ-liftability across the fibre. Manuscript content: lem:radicaledge step 6 at Γ = G_{ℚ₂} — prop:localduality perfectness + the variation computation; §13-P8WL records why this residue is not derivable from the current citable clauses ((W1)/(W2)).

Equations

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

theorem Q2Presentation.Induction.edgeHalvingGQ2_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)) (hflip : EdgeTwistFlipGQ2 chief K lam hinv) : EdgeHalvingGQ2 chief K lam hinv

(t3) The halving from the flip (hom-level mirror of edgeHalvingGammaA_of_twistFlip): a flipping T'-twist pairs the fibre involutively across λ-liftability, so exactly half of each fibre is λ-liftable. Either keep-2 endgame recovers q2_edgeHalving's statement through this exit.

(t4)/(t5): direction 1 and fibre-uniformity at the cover

theorem Q2Presentation.Induction.mem_tCover_iff_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) : x ∈ tCover chief K lam hinv ↔ (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) x ∈ tChild chief K

T̃ is the full p_λ-preimage of T' (support, §13-P8WL): the backward inclusion factors an arbitrary preimage through relN ≤ T̃.

theorem Q2Presentation.Induction.twist_lift_difference {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) (u : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y)).toProfinite.toTop) (humem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), u γ ∈ tChild chief K) (ft ft' : GQ2Profinite ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)) (hft : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) ((ProfiniteGrp.Hom.hom ft) γ) = (ProfiniteGrp.Hom.hom ↑f) γ) (hft' : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) ((ProfiniteGrp.Hom.hom ft') γ) = (ProfiniteGrp.Hom.hom ↑f) γ * u γ) : (∀ (γ : ↑GQ2Profinite.toProfinite.toTop), ((ProfiniteGrp.Hom.hom ft) γ)⁻¹ * (ProfiniteGrp.Hom.hom ft') γ ∈ tCover chief K lam hinv) ∧ (Continuous fun (γ : ↑GQ2Profinite.toProfinite.toTop) => ((ProfiniteGrp.Hom.hom ft) γ)⁻¹ * (ProfiniteGrp.Hom.hom ft') γ) ∧ (∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), ((ProfiniteGrp.Hom.hom ft) (γ * γ'))⁻¹ * (ProfiniteGrp.Hom.hom ft') (γ * γ') = ((ProfiniteGrp.Hom.hom ft) γ')⁻¹ * (((ProfiniteGrp.Hom.hom ft) γ)⁻¹ * (ProfiniteGrp.Hom.hom ft') γ) * (ProfiniteGrp.Hom.hom ft) γ' * (((ProfiniteGrp.Hom.hom ft) γ')⁻¹ * (ProfiniteGrp.Hom.hom ft') γ')) ∧ ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) (((ProfiniteGrp.Hom.hom ft) γ)⁻¹ * (ProfiniteGrp.Hom.hom ft') γ) = u γ

(t4) Flip direction 1 (both-liftable data ⟹ the twist lifts): the pointwise difference of a cover-lift of f and a cover-lift of its T'-twist is a T̃-valued continuous ft-cocycle projecting to u. The (W2)-converse is NOT asserted.

theorem Q2Presentation.Induction.cover_cocycle_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) (ft 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) ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) ((ProfiniteGrp.Hom.hom ft₁) γ))) (w : ↑GQ2Profinite.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y)).toProfinite.toTop) (hwmem : ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), w γ ∈ tCover chief K lam hinv) (hwcoc : ∀ (γ γ' : ↑GQ2Profinite.toProfinite.toTop), w (γ * γ') = ((ProfiniteGrp.Hom.hom ft) γ')⁻¹ * w γ * (ProfiniteGrp.Hom.hom ft) γ' * w γ') (γ γ' : ↑GQ2Profinite.toProfinite.toTop) : w (γ * γ') = ((ProfiniteGrp.Hom.hom ft₁) γ')⁻¹ * w γ * (ProfiniteGrp.Hom.hom ft₁) γ' * w γ'

(t5) Cover-cocycles are fibre-uniform (hom-level C-factorization): cover-value functions with the same M'-classes downstairs differ by M̃-elements, which act trivially on T̃ (mCover_conj_fix), so a T̃-valued cocycle law at one transports to the other.

(t6) The |X|-dichotomy: the dual pullback along T̃ ↠ T'

def Q2Presentation.Induction.tCoverProjMul {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) : ↥(tCoverKernel chief K lam hinv hne).N →* ↥(tChildKernel chief K).N

The projection T̃ → T' as a group hom (idiom: scalarRelProjMul; both carriers in the KERNEL-projection spelling so that the NAdd-headed instances fire reducibly — banked fix-class).

Equations

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

noncomputable def Q2Presentation.Induction.tCoverProjT {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.NAdd (tCoverKernel chief K lam hinv hne) →ₗ[ZMod 2] Lifting.NAdd (tChildKernel chief K)

The induced 𝔽₂-linear surjection NAdd T̃ →ₗ NAdd T' (idiom: scalarRelProj).

Equations

• Q2Presentation.Induction.tCoverProjT chief K lam hinv hne = { toFun := ⇑(MonoidHom.toAdditive (Q2Presentation.Induction.tCoverProjMul chief K lam hinv hne)), map_add' := ⋯, map_smul' := ⋯ }

theorem Q2Presentation.Induction.tCoverProjT_surjective {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) : Function.Surjective ⇑(tCoverProjT chief K lam hinv hne)

theorem Q2Presentation.Induction.tCoverProjT_eq_zero_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)) (hne : lam ≠ 0) (v : Lifting.NAdd (tCoverKernel chief K lam hinv hne)) : (tCoverProjT chief K lam hinv hne) v = 0 ↔ ↑(Additive.toMul v) ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N

The kernel of the projection is the deck line.

theorem Q2Presentation.Induction.tCoverProjT_conj {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) (v : Lifting.NAdd (tCoverKernel chief K lam hinv hne)) : (tCoverProjT chief K lam hinv hne) ((Lifting.conjEndN (tCoverKernel chief K lam hinv hne) y) v) = (Lifting.conjEndN (tChildKernel chief K) ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) y)) ((tCoverProjT chief K lam hinv hne) v)

The projection intertwines the conjugation operators.

noncomputable def Q2Presentation.Induction.pullbackInvDual {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.conjInvDuals (tChildKernel chief K))) : ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne))

The pullback of an invariant T'-dual is an invariant T̃-dual.

Equations

• Q2Presentation.Induction.pullbackInvDual chief K lam hinv hne φ = ⟨↑φ ∘ₗ Q2Presentation.Induction.tCoverProjT chief K lam hinv hne, ⋯⟩

theorem Q2Presentation.Induction.pullbackInvDual_injective {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) : Function.Injective (pullbackInvDual chief K lam hinv hne)

theorem Q2Presentation.Induction.invDual_kills_deck_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) (θ : ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne))) (v : Lifting.NAdd (tCoverKernel chief K lam hinv hne)) (hv : ↑(Additive.toMul v) ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) : ↑θ v = 0

Invariant T̃-duals kill the deck line at a nonzero edge (§12-P8W's dichotomy, dual reading): a nonzero value on the deck generator would produce a normal edge complement.

theorem Q2Presentation.Induction.pullbackInvDual_surjective_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) : Function.Surjective (pullbackInvDual chief K lam hinv hne)

The dual pullback is onto the invariant T̃-duals at a nonzero edge: an invariant dual kills the deck line, hence factors through the projection; the factor is invariant since the projection is onto and intertwines.

(t6) The ZeroEdge side: the deck functional of a normal complement

noncomputable def Q2Presentation.Induction.deckDual {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) (D : EdgeComplement chief K lam hinv) : Lifting.NAdd (tCoverKernel chief K lam hinv hne) → ZMod 2

The relN-coordinate reading along an edge complement.

Equations

• Q2Presentation.Induction.deckDual chief K lam hinv hne D v = Q2Presentation.Induction.relRead chief K lam hinv (Q2Presentation.Induction.edgeZ chief K lam hinv D hne ↑(Additive.toMul v) ⋯)

theorem Q2Presentation.Induction.deckDual_add {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) (D : EdgeComplement chief K lam hinv) (a b : Lifting.NAdd (tCoverKernel chief K lam hinv hne)) : deckDual chief K lam hinv hne D (a + b) = deckDual chief K lam hinv hne D a + deckDual chief K lam hinv hne D b

Additivity of the deck reading (unique-decomposition recombination).

noncomputable def Q2Presentation.Induction.deckDualLin {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) (D : EdgeComplement chief K lam hinv) : Module.Dual (ZMod 2) (Lifting.NAdd (tCoverKernel chief K lam hinv hne))

The deck reading as a linear functional.

Equations

• Q2Presentation.Induction.deckDualLin chief K lam hinv hne D = { toFun := Q2Presentation.Induction.deckDual chief K lam hinv hne D, map_add' := ⋯, map_smul' := ⋯ }

theorem Q2Presentation.Induction.deckDualLin_invariant {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) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (y : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (v : Lifting.NAdd (tCoverKernel chief K lam hinv hne)) : (deckDualLin chief K lam hinv hne D) ((Lifting.conjEndN (tCoverKernel chief K lam hinv hne) y) v) = (deckDualLin chief K lam hinv hne D) v

Normality makes the deck reading invariant: conjugation moves the W-component inside W and fixes the central relN-component.

theorem Q2Presentation.Induction.deckDualLin_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) (D : EdgeComplement chief K lam hinv) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hzrel : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) (hz1 : z ≠ 1) : (deckDualLin chief K lam hinv hne D) (Additive.ofMul ⟨z, ⋯⟩) = 1

The deck reading is 1 on the deck generator.

(t6) The |X|-dichotomy, assembled

theorem Q2Presentation.Induction.card_conjInvDuals_eq_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) : Nat.card ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne)) = Nat.card ↥(Lifting.conjInvDuals (tChildKernel chief K))

At a nonzero edge the pullback is a bijection: |X_{T̃}| = |X_{T'}|.

theorem Q2Presentation.Induction.card_conjInvDuals_ne_of_zeroEdge {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) (hzero : ZeroEdge chief K lam hinv) : Nat.card ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne)) ≠ Nat.card ↥(Lifting.conjInvDuals (tChildKernel chief K))

At zero edge the deck functional of a normal complement enlarges the invariant-dual space: the cards differ.

theorem Q2Presentation.Induction.nonzeroEdge_iff_conjInvDuals_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) : ¬ZeroEdge chief K lam hinv ↔ Nat.card ↥(Lifting.conjInvDuals (tCoverKernel chief K lam hinv hne)) = Nat.card ↥(Lifting.conjInvDuals (tChildKernel chief K))

(t6) The |X|-dichotomy (§13-P8WL): the edge is nonzero exactly when the invariant-dual spaces of T̃ and T' have the same size — the count-comparison input of the keep-2 endgame.