Ambient choice layers (normalized at 1/0)

def Q2Presentation.Induction.readSecAmb {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) : p.fst.Y

A choice of ambient representative for a C-class (1-pinned).

Equations

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

theorem Q2Presentation.Induction.readSecAmb_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : readSecAmb chief K 1 = 1

theorem Q2Presentation.Induction.readSecAmb_spec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) : (QuotientGroup.mk' K.Ksub) (readSecAmb chief K c) = c

def Q2Presentation.Induction.readFibK {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : ↥K.Ksub

A choice of kernel representative for a head vector (0-pinned).

Equations

• Q2Presentation.Induction.readFibK chief K v = if v = 0 then 1 else ⋯.choose

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

theorem Q2Presentation.Induction.readFibK_spec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : Submodule.Quotient.mk (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) (readFibK chief K v))) = v

The composite projection formula (three Noether layers)

theorem Q2Presentation.Induction.descCollapse_mk_mk {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) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (descCollapse chief K lam hinv D hW hne) ((QuotientGroup.mk' (descKernel chief K lam hinv D hW hne).N) ((descProj chief K lam hinv D hW) b)) = (QuotientGroup.mk' (tCover chief K lam hinv)) b

Layer 1: the deck collapse on a double class.

theorem Q2Presentation.Induction.tCoverCollapseAmbient_mk {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 : p.fst.Y) : (tCoverCollapseAmbient chief K lam hinv) ((QuotientGroup.mk' (tCover chief K lam hinv)) ((Lifting.scalarProj (xrKernel chief K) lam hinv) x)) = (QuotientGroup.mk' (tAmbient chief K)) x

Layer 2: the T̃-collapse in ambient form.

theorem Q2Presentation.Induction.tChildCollapseAmbient_symm_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : p.fst.Y) : (tChildCollapseAmbient chief K).symm ((QuotientGroup.mk' (tAmbient chief K)) x) = (QuotientGroup.mk' (tChild chief K)) (childMk chief K x)

Layer 3: the child T-collapse, symm direction.

theorem Q2Presentation.Induction.descToBt_descProj_scalarProj {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) (x : p.fst.Y) : (descToBt chief K lam hinv D hW hne) ((descProj chief K lam hinv D hW) ((Lifting.scalarProj (xrKernel chief K) lam hinv) x)) = (QuotientGroup.mk' (tChild chief K)) (childMk chief K x)

The composite projection formula: the descended cover maps onto B/T' by the child class of the ambient element.

Deck tools: kernel characterization, surjectivity, readings

theorem Q2Presentation.Induction.descToBt_eq_one_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (x : (descTarget chief K lam hinv D hW).Y) : (descToBt chief K lam hinv D hW hne) x = 1 ↔ x ∈ (descKernel chief K lam hinv D hW hne).N

Membership in the descended deck = dying under the cover map.

theorem Q2Presentation.Induction.descToBt_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : Function.Surjective ⇑(descToBt chief K lam hinv D hW hne)

theorem Q2Presentation.Induction.descRead_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) : descRead chief K lam hinv D hW 1 = 0

theorem Q2Presentation.Induction.descRead_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (x : (descTarget chief K lam hinv D hW).Y) : descRead chief K lam hinv D hW x = 0 ↔ x = 1

theorem Q2Presentation.Induction.descRead_mul {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) (a b : (descTarget chief K lam hinv D hW).Y) (ha : a ∈ (descKernel chief K lam hinv D hW hne).N) (hb : b ∈ (descKernel chief K lam hinv D hW hne).N) : descRead chief K lam hinv D hW (a * b) = descRead chief K lam hinv D hW a + descRead chief K lam hinv D hW b

Additivity of the deck reading (order-2 kernel).

theorem Q2Presentation.Induction.descKernel_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) (z g : (descTarget chief K lam hinv D hW).Y) (hz : z ∈ (descKernel chief K lam hinv D hW hne).N) : g * z = z * g

The deck is central in the descended cover (elementwise form).

theorem Q2Presentation.Induction.mem_relN_of_kernelFrattini {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)) (r : p.fst.Y) (hr : r ∈ kernelFrattini K) : (Lifting.scalarProj (xrKernel chief K) lam hinv) r ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N

