The λ-free extension structure of B/T'

theorem Q2Presentation.Induction.vLayer_mul_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) (hx : x ∈ vLayer chief K) : x * x = 1

vLayer-elements square to 1 (M' is elementary, descended).

theorem Q2Presentation.Induction.vLayer_comm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x x' : (btChild chief K).fst.Y) (hx : x ∈ vLayer chief K) (hx' : x' ∈ vLayer chief K) : x * x' = x' * x

vLayer is abelian (M' is abelian, descended).

instance Q2Presentation.Induction.instCommGroupVLayer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : CommGroup ↥(vLayer chief K)

Equations

• Q2Presentation.Induction.instCommGroupVLayer chief K = { toGroup := inferInstance, mul_comm := ⋯ }

instance Q2Presentation.Induction.instModuleVLayerAdditive {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Module (ZMod 2) (Additive ↥(vLayer chief K))

Equations

• Q2Presentation.Induction.instModuleVLayerAdditive chief K = AddCommGroup.zmodModule ⋯

def Q2Presentation.Induction.btProjAux {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (XRZero.xrChild chief K).fst.Y →* towerC K

The projection to the base of 1 → V → B/T' → C → 1, ambient form.

Equations

• Q2Presentation.Induction.btProjAux chief K = (Q2Presentation.Induction.mChildCollapse chief K).toMonoidHom.comp (QuotientGroup.mk' (Q2Presentation.Induction.mChild chief K))

@[simp]

theorem Q2Presentation.Induction.btProjAux_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : (XRZero.xrChild chief K).fst.Y) : (btProjAux chief K) y = (mChildCollapse chief K) ((QuotientGroup.mk' (mChild chief K)) y)

def Q2Presentation.Induction.btProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (btChild chief K).fst.Y →* towerC K

The base projection btProj : B/T' ↠ C (T' ≤ M' collapse).

Equations

• Q2Presentation.Induction.btProj chief K = QuotientGroup.lift (Q2Presentation.Induction.tChild chief K) (Q2Presentation.Induction.btProjAux chief K) ⋯

@[simp]

theorem Q2Presentation.Induction.btProj_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : (XRZero.xrChild chief K).fst.Y) : (btProj chief K) ((QuotientGroup.mk' (tChild chief K)) y) = (btProjAux chief K) y

theorem Q2Presentation.Induction.btProj_mk_childMk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : (btProj chief K) ((QuotientGroup.mk' (tChild chief K)) (childMk chief K y)) = (QuotientGroup.mk' K.Ksub) y

btProj on a double child class: the C-class of the ambient element (Noether III computed).

theorem Q2Presentation.Induction.btProj_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Surjective ⇑(btProj chief K)

theorem Q2Presentation.Induction.mem_vLayer_iff_btProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) : x ∈ vLayer chief K ↔ (btProj chief K) x = 1

ker btProj = vLayer, elementwise (the extension identity).

The fibre inclusion vInG : V → B/T' and its conjugation law

def Q2Presentation.Induction.vLayerHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerMgrp K →* ↥(vLayer chief K)

The multiplicative fibre map M → vLayer (through mChildDescend).

Equations

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

theorem Q2Presentation.Induction.vLayerHom_towerTgrp {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerMgrp K) (hm : m ∈ towerTgrp K) : (vLayerHom chief K) m = 1

The fibre map kills the radical layer (T-transport of the bridge).

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

The linear fibre inclusion V = M/T →ₗ Additive vLayer (the T-quotient descent of vLayerHom).

Equations

• Q2Presentation.Induction.vIn chief K = (Q2Presentation.Induction.towerT K).liftQ (AddMonoidHom.toZModLinearMap 2 (MonoidHom.toAdditive (Q2Presentation.Induction.vLayerHom chief K))) ⋯

def Q2Presentation.Induction.vInG {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : (btChild chief K).fst.Y

The group-carrier fibre inclusion V → B/T'.

Equations

• Q2Presentation.Induction.vInG chief K v = ↑(Additive.toMul ((Q2Presentation.Induction.vIn chief K) v))

@[simp]

theorem Q2Presentation.Induction.vInG_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) : vInG chief K (Submodule.Quotient.mk m) = (QuotientGroup.mk' (tChild chief K)) ↑((mChildDescend chief K) (Additive.toMul m))

theorem Q2Presentation.Induction.vInG_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : vInG chief K v ∈ vLayer chief K

theorem Q2Presentation.Induction.vInG_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : vInG chief K 0 = 1

theorem Q2Presentation.Induction.vInG_add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v w : towerM K ⧸ towerT K) : vInG chief K (v + w) = vInG chief K v * vInG chief K w

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

theorem Q2Presentation.Induction.vInG_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) (v : towerM K ⧸ towerT K) : x * vInG chief K v * x⁻¹ = vInG chief K ((headActE chief K ((btProj chief K) x)) v)

Conjugation covers the head action: conjugating the fibre by any element of B/T' acts by headActE at the image C-class — the lem:transgression compatibility, fully proven.

The splitting statement and its section criterion

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

B/T' splits as V⋊C (the conclusion of lem:transgression at the child, complement form — the exact shape of the Csec/hdisj/hsup slots of ZeroEdgeDescentData, design §4.7).

Equations

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

theorem Q2Presentation.Induction.btChild_splits_of_section {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K →* (btChild chief K).fst.Y) (hs : ∀ (c : towerC K), (btProj chief K) (s c) = c) : SplitsBtChild chief K

A homomorphic section of btProj yields the complement.

The two remaining inputs, as named data/Props (hypothesis

discipline — the RadicalEdgeHalving pattern; NOT axioms)

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

The κ_q⁰-model data at the R4b head: the coherent equivariant correction functions m_c of lem:extraspecialconnecting (eq:mquadratic l.2118–2120 + eq:mcoherent l.2122–2124) against the bilinear factor set edgeBaseFactor — exactly the mC-slots of ZeroEdgeDescentData.

• m : towerC K → towerM K ⧸ towerT K → ZMod 2
• m_one (v : towerM K ⧸ towerT K) : self.m 1 v = 0
• m_quadratic (c : towerC K) (v w : towerM K ⧸ towerT K) : self.m c (v + w) + self.m c v + self.m c w = ((edgeBaseFactor chief K lam hinv hne) ((headActE chief K c) v)) ((headActE chief K c) w) + ((edgeBaseFactor chief K lam hinv hne) v) w
• m_coherent (c d : towerC K) (v : towerM K ⧸ towerT K) : self.m (c * d) v = self.m c ((headActE chief K d) v) + self.m d v

def Q2Presentation.Induction.BaseModelExists {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

KEEP-SHAPED INPUT (named Prop, consumed as a hypothesis): the base equivariant determinant class exists at the R4b head.

Provenance (manuscript): lem:basedetclass l.2286–2360 — the normalized base class κ_q⁰ ∈ Z²(V⋊H,𝔽₂) with fibre square map q, built on an H-split regular pair via the three orbit-polynomial factor sets (eq:squareorbitfactor, eq:freeorbitfactor, eq:kappahalforbit); its normalized-section action data are exactly the m_c of lem:extraspecialconnecting. The proof consumes the tame module structure (projectivity via lem:faithfulprojective in the ramified case, Maschke in the odd unramified case) — genuinely arithmetic input about V, NOT finite bookkeeping.

Dissolution program (owner: the P6 base-class lane, coordinated with BLOCKR_P6_DESIGN §1.1 which records the eq:basekappacochain normalization shape): (i) the split pair V → 𝔽₂[H]^N → V at the head (edgeHead-carrier Maschke/projectivity); (ii) the three orbit factor sets with their m_c = 0 resp. half-orbit corrections; (iii) pullback and the eq:mquadratic/eq:mcoherent laws. Until it lands, both btChild_splits_of and zeroEdgeDescentData_nonempty_of consume the DATA (BaseModelData) as an explicit hypothesis.

Equations

• Q2Presentation.Induction.BaseModelExists chief K lam hinv hne = Nonempty (Q2Presentation.Induction.BaseModelData chief K lam hinv hne)

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

The descended-cover reading data for lem:transgression at the child: a normalized set-section σ of btProj with its section cochain η (eq:extensionfactortransgression), and the two 𝔽₂-readings of the descended central double cover — the fibre factor cochain g (squares = q̄_λ, symmetry defect = b̄, 2-cocycle) and the conjugation defect n ((†) quadratic law; (‡) eq:transgressioncochain, concrete).

Every field is FINITE BOOKKEEPING over the GREEN U1–U3 layer (no arithmetic input): g/n are relRead-readings in descTarget D hW (squares/commutators/conjugations of mCover-lifts — scalarProj_sq_eq_form, scalarProj_comm_eq_polar, mCover_conj_fix through descProj; centrality of the deck by descKernel_le_center), σ/η come from Classical.choice sections of the two surjections. The construction is the remaining MECHANICAL obligation of this unit (deferred for size, NOT keep-shaped; program in the §14 design notes).

• sigma : towerC K → (btChild chief K).fst.Y
• sigma_one : self.sigma 1 = 1
• sigma_sec (c : towerC K) : (btProj chief K) (self.sigma c) = c
• g : towerM K ⧸ towerT K → towerM K ⧸ towerT K → ZMod 2
• g_diag (v : towerM K ⧸ towerT K) : self.g v v = (edgeHeadForm chief K lam hinv hne).form v
• g_polar (v w : towerM K ⧸ towerT K) : self.g v w + self.g w v = ((edgeHeadForm chief K lam hinv hne).polar v) w
• g_cocycle (u v w : towerM K ⧸ towerT K) : self.g u v + self.g (u + v) w = self.g v w + self.g u (v + w)
• n : towerC K → towerM K ⧸ towerT K → ZMod 2
• n_one (v : towerM K ⧸ towerT K) : self.n 1 v = 0
• n_quadratic (c : towerC K) (v w : towerM K ⧸ towerT K) : self.n c (v + w) + self.n c v + self.n c w = self.g ((headActE chief K c) v) ((headActE chief K c) w) + self.g v w
• eta : towerC K → towerC K → towerM K ⧸ towerT K
• sigma_eta (c d : towerC K) : self.sigma c * self.sigma d = vInG chief K (self.eta c d) * self.sigma (c * d)
• n_coherent (c d : towerC K) (v : towerM K ⧸ towerT K) : self.n c ((headActE chief K d) v) + self.n d v + self.n (c * d) v = ((edgeHeadForm chief K lam hinv hne).polar (self.eta c d)) ((headActE chief K (c * d)) v)

def Q2Presentation.Induction.TransgressionReading {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

Named deferred-construction Prop (hypothesis slot; see the TransgressionDescentData docstring for the two-part provenance: the manuscript source is lem:transgression's section/reading choices at the descended cover of lem:radicaledge step 7, and the dissolution is the mechanical U1–U3 reading construction — finite bookkeeping, no keeps).

Equations

• Q2Presentation.Induction.TransgressionReading chief K lam hinv hne = Nonempty (Q2Presentation.Induction.TransgressionDescentData chief K lam hinv hne)

theorem Q2Presentation.Induction.btChild_splits_of {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) (R : TransgressionDescentData chief K lam hinv hne) (M : BaseModelData chief K lam hinv hne) : SplitsBtChild chief K

lem:transgression at the child, PROVEN from the reading data and the κ_q⁰-model (l.3464–3530 + l.4032–4034): the engine's coboundary a shears the section homomorphic, and its range is the complement.

theorem Q2Presentation.Induction.btChild_splits {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) (hread : TransgressionReading chief K lam hinv hne) (hbase : BaseModelExists chief K lam hinv hne) : SplitsBtChild chief K

(a) btChild_splits, in the honest hypothesis-form: the zero-edge B/T' splits as V⋊C, GIVEN the two named inputs (reading data: mechanical, deferred; base model: lem:basedetclass, P6-owned).

theorem Q2Presentation.Induction.zeroEdgeDescentData_nonempty_of {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) (hZ : ZeroEdge chief K lam hinv) (hsplit : SplitsBtChild chief K) (M : BaseModelData chief K lam hinv hne) : Nonempty (ZeroEdgeDescentData chief K lam hinv)

(b) the U8 bundle exists given ZeroEdge + the splitting + a κ_q⁰-model: Csec/hdisj/hsup from the splitting, mC from the model, and the UNPINNED cochain slots γ_κ = δ_κ = e = 0 (all cocycle laws trivial). This is exactly the existence half P8's Classical.byCases split consumes (design §6.1); the tie to the ACTUAL descended class is the separate pinning (ZeroEdgePinning below), carried by the future coordinated keep — the §13 note's discipline.

theorem Q2Presentation.Induction.zeroEdgeDescentData_nonempty {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) (hZ : ZeroEdge chief K lam hinv) (hread : TransgressionReading chief K lam hinv hne) (hbase : BaseModelExists chief K lam hinv hne) : Nonempty (ZeroEdgeDescentData chief K lam hinv)

(b) zeroEdgeDescentData_nonempty, hypothesis-form (the design §4.7 name): ZeroEdge + the two named inputs give the bundle.

(c) The base-identity pinning (eq:descendedclass +

lem:affinelifting's zero-section pullback, in Csec-coordinates)

def Q2Presentation.Induction.tIn {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (t : ↥(towerT K)) : (XRZero.xrChild chief K).fst.Y

The radical-layer inclusion T → B (bridge form; lands in T').

Equations

• Q2Presentation.Induction.tIn chief K t = ↑((Q2Presentation.Induction.mChildDescend chief K) (Additive.toMul ↑t))

theorem Q2Presentation.Induction.tIn_mem_tChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (t : ↥(towerT K)) : tIn chief K t ∈ tChild chief K

def Q2Presentation.Induction.descToBt {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : (descTarget chief K lam hinv D hW).Y →* (btChild chief K).fst.Y

The descended double cover mapped onto B/T' (deck collapse composed with descCollapseChild).

Equations

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

def Q2Presentation.Induction.descRead {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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (x : (descTarget chief K lam hinv D hW).Y) : ZMod 2

The 𝔽₂-reading of the descended deck (relRead idiom at the descended target: 1 ↦ 0, else 1; on the order-2 descKernel this is the λ-pinned isomorphism, card_descKernel_eq_two).

Equations

• Q2Presentation.Induction.descRead chief K lam hinv D hW x = if x = 1 then 0 else 1

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

The base-identity pinning of a bundle Z — the §13 deferral's third item, concrete. In the Z.Csec-coordinates (a multiplicative section s, so the section cochain η vanishes), the normalized section cocycle of the ACTUAL descended cover descTarget Z.D Z.hW at the total section (v,c) ↦ ℓ̂(v)·σ̂(c) is κ((v,c),(w,d)) = g(v,cw) + n_c(w) + e(c,d) with g/n/e the three deck readings; the fields pin

• g = edgeBaseFactor (fib_*): the fibre part is the κ_q⁰-model factor set — eq:basekappacochain's fibre normalization;
• n_c = Z.mC c + Z.gammaK c ∘ (c·) (conj_*): the conjugation defect is the model correction plus the Γ_{γ_κ}-term (eq:Gammagamma);
• e = Z.deltaK (sec_*): the pure base part is the inflated scalar —

i.e. κ = κ_q⁰ + Γ_{γ_κ} + inf δ_κ as normalized cochains, eq:descendedclass l.4037–4045 ON THE NOSE; and tau_eT pins Z.eT as the actual zero-section pullback of B → V⋊C along the Csec-section (lem:affinelifting l.4050–4056). Nonempty (ZeroEdgePinning … Z) is the pinning hypothesis the FUTURE coordinated R4b keep must carry alongside Z (both U8/U9 zero-edge keep docstrings + §13 note 6).

• s : towerC K → (btChild chief K).fst.Y
• s_one : self.s 1 = 1
• s_mem (c : towerC K) : self.s c ∈ Z.Csec
• s_sec (c : towerC K) : (btProj chief K) (self.s c) = c
• s_mul (c d : towerC K) : self.s c * self.s d = self.s (c * d)
• tau : towerC K → (XRZero.xrChild chief K).fst.Y
• tau_proj (c : towerC K) : (QuotientGroup.mk' (tChild chief K)) (self.tau c) = self.s c
• tau_eT (c d : towerC K) : self.tau c * self.tau d = tIn chief K (Z.eT c d) * self.tau (c * d)
• ellHat : towerM K ⧸ towerT K → (descTarget chief K lam hinv Z.D ⋯).Y
• ellHat_zero : self.ellHat 0 = 1
• ellHat_proj (v : towerM K ⧸ towerT K) : (descToBt chief K lam hinv Z.D ⋯ ⋯) (self.ellHat v) = vInG chief K v
• sigmaHat : towerC K → (descTarget chief K lam hinv Z.D ⋯).Y
• sigmaHat_one : self.sigmaHat 1 = 1
• sigmaHat_proj (c : towerC K) : (descToBt chief K lam hinv Z.D ⋯ ⋯) (self.sigmaHat c) = self.s c
• fib_mem (v w : towerM K ⧸ towerT K) : self.ellHat v * self.ellHat w * (self.ellHat (v + w))⁻¹ ∈ (descKernel chief K lam hinv Z.D ⋯ ⋯).N
• fib_read (v w : towerM K ⧸ towerT K) : descRead chief K lam hinv Z.D ⋯ (self.ellHat v * self.ellHat w * (self.ellHat (v + w))⁻¹) = ((edgeBaseFactor chief K lam hinv ⋯) v) w
• conj_mem (c : towerC K) (v : towerM K ⧸ towerT K) : self.sigmaHat c * self.ellHat v * (self.sigmaHat c)⁻¹ * (self.ellHat ((headActE chief K c) v))⁻¹ ∈ (descKernel chief K lam hinv Z.D ⋯ ⋯).N
• conj_read (c : towerC K) (v : towerM K ⧸ towerT K) : descRead chief K lam hinv Z.D ⋯ (self.sigmaHat c * self.ellHat v * (self.sigmaHat c)⁻¹ * (self.ellHat ((headActE chief K c) v))⁻¹) = Z.mC c v + (Z.gammaK c) ((headActE chief K c) v)
• sec_mem (c d : towerC K) : self.sigmaHat c * self.sigmaHat d * (self.sigmaHat (c * d))⁻¹ ∈ (descKernel chief K lam hinv Z.D ⋯ ⋯).N
• sec_read (c d : towerC K) : descRead chief K lam hinv Z.D ⋯ (self.sigmaHat c * self.sigmaHat d * (self.sigmaHat (c * d))⁻¹) = Z.deltaK c d

theorem Q2Presentation.Induction.ZeroEdgePinning.splitsBtChild {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} (P : ZeroEdgePinning chief K lam hinv Z) : SplitsBtChild chief K

A pinned bundle's Csec-section witnesses the splitting (the pinning implies (a) for its own bundle — consistency of the packaging).

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

The pinning Prop — the exact hypothesis slot the future coordinated zero-edge keep must carry alongside the bundle Z until the reading-data construction lands (the §13 note's discipline: conditioning lives on the future keep, never in the count Props).

Equations

• Q2Presentation.Induction.ZeroEdgeDescentDataPinned chief K lam hinv Z = Nonempty (Q2Presentation.Induction.ZeroEdgePinning chief K lam hinv Z)