The quadratic-refinement carrier (QRef): a symmetric zero-diagonal

normalized 2-cocycle on V twists V × 𝔽₂ into an exponent-2 module

structure Q2Presentation.Induction.QRefPkg {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

A symmetric zero-diagonal normalized 2-cocycle on the head V (the difference g + f of two factor cochains with equal squares and equal symmetry defect — lem:transgression's section-change freedom).

• h : towerM K ⧸ towerT K → towerM K ⧸ towerT K → ZMod 2
• hsym (v w : towerM K ⧸ towerT K) : self.h v w = self.h w v
• hdiag (v : towerM K ⧸ towerT K) : self.h v v = 0
• hzero (w : towerM K ⧸ towerT K) : self.h 0 w = 0
• hcoc (u v w : towerM K ⧸ towerT K) : self.h u v + self.h (u + v) w = self.h v w + self.h u (v + w)

def Q2Presentation.Induction.QRef {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (_P : QRefPkg chief K) : Type

The twisted carrier V × 𝔽₂ (type synonym; own instances only).

Equations

• Q2Presentation.Induction.QRef chief K _P = ((Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K) × ZMod 2)

def Q2Presentation.Induction.QRef.mk {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (P : QRefPkg chief K) (v : towerM K ⧸ towerT K) (s : ZMod 2) : QRef chief K P

Constructor (hygiene def for the synonym carrier).

Equations

• Q2Presentation.Induction.QRef.mk P v s = (v, s)

def Q2Presentation.Induction.QRef.fst {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} (x : QRef chief K P) : towerM K ⧸ towerT K

First component.

Equations

• x.fst = x.1

def Q2Presentation.Induction.QRef.snd {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} (x : QRef chief K P) : ZMod 2

Second component.

Equations

• x.snd = x.2

theorem Q2Presentation.Induction.QRef.ext {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} {x y : QRef chief K P} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y

instance Q2Presentation.Induction.instZeroQRef {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P : QRefPkg chief K) : Zero (QRef chief K P)

Equations

• Q2Presentation.Induction.instZeroQRef chief K P = { zero := Q2Presentation.Induction.QRef.mk P 0 0 }

instance Q2Presentation.Induction.instAddQRef {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P : QRefPkg chief K) : Add (QRef chief K P)

Equations

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

instance Q2Presentation.Induction.instNegQRef {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P : QRefPkg chief K) : Neg (QRef chief K P)

Equations

• Q2Presentation.Induction.instNegQRef chief K P = { neg := fun (x : Q2Presentation.Induction.QRef chief K P) => x }

@[simp]

theorem Q2Presentation.Induction.QRef.add_fst {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} (x y : QRef chief K P) : (x + y).fst = x.fst + y.fst

@[simp]

theorem Q2Presentation.Induction.QRef.add_snd {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} (x y : QRef chief K P) : (x + y).snd = x.snd + y.snd + P.h x.fst y.fst

@[simp]

theorem Q2Presentation.Induction.QRef.zero_fst {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} : fst 0 = 0

@[simp]

theorem Q2Presentation.Induction.QRef.zero_snd {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {P : QRefPkg chief K} : snd 0 = 0

theorem Q2Presentation.Induction.QRefPkg.hzero' {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (P : QRefPkg chief K) (v : towerM K ⧸ towerT K) : P.h v 0 = 0

instance Q2Presentation.Induction.instAddCommGroupQRef {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P : QRefPkg chief K) : AddCommGroup (QRef chief K P)

Equations

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

instance Q2Presentation.Induction.instModuleZModOfNatNatQRef {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P : QRefPkg chief K) : Module (ZMod 2) (QRef chief K P)

Equations

• Q2Presentation.Induction.instModuleZModOfNatNatQRef chief K P = AddCommGroup.zmodModule ⋯

def Q2Presentation.Induction.QRef.incl {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (P : QRefPkg chief K) : ZMod 2 →ₗ[ZMod 2] QRef chief K P

The central inclusion 𝔽₂ → QRef (linear; the deck slot).

Equations

• Q2Presentation.Induction.QRef.incl P = AddMonoidHom.toZModLinearMap 2 (AddMonoidHom.mk' (fun (s : ZMod 2) => Q2Presentation.Induction.QRef.mk P 0 s) ⋯)

@[simp]

theorem Q2Presentation.Induction.QRef.incl_apply {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (P : QRefPkg chief K) (s : ZMod 2) : (incl P) s = mk P 0 s

theorem Q2Presentation.Induction.QRef.incl_injective {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (P : QRefPkg chief K) : Function.Injective ⇑(incl P)

theorem Q2Presentation.Induction.exists_quadRefinement {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P : QRefPkg chief K) : ∃ (k : towerM K ⧸ towerT K → ZMod 2), k 0 = 0 ∧ ∀ (v w : towerM K ⧸ towerT K), P.h v w = k (v + w) + k v + k w

Quadratic refinement exists: a symmetric zero-diagonal normalized 2-cocycle on the head is a coboundary h(v,w) = k(v+w) + k(v) + k(w) (lem:transgression's section-renormalization step: split the central 𝔽₂ out of the exponent-2 extension QRef linearly).

The engine: η is exactly a twisted coboundary

theorem Q2Presentation.Induction.transgression_coboundary {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) (g : towerM K ⧸ towerT K → towerM K ⧸ towerT K → ZMod 2) (hgdiag : ∀ (v : towerM K ⧸ towerT K), g v v = (edgeHeadForm chief K lam hinv hne).form v) (hgpolar : ∀ (v w : towerM K ⧸ towerT K), g v w + g w v = ((edgeHeadForm chief K lam hinv hne).polar v) w) (hgcoc : ∀ (u v w : towerM K ⧸ towerT K), g u v + g (u + v) w = g v w + g u (v + w)) (n : towerC K → towerM K ⧸ towerT K → ZMod 2) (hnone : ∀ (v : towerM K ⧸ towerT K), n 1 v = 0) (hnquad : ∀ (c : towerC K) (v w : towerM K ⧸ towerT K), n c (v + w) + n c v + n c w = g ((headActE chief K c) v) ((headActE chief K c) w) + g v w) (eta : towerC K → towerC K → towerM K ⧸ towerT K) (hncoh : ∀ (c d : towerC K) (v : towerM K ⧸ towerT K), n c ((headActE chief K d) v) + n d v + n (c * d) v = ((edgeHeadForm chief K lam hinv hne).polar (eta c d)) ((headActE chief K (c * d)) v)) (m : towerC K → towerM K ⧸ towerT K → ZMod 2) (hmone : ∀ (v : towerM K ⧸ towerT K), m 1 v = 0) (hmquad : ∀ (c : towerC K) (v w : towerM K ⧸ towerT K), m c (v + w) + m c v + 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) (hmcoh : ∀ (c d : towerC K) (v : towerM K ⧸ towerT K), m (c * d) v = m c ((headActE chief K d) v) + m d v) : ∃ (a : towerC K → towerM K ⧸ towerT K), a 1 = 0 ∧ ∀ (c d : towerC K), a (c * d) = a c + (headActE chief K c) (a d) + eta c d

The transgression engine (lem:transgression l.3464–3530, cochain form; design §4.7's "one genuinely heavy provable unit", automorphism-free): given the fibre factor cochain g of the descended cover (squares q̄_λ, symmetry defect the polar form, cocycle law), the conjugation-defect cochain n (normalized; quadratic law (†); transgression coherence (‡) n_c(dv) + n_d(v) + n_{cd}(v) = b̄(η(c,d), (cd)v) — the concrete eq:transgressioncochain), and a κ_q⁰-model m (eq:mquadratic/eq:mcoherent), the section cochain η is EXACTLY a twisted coboundary: a(cd) = a(c) + c·a(d) + η(c,d) with a(1) = 0. Nonsingularity of q̄_λ enters through edgePolarEquiv.