Frattini-layer elements land in the deck of the λ-cover.

theorem Q2Presentation.Induction.descRead_descProj {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) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) (hz : z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N) : descRead chief K lam hinv D hW ((descProj chief K lam hinv D hW) z) = relRead chief K lam hinv z

The deck reading transports along descProj (W ⊓ relN = ⊥).

The lifted section and fibre choices

def Q2Presentation.Induction.sigmaHatR {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) (c : towerC K) : (descTarget chief K lam hinv D hW).Y

The lifted base-section choice σ̂ : C → descTarget D hW.

Equations

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

theorem Q2Presentation.Induction.sigmaHatR_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) : sigmaHatR chief K lam hinv D hW 1 = 1

theorem Q2Presentation.Induction.sigmaHatR_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) (c : towerC K) : (btProj chief K) ((descToBt chief K lam hinv D hW hne) (sigmaHatR chief K lam hinv D hW c)) = c

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

The lifted fibre choice ℓ : V → descTarget D hW.

Equations

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

theorem Q2Presentation.Induction.ellR_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) : ellR chief K lam hinv D hW 0 = 1

theorem Q2Presentation.Induction.ellR_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) (v : towerM K ⧸ towerT K) : (descToBt chief K lam hinv D hW hne) (ellR chief K lam hinv D hW v) = vInG chief K v

The fibre lift covers the fibre inclusion: p(ℓ v) = vInG v.

The crux readings: squares and commutators of fibre lifts

theorem Q2Presentation.Induction.edgeHeadForm_mk {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) (m : towerM K) : (edgeHeadForm chief K lam hinv hne).form (Submodule.Quotient.mk m) = (sec7SquareFamily chief K lam).form m

Descend-form bridge at the head form (rfl at Annihilates.descend).

theorem Q2Presentation.Induction.edgeHeadPolar_mk {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) (m m' : towerM K) : ((edgeHeadForm chief K lam hinv hne).polar (Submodule.Quotient.mk m)) (Submodule.Quotient.mk m') = ((sec7SquareFamily chief K lam).polar m) m'

Descend-form bridge at the polar form.

theorem Q2Presentation.Induction.readSq {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) (v : towerM K ⧸ towerT K) : descRead chief K lam hinv D hW (ellR chief K lam hinv D hW v * ellR chief K lam hinv D hW v) = (edgeHeadForm chief K lam hinv hne).form v

Squares of fibre lifts read the head form (the crux alignment scalarProj_sq_eq_form through the deck transport).

theorem Q2Presentation.Induction.readComm {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) (v w : towerM K ⧸ towerT K) : descRead chief K lam hinv D hW ⁅ellR chief K lam hinv D hW v, ellR chief K lam hinv D hW w⁆ = ((edgeHeadForm chief K lam hinv hne).polar v) w

Commutators of fibre lifts read the polar form.

The fibre factor cochain g and its laws

def Q2Presentation.Induction.gRead {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) (v w : towerM K ⧸ towerT K) : ZMod 2

The fibre factor cochain: the deck coordinate of ℓ(v)ℓ(w)ℓ(v+w)⁻¹.

Equations

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

theorem Q2Presentation.Induction.gElt_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) (v w : towerM K ⧸ towerT K) : 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))⁻¹ ∈ (descKernel chief K lam hinv D hW hne).N

The factor element lies in the deck.

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

theorem Q2Presentation.Induction.gRead_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)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (v w : towerM K ⧸ towerT K) : gRead chief K lam hinv D hW v w + gRead chief K lam hinv D hW w v = ((edgeHeadForm chief K lam hinv hne).polar v) w

theorem Q2Presentation.Induction.gRead_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) (u v w : towerM K ⧸ towerT K) : gRead chief K lam hinv D hW u v + gRead chief K lam hinv D hW (u + v) w = gRead chief K lam hinv D hW v w + gRead chief K lam hinv D hW u (v + w)

