The B/T' framed pair and its V-layer

def Q2Presentation.Induction.btChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : FramedPair

The B/T'-child: the framed pair the descended cover covers (lem:transgression's base, manuscript l.4032–4034; the quotient of the child by the radical layer T').

Equations

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

def Q2Presentation.Induction.vLayer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup (btChild chief K).fst.Y

The V-layer of B/T': the image of M' (≅ V = M/T via the tower collapses; the kernel of B/T' ↠ C).

Equations

• Q2Presentation.Induction.vLayer chief K = Subgroup.map (QuotientGroup.mk' (Q2Presentation.Induction.tChild chief K)) (Q2Presentation.Induction.mChild chief K)

instance Q2Presentation.Induction.vLayer_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (vLayer chief K).Normal

def Q2Presentation.Induction.cChildCollapse {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (cChild chief K).fst.Y ≃* towerC K

The C-child collapse as a hygiene def at the cChild carrier (the banked mixed-defeq-carrier fix-class): B/M' ≃* C = Y/K. Only its map_one/map_mul are consumed (the Delta transport laws).

Equations

• Q2Presentation.Induction.cChildCollapse chief K = Q2Presentation.Induction.mChildCollapse chief K

theorem Q2Presentation.Induction.muT_int {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↑(muT chief K) = 2 ^ dimV chief K * 2 ^ (2 * dimT chief K + rT chief K)

μ as a ℤ-value (eq:mumultiplicity, the target-side VALUE |B¹(V)|·|Z¹(T)| = 2^d·2^{2·dimT+r} — P3-U2's muT; the per-source realization of the count is the affine-lifting dissolution lane).

The head V = M/T: descended action and descended form

def Q2Presentation.Induction.headActE {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) : towerM K ⧸ towerT K →ₗ[ZMod 2] towerM K ⧸ towerT K

The descended C-action on the head V = M/T (towerActM mod the stable radical layer, via Submodule.mapQ).

Equations

• Q2Presentation.Induction.headActE chief K c = (Q2Presentation.Induction.towerT K).mapQ (Q2Presentation.Induction.towerT K) ↑((Q2Presentation.Induction.towerActM K) c) ⋯

@[simp]

theorem Q2Presentation.Induction.headActE_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (m : towerM K) : (headActE chief K c) (Submodule.Quotient.mk m) = Submodule.Quotient.mk (((towerActM K) c) m)

theorem Q2Presentation.Induction.headActE_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : (headActE chief K 1) v = v

theorem Q2Presentation.Induction.headActE_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c d : towerC K) (v : towerM K ⧸ towerT K) : (headActE chief K (c * d)) v = (headActE chief K c) ((headActE chief K d) v)

theorem Q2Presentation.Induction.headActE_cancel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (v : towerM K ⧸ towerT K) : (headActE chief K c) ((headActE chief K c⁻¹) v) = v

theorem Q2Presentation.Induction.edgeHeadAnn {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) : Annihilates (sec7SquareFamily chief K lam) (towerT K)

The λ-composed square family annihilates T (the proven crux clauses q_λ|_T = 0, b_λ(T,M) = 0, through the invariance bridge; hinv is consumed by the proof only — included so the signature carries the uniform (chief K lam hinv hne) slot order of every call site).

def Q2Presentation.Induction.edgeHeadForm {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) : Quadratic.QuadF2 (towerM K ⧸ towerT K)

The descended head form q̄_λ : QuadF2 (M/T) (prop:simpleheaddet at the tower, the U1-aligned carrier of the R4b Gauss data).

Equations

• Q2Presentation.Induction.edgeHeadForm chief K lam hinv hne = ⋯.descend

theorem Q2Presentation.Induction.edgeHeadForm_nonsingular {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) : (edgeHeadForm chief K lam hinv hne).Nonsingular

q̄_λ is nonsingular (crux radical clause: polar radical = T).

theorem Q2Presentation.Induction.edgeHead_nontrivial {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nontrivial (towerM K ⧸ towerT K)

The head is nontrivial (towerT_ne_top, hR-free) — the [Nontrivial V] guard of the P6 Dickson pinning holds at the R4b head.

theorem Q2Presentation.Induction.edgeHeadForm_form_act {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) (c : towerC K) (v : towerM K ⧸ towerT K) : (edgeHeadForm chief K lam hinv hne).form ((headActE chief K c) v) = (edgeHeadForm chief K lam hinv hne).form v

theorem Q2Presentation.Induction.edgeHeadForm_polar_act {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) (c : towerC K) (v w : towerM K ⧸ towerT K) : ((edgeHeadForm chief K lam hinv hne).polar ((headActE chief K c) v)) ((headActE chief K c) w) = ((edgeHeadForm chief K lam hinv hne).polar v) w

theorem Q2Presentation.Induction.edgeHeadForm_polar_adjoint {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) (c : towerC K) (v w : towerM K ⧸ towerT K) : ((edgeHeadForm chief K lam hinv hne).polar ((headActE chief K c) v)) w = ((edgeHeadForm chief K lam hinv hne).polar v) ((headActE chief K c⁻¹) w)

Polar equivariance in adjoint form: b(c·v, w) = b(v, c⁻¹·w).

The bilinear normalized factor set f of κ_q⁰

(eq:basekappacochain's fibre data, chosen BILINEAR via Quadratic.polarization so the factor-set 2-cocycle law is automatic)

def Q2Presentation.Induction.edgeBaseFactor {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) : towerM K ⧸ towerT K →ₗ[ZMod 2] towerM K ⧸ towerT K →ₗ[ZMod 2] ZMod 2

f: the bilinear factor set of the base determinant model — f(v,v) = q̄(v), f(v,w) + f(w,v) = b_q̄(v,w) (hygiene def fixing the FiniteDimensional instance path once).

Equations

• Q2Presentation.Induction.edgeBaseFactor chief K lam hinv hne = Q2Presentation.Quadratic.polarization (Q2Presentation.Induction.edgeHeadForm chief K lam hinv hne)

theorem Q2Presentation.Induction.edgeBaseFactor_diagonal {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 : towerM K ⧸ towerT K) : ((edgeBaseFactor chief K lam hinv hne) v) v = (edgeHeadForm chief K lam hinv hne).form v

theorem Q2Presentation.Induction.edgeBaseFactor_polar {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 w : towerM K ⧸ towerT K) : ((edgeBaseFactor chief K lam hinv hne) v) w + ((edgeBaseFactor chief K lam hinv hne) w) v = ((edgeHeadForm chief K lam hinv hne).polar v) w

theorem Q2Presentation.Induction.edgeBaseFactor_add_left {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 y z : towerM K ⧸ towerT K) : ((edgeBaseFactor chief K lam hinv hne) (x + y)) z = ((edgeBaseFactor chief K lam hinv hne) x) z + ((edgeBaseFactor chief K lam hinv hne) y) z

theorem Q2Presentation.Induction.edgeBaseFactor_add_right {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 y z : towerM K ⧸ towerT K) : ((edgeBaseFactor chief K lam hinv hne) x) (y + z) = ((edgeBaseFactor chief K lam hinv hne) x) y + ((edgeBaseFactor chief K lam hinv hne) x) z

theorem Q2Presentation.Induction.edgeBaseFactor_zero_left {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 : towerM K ⧸ towerT K) : ((edgeBaseFactor chief K lam hinv hne) 0) z = 0

theorem Q2Presentation.Induction.edgeBaseFactor_zero_right {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 : towerM K ⧸ towerT K) : ((edgeBaseFactor chief K lam hinv hne) x) 0 = 0

𝒳_T-side: the connecting cochain γ_χ = ∂^∨(χ)

(concrete: extend χ along a fixed linear retraction onto T, take the δ-difference, descend to V^∨; manuscript l.4085–4092)

instance Q2Presentation.Induction.instFiniteXTEdge {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Finite ↥(XT chief K)

noncomputable instance Q2Presentation.Induction.instFintypeXTEdge {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Fintype ↥(XT chief K)

Equations

• Q2Presentation.Induction.instFintypeXTEdge chief K = Fintype.ofFinite ↥(Q2Presentation.Induction.XT chief K)

def Q2Presentation.Induction.edgeTCompl {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Submodule (ZMod 2) (towerM K)

A fixed complement of T in M (data-fixing choice; 𝔽₂-linear algebra).

Equations

• Q2Presentation.Induction.edgeTCompl chief K = ⋯.choose

theorem Q2Presentation.Induction.edgeTCompl_isCompl {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : IsCompl (towerT K) (edgeTCompl chief K)

def Q2Presentation.Induction.edgeTProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerM K →ₗ[ZMod 2] ↥(towerT K)

The fixed linear retraction π_T : M → T (identity on T).

Equations

• Q2Presentation.Induction.edgeTProj chief K = (Q2Presentation.Induction.towerT K).linearProjOfIsCompl (Q2Presentation.Induction.edgeTCompl chief K) ⋯

theorem Q2Presentation.Induction.edgeTProj_of_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) (hm : m ∈ towerT K) : (edgeTProj chief K) m = ⟨m, hm⟩

The paired characterization of the data-fixing def (banked fix-class): π_T restricts to the identity on T.

def Q2Presentation.Induction.chiTilde {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : Module.Dual (ZMod 2) (towerM K)

χ̃ = χ ∘ π_T : M^∨ — the retracted extension of χ ∈ 𝒳_T.

Equations

• Q2Presentation.Induction.chiTilde chief K chi = ↑chi ∘ₗ Q2Presentation.Induction.edgeTProj chief K

@[simp]

theorem Q2Presentation.Induction.chiTilde_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (m : towerM K) : (chiTilde chief K chi) m = ↑chi ((edgeTProj chief K) m)

theorem Q2Presentation.Induction.chi_act {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) (t : ↥(towerT K)) : ↑chi (((sec7ActOnTHom chief K) c) t) = ↑chi t

χ ∈ 𝒳_T is invariant under the restricted action (elementwise form of the mem_XT clause).

def Q2Presentation.Induction.gammaChiRaw {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) : Module.Dual (ZMod 2) (towerM K)

The δ(χ̃)-cochain on M: m ↦ χ̃(c⁻¹·m) + χ̃(m).

Equations

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

@[simp]

theorem Q2Presentation.Induction.gammaChiRaw_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) (m : towerM K) : (gammaChiRaw chief K chi c) m = (chiTilde chief K chi) (((towerActM K) c⁻¹) m) + (chiTilde chief K chi) m

theorem Q2Presentation.Induction.gammaChiRaw_zero_on_T {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) (t : towerM K) : t ∈ towerT K → (gammaChiRaw chief K chi c) t = 0

δ(χ̃) kills T (stability of T + invariance of χ + char 2), so it descends to V^∨.

def Q2Presentation.Induction.gammaChi {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) : Module.Dual (ZMod 2) (towerM K ⧸ towerT K)

γ_χ = ∂^∨(χ) ∈ V^∨, per c (manuscript l.4090–4092): the descended δ(χ̃)-difference.

Equations

• Q2Presentation.Induction.gammaChi chief K chi c = (Q2Presentation.Induction.towerT K).liftQ (Q2Presentation.Induction.gammaChiRaw chief K chi c) ⋯

@[simp]

theorem Q2Presentation.Induction.gammaChi_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) (m : towerM K) : (gammaChi chief K chi c) (Submodule.Quotient.mk m) = (chiTilde chief K chi) (((towerActM K) c⁻¹) m) + (chiTilde chief K chi) m

theorem Q2Presentation.Induction.gammaChi_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : gammaChi chief K chi 1 = 0

Normalization: γ_χ(1) = 0.

theorem Q2Presentation.Induction.gammaChi_cocycle {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c d : towerC K) (v : towerM K ⧸ towerT K) : (gammaChi chief K chi (c * d)) v = (gammaChi chief K chi c) v + (gammaChi chief K chi d) ((headActE chief K c⁻¹) v)

The twisted Z¹(C, V^∨) law for γ_χ: γ_χ(cd) = γ_χ(c) + c·γ_χ(d) with the dual action (c·φ)(v) = φ(c⁻¹·v).

The zero-edge descent bundle

structure Q2Presentation.Induction.ZeroEdgeDescentData {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)) : Type

The zero-edge descent data (eq:descendedclass l.4037–4045 + lem:affinelifting l.4048–4083, as one choice bundle — the §6.5 choice discipline: both R4b keeps take the SAME bundle):

• D/hW — the zero-edge witness (a normal edge complement, P3-U3); the bundle therefore implies ZeroEdge (ZeroEdgeDescentData.zeroEdge);
• Csec + hdisj/hsup — the lem:transgression splitting coordinates B/T' = V ⋊ C (Csec a complement to the V-layer);
• gammaK/deltaK — the normalized decomposition data γ_κ ∈ Z¹(C,V^∨), δ_κ ∈ Z²(C,𝔽₂) of the descended class, with concrete cocycle laws (dual action (c·φ)(v) = φ(c⁻¹·v));
• eT — the lem:affinelifting class e ∈ Z²(C,T) (pullback of B → V⋊C along the zero section), twisted cocycle law in the hzc-ready orientation;
• mC — the equivariant-lift correction functions m_c of the κ_q⁰-model (eq:mquadratic/eq:mcoherent l.4118–4125, stated against the bilinear factor set edgeBaseFactor).

The deep pinning identity — that a normalized section cocycle of the descended double cover descTarget D hW equals κ_q⁰-model + Γ_{γ_κ} + inf δ_κ in the Csec-coordinates, and that eT is the actual zero-section pullback — is owned by the deferred transgression unit (btChild_splits/zeroEdgeDescentData_nonempty, design §4.7); until it lands, the coordinated R4b keep must carry that pinning alongside this bundle (same discipline as U7's ¬ZeroEdge conditioning living on the future keep).

• hne : lam ≠ 0
• D : EdgeComplement chief K lam hinv
• hW : self.D.W.Normal
• Csec : Subgroup (btChild chief K).fst.Y
• hdisj : self.Csec ⊓ vLayer chief K = ⊥
• hsup : self.Csec ⊔ vLayer chief K = ⊤
• gammaK : towerC K → Module.Dual (ZMod 2) (towerM K ⧸ towerT K)
• gammaK_one : self.gammaK 1 = 0
• gammaK_cocycle (c d : towerC K) (v : towerM K ⧸ towerT K) : (self.gammaK (c * d)) v = (self.gammaK c) v + (self.gammaK d) ((headActE chief K c⁻¹) v)
• deltaK : towerC K → towerC K → ZMod 2
• deltaK_one_left (d : towerC K) : self.deltaK 1 d = 0
• deltaK_one_right (c : towerC K) : self.deltaK c 1 = 0
• deltaK_cocycle (a b c : towerC K) : self.deltaK a b + self.deltaK (a * b) c = self.deltaK b c + self.deltaK a (b * c)
• eT : towerC K → towerC K → ↥(towerT K)
• eT_one_left (d : towerC K) : self.eT 1 d = 0
• eT_one_right (c : towerC K) : self.eT c 1 = 0
• eT_cocycle (a b c : towerC K) : self.eT a b + self.eT (a * b) c = ((sec7ActOnTHom chief K) a) (self.eT b c) + self.eT a (b * c)
• mC : towerC K → towerM K ⧸ towerT K → ZMod 2
• mC_one (v : towerM K ⧸ towerT K) : self.mC 1 v = 0
• mC_quadratic (c : towerC K) (v w : towerM K ⧸ towerT K) : self.mC c (v + w) + self.mC c v + self.mC c w = ((edgeBaseFactor chief K lam hinv ⋯) ((headActE chief K c) v)) ((headActE chief K c) w) + ((edgeBaseFactor chief K lam hinv ⋯) v) w
• mC_coherent (c d : towerC K) (v : towerM K ⧸ towerT K) : self.mC (c * d) v = self.mC c ((headActE chief K d) v) + self.mC d v

theorem Q2Presentation.Induction.ZeroEdgeDescentData.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)) (Z : ZeroEdgeDescentData chief K lam hinv) : ZeroEdge chief K lam hinv

The bundle implies the zero-edge branch (design §6.1: the two R4 branches are mutually exclusive by construction).

theorem Q2Presentation.Induction.mC_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)) (Z : ZeroEdgeDescentData chief K lam hinv) (c : towerC K) : Z.mC c 0 = 0

m_c(0) = 0 (from eq:mquadratic at v = w = 0, char 2).

theorem Q2Presentation.Induction.mC_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)) (Z : ZeroEdgeDescentData chief K lam hinv) (c : towerC K) (v w : towerM K ⧸ towerT K) : Z.mC c (v + w) = Z.mC c v + Z.mC c w + ((edgeBaseFactor chief K lam hinv ⋯) ((headActE chief K c) v)) ((headActE chief K c) w) + ((edgeBaseFactor chief K lam hinv ⋯) v) w

eq:mquadratic in solved form: m_c(v+w) = m_c(v) + m_c(w) + f(cv, cw) + f(v, w).

a_{χ,κ} = (b_q̄^♭)⁻¹(γ_χ + γ_κ) (P6's polar_bijective at the

head form; exists_polarRep/polarRep_unique packaged as the linear equivalence)

def Q2Presentation.Induction.edgePolarEquiv {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) : (towerM K ⧸ towerT K) ≃ₗ[ZMod 2] Module.Dual (ZMod 2) (towerM K ⧸ towerT K)

The polar map of q̄_λ as a linear equivalence onto the dual (nonsingularity + finiteness; lem:constrainedgauss l.3883–3885).

Equations

• Q2Presentation.Induction.edgePolarEquiv chief K lam hinv hne = LinearEquiv.ofBijective (Q2Presentation.Induction.edgeHeadForm chief K lam hinv hne).polar ⋯

@[simp]

theorem Q2Presentation.Induction.edgePolarEquiv_apply {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 : towerM K ⧸ towerT K) : (edgePolarEquiv chief K lam hinv hne) v = (edgeHeadForm chief K lam hinv hne).polar v

def Q2Presentation.Induction.aRep {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c : towerC K) : towerM K ⧸ towerT K

The representing 1-cochain a_{χ,κ} (eq:phaseclass input, manuscript l.4093–4095): a_{χ,κ}(c) = (b_q̄^♭)⁻¹(γ_χ(c) + γ_κ(c)).

Equations

• Q2Presentation.Induction.aRep chief K lam hinv Z chi c = (Q2Presentation.Induction.edgePolarEquiv chief K lam hinv ⋯).symm (Q2Presentation.Induction.gammaChi chief K chi c + Z.gammaK c)

theorem Q2Presentation.Induction.aRep_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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) : aRep chief K lam hinv Z chi 1 = 0

Normalization: a_{χ,κ}(1) = 0.

theorem Q2Presentation.Induction.aRep_cocycle {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c d : towerC K) : aRep chief K lam hinv Z chi (c * d) = aRep chief K lam hinv Z chi c + (headActE chief K c) (aRep chief K lam hinv Z chi d)

a_{χ,κ} ∈ Z¹(C, V): the twisted 1-cocycle law a(cd) = a(c) + c·a(d) (γ-cocycle laws + polar equivariance).

The base graph cocycle Θ_q⁰(a_{χ,κ}) and the total phase Δ_{χ,κ}

def Q2Presentation.Induction.thetaGraph {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c d : towerC K) : ZMod 2

Θ_q⁰(a_{χ,κ}) (eq:Theta0phase l.4097–4100, concrete graph form eq:baseconnectingcochain l.2136–2139: Θ(c,d) = f(a(c), c·a(d)) + m_c(a(d))).

Equations

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

theorem Q2Presentation.Induction.thetaGraph_one_left {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (d : towerC K) : thetaGraph chief K lam hinv Z chi 1 d = 0

theorem Q2Presentation.Induction.thetaGraph_one_right {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c : towerC K) : thetaGraph chief K lam hinv Z chi c 1 = 0

theorem Q2Presentation.Induction.thetaGraph_cocycle {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (a b c : towerC K) : thetaGraph chief K lam hinv Z chi a b + thetaGraph chief K lam hinv Z chi (a * b) c = thetaGraph chief K lam hinv Z chi b c + thetaGraph chief K lam hinv Z chi a (b * c)

Θ_q⁰(a_{χ,κ}) is a 2-cocycle (graph of a Z¹-cocycle pulled back against the bilinear base model).

def Q2Presentation.Induction.DeltaC {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c d : towerC K) : ZMod 2

The total target-side phase Δ_{χ,κ}, towerC-spelling (eq:phaseclass l.4101–4106): Δ = χ_*e + δ_κ + Θ_q⁰(a_{χ,κ}) — the δ_κ-term enters exactly once (P6 §7.6 discipline; the engine's ε-slot IS this term).

Equations

• Q2Presentation.Induction.DeltaC chief K lam hinv Z chi c d = ↑chi (Z.eT c d) + Z.deltaK c d + Q2Presentation.Induction.thetaGraph chief K lam hinv Z chi c d

@[simp]

theorem Q2Presentation.Induction.DeltaC_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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c d : towerC K) : DeltaC chief K lam hinv Z chi c d = ↑chi (Z.eT c d) + Z.deltaK c d + thetaGraph chief K lam hinv Z chi c d

theorem Q2Presentation.Induction.DeltaC_one_left {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (d : towerC K) : DeltaC chief K lam hinv Z chi 1 d = 0

theorem Q2Presentation.Induction.DeltaC_one_right {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (c : towerC K) : DeltaC chief K lam hinv Z chi c 1 = 0

theorem Q2Presentation.Induction.DeltaC_cocycle {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (a b c : towerC K) : DeltaC chief K lam hinv Z chi a b + DeltaC chief K lam hinv Z chi (a * b) c = DeltaC chief K lam hinv Z chi b c + DeltaC chief K lam hinv Z chi a (b * c)

Δ_{χ,κ} is a normalized 2-cocycle: the χ_*e-leg by χ-invariance (chi_act) applied to the twisted eT-law, the δ_κ-leg by the bundle law, the Θ-leg by thetaGraph_cocycle.

Δ_{χ,κ} at the C-child carrier (the phaseCount-consumable

spelling: P7's PhaseCoverTransform cocycle slots)

def Q2Presentation.Induction.Delta {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2

The phase class Δ_{χ,κ} on the C-child carrier — DeltaC transported along the canonical collapse B/M' ≃* C (cChildCollapse); the cocycle P7's phaseCount/phaseCoverPair consume at ζ := Delta Z chi (design §4.7; per-cocycle discipline, no class-invariance asserted).

Equations

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

theorem Q2Presentation.Induction.Delta_one_left {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (y : (cChild chief K).fst.Y) : Delta chief K lam hinv Z chi 1 y = 0

Normalization, left slot (the hz1-slot of phaseCount).

theorem Q2Presentation.Induction.Delta_one_right {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (y : (cChild chief K).fst.Y) : Delta chief K lam hinv Z chi y 1 = 0

Normalization, right slot (the hz2-slot of phaseCount).

theorem Q2Presentation.Induction.Delta_cocycle {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (chi : ↥(XT chief K)) (a b c : (cChild chief K).fst.Y) : Delta chief K lam hinv Z chi a b + Delta chief K lam hinv Z chi (a * b) c = Delta chief K lam hinv Z chi b c + Delta chief K lam hinv Z chi a (b * c)

The 2-cocycle law (the hzc-slot of phaseCount).