§1 The T-layer reading toolkit (the tIn-bridge inverted)

tIn : T → B (TransgressionUnit) lands in tChild and is injective with image exactly tChild (through the mChildEquiv-bridge); its conjugation law covers sec7ActOnTHom. These are the tools that read the tau-defects back into T for the eT-slot.

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

tIn is normalized: tIn 0 = 1.

theorem Q2Presentation.Induction.pinTIn_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (t t' : ↥(towerT K)) : tIn chief K (t + t') = tIn chief K t * tIn chief K t'

tIn is additive-to-multiplicative.

theorem Q2Presentation.Induction.pinTIn_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Injective (tIn chief K)

tIn is injective (mChildDescend is bijective).

theorem Q2Presentation.Induction.pinTIn_exists {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (XRZero.xrChild chief K).fst.Y) (hx : x ∈ tChild chief K) : ∃ (t : ↥(towerT K)), tIn chief K t = x

tIn covers tChild (the bridge inverted on the radical layer).

theorem Q2Presentation.Induction.pinTIn_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (t : ↥(towerT K)) : childMk chief K y * tIn chief K t * (childMk chief K y)⁻¹ = tIn chief K (((sec7ActOnTHom chief K) ((QuotientGroup.mk' K.Ksub) y)) t)

Conjugation transport across the T-bridge: conjugating tIn t by an ambient class-representative acts by sec7ActOnTHom at the C-class — the vInG_conj compatibility one layer down (through mChildEquiv_conjOnMgrp + towerActM_mk).

§2 The tau-layer over a multiplicative section of btProj

Everything here is generic over an abstract section s : C → B/T' with s 1 = 1, s-multiplicativity, and the section property — instantiated at csecSec in the main theorem.

def Q2Presentation.Induction.pinTau {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (c : towerC K) : (XRZero.xrChild chief K).fst.Y

The 1-pinned B-representative choice over a section of btProj (the readSecAmb-style choice at the child, design §4-N10).

Equations

• Q2Presentation.Induction.pinTau chief K s c = if c = 1 then 1 else ⋯.choose

theorem Q2Presentation.Induction.pinTau_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) : pinTau chief K s 1 = 1

theorem Q2Presentation.Induction.pinTau_proj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (c : towerC K) : (QuotientGroup.mk' (tChild chief K)) (pinTau chief K s c) = s c

theorem Q2Presentation.Induction.pinTau_defect_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (c d : towerC K) : pinTau chief K s c * pinTau chief K s d * (pinTau chief K s (c * d))⁻¹ ∈ tChild chief K

The tau-defect dies in T' (multiplicativity of s).

def Q2Presentation.Induction.pinET {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (c d : towerC K) : ↥(towerT K)

The lem:affinelifting zero-section pullback read: the T-element carried by the tau-defect.

Equations

• Q2Presentation.Induction.pinET chief K s hs1 hsmul c d = ⋯.choose

theorem Q2Presentation.Induction.pinETSpec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (c d : towerC K) : tIn chief K (pinET chief K s hs1 hsmul c d) = pinTau chief K s c * pinTau chief K s d * (pinTau chief K s (c * d))⁻¹

theorem Q2Presentation.Induction.pinTau_eT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (c d : towerC K) : pinTau chief K s c * pinTau chief K s d = tIn chief K (pinET chief K s hs1 hsmul c d) * pinTau chief K s (c * d)

The tau_eT-pinning shape: tau c · tau d = tIn (e_T c d) · tau (cd).

theorem Q2Presentation.Induction.pinET_one_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (d : towerC K) : pinET chief K s hs1 hsmul 1 d = 0

theorem Q2Presentation.Induction.pinET_one_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (c : towerC K) : pinET chief K s hs1 hsmul c 1 = 0

theorem Q2Presentation.Induction.pinTau_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hssec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (a : towerC K) (t : ↥(towerT K)) : pinTau chief K s a * tIn chief K t * (pinTau chief K s a)⁻¹ = tIn chief K (((sec7ActOnTHom chief K) a) t)

Conjugation by tau a covers sec7ActOnTHom a on tIn-images (the section property identifies the ambient class of any representative).

theorem Q2Presentation.Induction.pinET_cocycle {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hs1 : s 1 = 1) (hsmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (hssec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (a b c : towerC K) : pinET chief K s hs1 hsmul a b + pinET chief K s hs1 hsmul (a * b) c = ((sec7ActOnTHom chief K) a) (pinET chief K s hs1 hsmul b c) + pinET chief K s hs1 hsmul a (b * c)

The twisted Z²(C,T)-law of the tau-defect read (the bundle's eT_cocycle-slot): pure factor-set algebra plus pinTau_conj.

§3 The deck coordinate pinDeck (the λ-pinned ZMod 2 ≅ deck)

The order-2 central deck of the descended cover, parameterized by its 𝔽₂-coordinate: the correction currency of the ℓ̂-renormalization.

def Q2Presentation.Induction.pinDeckElt {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) : ↥(descKernel chief K lam hinv D hW hne).N

The unique nontrivial deck element (card_descKernel_eq_two).

Equations

• Q2Presentation.Induction.pinDeckElt chief K lam hinv D hW hne = Exists.choose ⋯

theorem Q2Presentation.Induction.pinDeckElt_ne_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : pinDeckElt chief K lam hinv D hW hne ≠ 1

def Q2Presentation.Induction.pinDeck {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) (r : ZMod 2) : (descTarget chief K lam hinv D hW).Y

The deck element with a prescribed 𝔽₂-reading.

Equations

• Q2Presentation.Induction.pinDeck chief K lam hinv D hW hne r = if r = 0 then 1 else ↑(Q2Presentation.Induction.pinDeckElt chief K lam hinv D hW hne)

theorem Q2Presentation.Induction.pinDeck_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : pinDeck chief K lam hinv D hW hne 0 = 1

theorem Q2Presentation.Induction.pinDeck_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (r : ZMod 2) : pinDeck chief K lam hinv D hW hne r ∈ (descKernel chief K lam hinv D hW hne).N

theorem Q2Presentation.Induction.pinDeck_read {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) (r : ZMod 2) : descRead chief K lam hinv D hW (pinDeck chief K lam hinv D hW hne r) = r

The deck coordinate reads back (descRead ∘ pinDeck = id).

theorem Q2Presentation.Induction.pinDeck_inv {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) (r : ZMod 2) : (pinDeck chief K lam hinv D hW hne r)⁻¹ = pinDeck chief K lam hinv D hW hne r

The deck coordinate is self-inverse (order-2 kernel).

theorem Q2Presentation.Induction.pinDeck_comm {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) (r : ZMod 2) (g : (descTarget chief K lam hinv D hW).Y) : g * pinDeck chief K lam hinv D hW hne r = pinDeck chief K lam hinv D hW hne r * g

The deck coordinate is central (elementwise descKernel_le_center).

theorem Q2Presentation.Induction.pinDeck_toBt {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) (r : ZMod 2) : (descToBt chief K lam hinv D hW hne) (pinDeck chief K lam hinv D hW hne r) = 1

The deck coordinate dies under the cover map.

§4 The section-defect reading pinDelta (the δ_κ-slot)

Generic over an abstract lift σ̂; the pinning's sec_read holds by rfl because the bundle's deltaK IS this reading.

def Q2Presentation.Induction.pinDelta {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) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (c d : towerC K) : ZMod 2

The deck reading of the σ̂-defect (eq:descendedclass's pure base part, inf δ_κ).

Equations

• Q2Presentation.Induction.pinDelta chief K lam hinv D hW shat c d = Q2Presentation.Induction.descRead chief K lam hinv D hW (shat c * shat d * (shat (c * d))⁻¹)

theorem Q2Presentation.Induction.pinDelta_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hone : shat 1 = 1) (d : towerC K) : pinDelta chief K lam hinv D hW shat 1 d = 0

theorem Q2Presentation.Induction.pinDelta_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hone : shat 1 = 1) (c : towerC K) : pinDelta chief K lam hinv D hW shat c 1 = 0

theorem Q2Presentation.Induction.pinDelta_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hU : ∀ (c d : towerC K), shat c * shat d * (shat (c * d))⁻¹ ∈ (descKernel chief K lam hinv D hW hne).N) (a b c : towerC K) : pinDelta chief K lam hinv D hW shat a b + pinDelta chief K lam hinv D hW shat (a * b) c = pinDelta chief K lam hinv D hW shat b c + pinDelta chief K lam hinv D hW shat a (b * c)

The factor-set 2-cocycle law of the section-defect reading (deck centrality + descRead-additivity; the multiplicative mirror of the green gRead_cocycle).

§5 The renormalized fibre lift ℓ̂ = pinEll

ellR corrected by the deck coordinate of a quadratic refinement k of gRead + edgeBaseFactor: the ONE budgeted exists_quadRefinement pass (design §4-N10), after which the fibre reading IS edgeBaseFactor.

def Q2Presentation.Induction.pinEll {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) (k : towerM K ⧸ towerT K → ZMod 2) (v : towerM K ⧸ towerT K) : (descTarget chief K lam hinv D hW).Y

The corrected fibre lift ℓ̂(v) := ℓ(v) · z(k v).

Equations

• Q2Presentation.Induction.pinEll chief K lam hinv D hW hne k v = Q2Presentation.Induction.ellR chief K lam hinv D hW v * Q2Presentation.Induction.pinDeck chief K lam hinv D hW hne (k v)

theorem Q2Presentation.Induction.pinEll_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (k : towerM K ⧸ towerT K → ZMod 2) (hk0 : k 0 = 0) : pinEll chief K lam hinv D hW hne k 0 = 1

theorem Q2Presentation.Induction.pinEll_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (k : towerM K ⧸ towerT K → ZMod 2) (v : towerM K ⧸ towerT K) : (descToBt chief K lam hinv D hW hne) (pinEll chief K lam hinv D hW hne k v) = vInG chief K v

theorem Q2Presentation.Induction.pinEll_defect_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (k : towerM K ⧸ towerT K → ZMod 2) (v w : towerM K ⧸ towerT K) : pinEll chief K lam hinv D hW hne k v * pinEll chief K lam hinv D hW hne k w * (pinEll chief K lam hinv D hW hne k (v + w))⁻¹ = ellR chief K lam hinv D hW v * ellR chief K lam hinv D hW w * (ellR chief K lam hinv D hW (v + w))⁻¹ * (pinDeck chief K lam hinv D hW hne (k v) * pinDeck chief K lam hinv D hW hne (k w) * pinDeck chief K lam hinv D hW hne (k (v + w)))

The ℓ̂-defect is the ℓ-defect times the three deck coordinates (centrality + self-inverseness of the deck).

theorem Q2Presentation.Induction.pinEll_defect_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (k : towerM K ⧸ towerT K → ZMod 2) (v w : towerM K ⧸ towerT K) : pinEll chief K lam hinv D hW hne k v * pinEll chief K lam hinv D hW hne k w * (pinEll chief K lam hinv D hW hne k (v + w))⁻¹ ∈ (descKernel chief K lam hinv D hW hne).N

The ℓ̂-defect dies in the deck (fib_mem-slot).

theorem Q2Presentation.Induction.pinEll_read {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) (k : towerM K ⧸ towerT K → ZMod 2) (hkf : ∀ (v w : towerM K ⧸ towerT K), gRead chief K lam hinv D hW v w + ((edgeBaseFactor chief K lam hinv hne) v) w = k (v + w) + k v + k w) (v w : towerM K ⧸ towerT K) : descRead chief K lam hinv D hW (pinEll chief K lam hinv D hW hne k v * pinEll chief K lam hinv D hW hne k w * (pinEll chief K lam hinv D hW hne k (v + w))⁻¹) = ((edgeBaseFactor chief K lam hinv hne) v) w

The renormalized fibre reading IS edgeBaseFactor (fib_read- slot): the deck shift contributes the coboundary ∂k = gRead + f.

§6 The conjugation defect at ℓ̂ (the conj_*-slots)

theorem Q2Presentation.Induction.pinConjElt_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (k : towerM K ⧸ towerT K → ZMod 2) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hproj : ∀ (c : towerC K), (btProj chief K) ((descToBt chief K lam hinv D hW hne) (shat c)) = c) (c : towerC K) (v : towerM K ⧸ towerT K) : shat c * pinEll chief K lam hinv D hW hne k v * (shat c)⁻¹ * (pinEll chief K lam hinv D hW hne k ((headActE chief K c) v))⁻¹ ∈ (descKernel chief K lam hinv D hW hne).N

The ℓ̂-conjugation defect dies in the deck (conj_mem-slot).

theorem Q2Presentation.Induction.pinConj_defect_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (k : towerM K ⧸ towerT K → ZMod 2) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (c : towerC K) (v : towerM K ⧸ towerT K) : shat c * pinEll chief K lam hinv D hW hne k v * (shat c)⁻¹ * (pinEll chief K lam hinv D hW hne k ((headActE chief K c) v))⁻¹ = shat c * ellR chief K lam hinv D hW v * (shat c)⁻¹ * (ellR chief K lam hinv D hW ((headActE chief K c) v))⁻¹ * (pinDeck chief K lam hinv D hW hne (k v) * pinDeck chief K lam hinv D hW hne (k ((headActE chief K c) v)))

The ℓ̂-conjugation defect is the ℓ-conjugation defect times two deck coordinates.

theorem Q2Presentation.Induction.pinConj_read {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) (k : towerM K ⧸ towerT K → ZMod 2) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hproj : ∀ (c : towerC K), (btProj chief K) ((descToBt chief K lam hinv D hW hne) (shat c)) = c) (c : towerC K) (v : towerM K ⧸ towerT K) : descRead chief K lam hinv D hW (shat c * pinEll chief K lam hinv D hW hne k v * (shat c)⁻¹ * (pinEll chief K lam hinv D hW hne k ((headActE chief K c) v))⁻¹) = nRead chief K lam hinv D hW shat c v + k v + k ((headActE chief K c) v)

The ℓ̂-conjugation reading in nRead-coordinates: the deck shift contributes k v + k (c·v).

§7 The exit: pinned existence on the branch

theorem Q2Presentation.Induction.zeroEdgePinnedExistence {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) (hbase : BaseModelExists chief K lam hinv hne) : ∃ (Z : ZeroEdgeDescentData chief K lam hinv), ZeroEdgeDescentDataPinned chief K lam hinv Z

N10 headline — the PINNED zero-edge bundle exists (keep 3's ∃-load (i) discharged): given ZeroEdge and the base model (lem:basedetclass, P6-owned; the §15 TransgressionReading is already theorem-backed), there is a bundle Z together with a ZeroEdgePinning — every cochain slot of Z is an ACTUAL deck read of the descended cover descTarget D hW in the Csec-coordinates (eq:descendedclass + the lem:affinelifting zero-section pullback). Hypotheses, never axioms.

theorem Q2Presentation.Induction.zeroEdgePinnedExistence_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) (M : BaseModelData chief K lam hinv hne) : ∃ (Z : ZeroEdgeDescentData chief K lam hinv), ZeroEdgeDescentDataPinned chief K lam hinv Z

The pinned bundle from the honest branch inputs, Nonempty-model form: BaseModelExists consumed through its Prop-wrapper (same shape as the green zeroEdgeDescentData_nonempty_of_zeroEdge, upgraded to PINNED existence).

theorem Q2Presentation.Induction.zeroEdgePinnedExistence_of_oddHeadAction {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) (hodd : Odd (Nat.card (HeadIm chief K))) : ∃ (Z : ZeroEdgeDescentData chief K lam hinv), ZeroEdgeDescentDataPinned chief K lam hinv Z

The odd-image branch (lem:basedetclass's unramified clause, fully in-tree): pinned existence with the base-model input DISCHARGED by baseModelExists_of_oddHeadAction — the R4b pinned-existence chain is hypothesis-free here beyond hne/hZ/hodd.