Generic conjugation-defect machinery over an abstract lift

def Q2Presentation.Induction.nRead {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 : towerC K) (v : towerM K ⧸ towerT K) : ZMod 2

The conjugation-defect reading n of an abstract lift.

Equations

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

theorem Q2Presentation.Induction.nElt_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) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hne : lam ≠ 0) (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 * ellR chief K lam hinv D hW v * (shat c)⁻¹ * (ellR chief K lam hinv D hW ((headActE chief K c) v))⁻¹ ∈ (descKernel chief K lam hinv D hW hne).N

theorem Q2Presentation.Induction.nRead_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) (shat : towerC K → (descTarget chief K lam hinv D hW).Y) (hone : shat 1 = 1) (v : towerM K ⧸ towerT K) : nRead chief K lam hinv D hW shat 1 v = 0

theorem Q2Presentation.Induction.nElt_recover {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 : towerC K) (v : towerM K ⧸ towerT K) : shat c * ellR chief K lam hinv D hW v * (shat c)⁻¹ = shat c * ellR chief K lam hinv D hW v * (shat c)⁻¹ * (ellR chief K lam hinv D hW ((headActE chief K c) v))⁻¹ * ellR chief K lam hinv D hW ((headActE chief K c) v)

theorem Q2Presentation.Induction.gElt_recover {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) (v w : towerM K ⧸ towerT K) : ellR chief K lam hinv D hW v * ellR chief K lam hinv D hW 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))⁻¹ * ellR chief K lam hinv D hW (v + w)

theorem Q2Presentation.Induction.nRead_quadratic {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) (hne : lam ≠ 0) (hproj : ∀ (c : towerC K), (btProj chief K) ((descToBt chief K lam hinv D hW hne) (shat c)) = c) (c : towerC K) (v w : towerM K ⧸ towerT K) : nRead chief K lam hinv D hW shat c (v + w) + nRead chief K lam hinv D hW shat c v + nRead chief K lam hinv D hW shat c w = gRead chief K lam hinv D hW ((headActE chief K c) v) ((headActE chief K c) w) + gRead chief K lam hinv D hW v w

The (†) quadratic law of the conjugation defect.

theorem Q2Presentation.Induction.commElt_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) (v w : towerM K ⧸ towerT K) : ⁅ellR chief K lam hinv D hW v, ellR chief K lam hinv D hW w⁆ ∈ (descKernel chief K lam hinv D hW hne).N

Commutators of fibre lifts lie in the deck (vLayer is abelian).

theorem Q2Presentation.Induction.nRead_coherent {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) (hne : lam ≠ 0) (hproj : ∀ (c : towerC K), (btProj chief K) ((descToBt chief K lam hinv D hW hne) (shat c)) = c) (eta0 : towerC K → towerC K → towerM K ⧸ towerT K) (heta : ∀ (c d : towerC K), shat c * shat d * (shat (c * d))⁻¹ * (ellR chief K lam hinv D hW (eta0 c d))⁻¹ ∈ (descKernel chief K lam hinv D hW hne).N) (c d : towerC K) (v : towerM K ⧸ towerT K) : nRead chief K lam hinv D hW shat c ((headActE chief K d) v) + nRead chief K lam hinv D hW shat d v + nRead chief K lam hinv D hW shat (c * d) v = ((edgeHeadForm chief K lam hinv hne).polar (eta0 c d)) ((headActE chief K (c * d)) v)

The (‡) transgression-coherence law against an eta0-witness (eq:transgressioncochain, concrete).

The σ-instantiation: TransgressionReading on the branch

theorem Q2Presentation.Induction.exists_vInG_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) (hx : x ∈ vLayer chief K) : ∃ (v : towerM K ⧸ towerT K), vInG chief K v = x

The fibre inclusion is onto the V-layer.

theorem Q2Presentation.Induction.transgressionReading_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) (hZ : ZeroEdge chief K lam hinv) : TransgressionReading chief K lam hinv hne

(A) TransgressionReading holds on the zero-edge branch — the §15 σ-instantiation of the generic reading machinery.

The s-instantiation: a Csec-section, its lift, and the model

theorem Q2Presentation.Induction.exists_csec_over {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) (c : towerC K) : ∃ x ∈ Csec, (btProj chief K) x = c

theorem Q2Presentation.Induction.csec_over_unique {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hdisj : Csec ⊓ vLayer chief K = ⊥) {x y : (btChild chief K).fst.Y} (hx : x ∈ Csec) (hy : y ∈ Csec) (hxy : (btProj chief K) x = (btProj chief K) y) : x = y

def Q2Presentation.Induction.csecSec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) (c : towerC K) : (btChild chief K).fst.Y

The 1-pinned choice of Csec-representatives.

Equations

• Q2Presentation.Induction.csecSec chief K Csec hsup c = if c = 1 then 1 else ⋯.choose

theorem Q2Presentation.Induction.csecSec_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) : csecSec chief K Csec hsup 1 = 1

theorem Q2Presentation.Induction.csecSec_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) (c : towerC K) : csecSec chief K Csec hsup c ∈ Csec

theorem Q2Presentation.Induction.csecSec_sec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) (c : towerC K) : (btProj chief K) (csecSec chief K Csec hsup c) = c

theorem Q2Presentation.Induction.csecSec_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Csec : Subgroup (btChild chief K).fst.Y) (hdisj : Csec ⊓ vLayer chief K = ⊥) (hsup : Csec ⊔ vLayer chief K = ⊤) (c d : towerC K) : csecSec chief K Csec hsup c * csecSec chief K Csec hsup d = csecSec chief K Csec hsup (c * d)

The Csec-section is multiplicative (complement uniqueness).

def Q2Presentation.Induction.csecLift {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) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) (c : towerC K) : (descTarget chief K lam hinv D hW).Y

The choice-lift of the Csec-section through the descended cover.

Equations

• Q2Presentation.Induction.csecLift chief K lam hinv D hW hne Csec hsup c = if c = 1 then 1 else ⋯.choose

theorem Q2Presentation.Induction.csecLift_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) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) : csecLift chief K lam hinv D hW hne Csec hsup 1 = 1

theorem Q2Presentation.Induction.csecLift_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) (Csec : Subgroup (btChild chief K).fst.Y) (hsup : Csec ⊔ vLayer chief K = ⊤) (c : towerC K) : (descToBt chief K lam hinv D hW hne) (csecLift chief K lam hinv D hW hne Csec hsup c) = csecSec chief K Csec hsup c

theorem Q2Presentation.Induction.baseModelExists_of_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) (hZ : ZeroEdge chief K lam hinv) (hsplit : SplitsBtChild chief K) : BaseModelExists chief K lam hinv hne

(B⟸) The κ_q⁰-model exists given the splitting (on the branch): the multiplicative Csec-section lifts through the cover, its conjugation defect is COHERENT (vanishing section cochain, (‡) at eta0 = 0), and the exists_quadRefinement correction m := n̂ + k∘c + k converts the g-quadratic law into the edgeBaseFactor law — once split, the restricted cover IS an equivariant class.

The discharge theorems (keep-3 upgrade interface)

theorem Q2Presentation.Induction.btChild_splits_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) (hZ : ZeroEdge chief K lam hinv) (hbase : BaseModelExists chief K lam hinv hne) : SplitsBtChild chief K

btChild splits given ZeroEdge + the model — after this file the R4b transgression chain's only named input is BaseModelExists.

theorem Q2Presentation.Induction.baseModelExists_iff_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) (hZ : ZeroEdge chief K lam hinv) : BaseModelExists chief K lam hinv hne ↔ SplitsBtChild chief K

(B) On the zero-edge branch the κ_q⁰-model is EQUIVALENT to the splitting — the residual arithmetic input is pinned exactly: BaseModelExists unconditionally is lem:basedetclass at the head (l.2286–2360, tame projectivity/Maschke; P6-owned), and NOTHING weaker suffices on this branch.

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

The U8 bundle exists on the branch given only the model — the zeroEdgeDescentData_nonempty consumer with TransgressionReading DISCHARGED.