Char-2 and head-action helpers

theorem Q2Presentation.Induction.headActE_cancel_left {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

Left inverse-cancellation of the head action: c⁻¹·(c·v) = v (from headActE_cancel at c⁻¹).

Carrier readout helpers (the one-spelling discipline: every

cochain below reads z.val and lowerBar — never a rewrapping)

theorem Q2Presentation.Induction.edgeZ1_val_add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z w : ↥(edgeZ1 chief K B ρ)) (γ : ↑Γ.toProfinite.toTop) : ↑(z + w) γ = ↑z γ + ↑w γ

Pointwise readout of a sum in Z¹_ρ(V) (Pi/Submodule transparency, banked as an explicit rfl-lemma).

theorem Q2Presentation.Induction.edgeZ1_val_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ : ↑Γ.toProfinite.toTop) : ↑0 γ = 0

Pointwise readout of the zero cocycle.

theorem Q2Presentation.Induction.edgeZ1_val_law {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : ↑z (γ * γ') = ↑z γ + (headActE chief K (lowerBar chief K B ρ γ)) (↑z γ')

The twisted law, subtype form (THE orientation pin of N1: z(γγ′) = z(γ) + ρ̄(γ)·z(γ′)).

theorem Q2Presentation.Induction.edgeZ1_val_lc {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : IsLocallyConstant ↑z

Local constancy, subtype form.

theorem Q2Presentation.Induction.edgeZ1_val_one' {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : ↑z 1 = 0

Normalization, subtype form.

theorem Q2Presentation.Induction.lowerBar_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Function.Surjective (lowerBar chief K B ρ)

ρ̄ is onto C (the framed surjection composed with the collapse equivalence) — the B¹(V)-orbit freeness input.

The defect cochains of the z-twisted lift, in pinning

coordinates (eq:descendedclass l.4038–4045 read along the graph of z; design §4-N7 bullet 1)

def Q2Presentation.Induction.edgeF0 {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The quadratic defect leg F₀(z) — the κ_q⁰-model graph read along the z-twisted lift: F₀(z)(γ,γ′) = f(z γ, ρ̄γ·z γ′) + m_{ρ̄γ}(z γ′) (the thetaGraph shape at the source).

Equations

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

theorem Q2Presentation.Induction.edgeF0_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : edgeF0 chief K lam hinv Z B ρ z γ γ' = ((edgeBaseFactor chief K lam hinv ⋯) (↑z γ)) ((headActE chief K (lowerBar chief K B ρ γ)) (↑z γ')) + Z.mC (lowerBar chief K B ρ γ) (↑z γ')

def Q2Presentation.Induction.edgeGraph {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (phi : towerC K → Module.Dual (ZMod 2) (towerM K ⧸ towerT K)) (z : ↥(edgeZ1 chief K B ρ)) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The graph leg at a twisted dual-valued 1-cochain φ (used at φ = Z.gammaK — the Γ_{γ_κ}-term of eq:Gammagamma — and at φ = gammaChi χ — the χ-constraint reads): (γ,γ′) ↦ φ(ρ̄γ)(ρ̄γ·z γ′).

Equations

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

theorem Q2Presentation.Induction.edgeGraph_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (phi : towerC K → Module.Dual (ZMod 2) (towerM K ⧸ towerT K)) (z : ↥(edgeZ1 chief K B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : edgeGraph chief K B ρ phi z γ γ' = (phi (lowerBar chief K B ρ γ)) ((headActE chief K (lowerBar chief K B ρ γ)) (↑z γ'))

def Q2Presentation.Induction.edgeEps {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The constant leg inf δ_κ: (γ,γ′) ↦ δ_κ(ρ̄γ, ρ̄γ′).

Equations

• Q2Presentation.Induction.edgeEps chief K lam hinv Z B ρ γ γ' = Z.deltaK (Q2Presentation.Induction.lowerBar chief K B ρ γ) (Q2Presentation.Induction.lowerBar chief K B ρ γ')

theorem Q2Presentation.Induction.edgeEps_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ γ' : ↑Γ.toProfinite.toTop) : edgeEps chief K lam hinv Z B ρ γ γ' = Z.deltaK (lowerBar chief K B ρ γ) (lowerBar chief K B ρ γ')

def Q2Presentation.Induction.edgeChiE {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The χ-pushout of the affine target e: (γ,γ′) ↦ χ(e(ρ̄γ, ρ̄γ′)) — the ρ*(χ_*e)-cochain whose ι-reading is the engine's κ₀-slot (eq:affineequation l.4060).

Equations

• Q2Presentation.Induction.edgeChiE chief K lam hinv Z B ρ chi γ γ' = ↑chi (Z.eT (Q2Presentation.Induction.lowerBar chief K B ρ γ) (Q2Presentation.Induction.lowerBar chief K B ρ γ'))

theorem Q2Presentation.Induction.edgeChiE_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) (γ γ' : ↑Γ.toProfinite.toTop) : edgeChiE chief K lam hinv Z B ρ chi γ γ' = ↑chi (Z.eT (lowerBar chief K B ρ γ) (lowerBar chief K B ρ γ'))

def Q2Presentation.Induction.edgePair {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (x y : ↥(edgeZ1 chief K B ρ)) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The polar pairing cochain P(x,y)(γ,γ′) = b(y γ, ρ̄γ·x γ′) — the cross term of the completed square (design §4-N7 bullet 2); its ι-reading is edgeQ's polar form.

Equations

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

theorem Q2Presentation.Induction.edgePair_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (x y : ↥(edgeZ1 chief K B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : edgePair chief K lam hinv Z B ρ x y γ γ' = ((edgeHeadForm chief K lam hinv ⋯).polar (↑y γ)) ((headActE chief K (lowerBar chief K B ρ γ)) (↑x γ'))

def Q2Presentation.Induction.edgeDefectFull {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The full defect cochain F(z) of the z-twisted lift through descTarget (eq:descendedclass along the graph): `F₀(z) + Γ_{γ_κ}(z)

• ρ*δ_κ— thel/ε-split of eq:Qkappadifference` (l.2158–2163) is this sum's shape, and the pinned-lift bridge below reads it off the actual cover.

Equations

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

theorem Q2Presentation.Induction.edgeDefectFull_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : edgeDefectFull chief K lam hinv Z B ρ z γ γ' = edgeF0 chief K lam hinv Z B ρ z γ γ' + edgeGraph chief K B ρ Z.gammaK z γ γ' + edgeEps chief K lam hinv Z B ρ γ γ'

The normalized-2-cocycle laws (the IotaToken carrier class)

theorem Q2Presentation.Induction.isNormalized2Cocycle_edgeF0 {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : IsNormalized2Cocycle Γ (edgeF0 chief K lam hinv Z B ρ z)

F₀(z) is a normalized continuous 2-cocycle (the Γ-level theta_cocycle_core algebra: bilinearity of f + the m-laws + the twisted law of z).

theorem Q2Presentation.Induction.isNormalized2Cocycle_edgeGraph {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (phi : towerC K → Module.Dual (ZMod 2) (towerM K ⧸ towerT K)) (hphi1 : phi 1 = 0) (hphic : ∀ (c d : towerC K) (v : towerM K ⧸ towerT K), (phi (c * d)) v = (phi c) v + (phi d) ((headActE chief K c⁻¹) v)) (z : ↥(edgeZ1 chief K B ρ)) : IsNormalized2Cocycle Γ (edgeGraph chief K B ρ phi z)

edgeGraph φ z is a normalized continuous 2-cocycle, for any normalized twisted 1-cochain φ in the gammaK_cocycle orientation.

theorem Q2Presentation.Induction.isNormalized2Cocycle_edgeEps {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : IsNormalized2Cocycle Γ (edgeEps chief K lam hinv Z B ρ)

ρ*δ_κ is a normalized continuous 2-cocycle (pullback of the bundle laws along ρ̄).

theorem Q2Presentation.Induction.isNormalized2Cocycle_edgeChiE {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) : IsNormalized2Cocycle Γ (edgeChiE chief K lam hinv Z B ρ chi)

ρ*(χ_*e) is a normalized continuous 2-cocycle (the χ-invariance chi_act kills the eT-twist — the DeltaC_cocycle hE-step).

theorem Q2Presentation.Induction.isNormalized2Cocycle_edgePair {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (x y : ↥(edgeZ1 chief K B ρ)) : IsNormalized2Cocycle Γ (edgePair chief K lam hinv Z B ρ x y)

edgePair x y is a normalized continuous 2-cocycle (polar act-invariance + the twisted laws of x and y).

theorem Q2Presentation.Induction.isNormalized2Cocycle_edgeDefectFull {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : IsNormalized2Cocycle Γ (edgeDefectFull chief K lam hinv Z B ρ z)

The full defect F(z) is a normalized continuous 2-cocycle.

The completed-square and additivity cochain identities

(design §4-N7 bullet 2: every identity is EXPLICIT — a pointwise equation with a named locally constant coboundary witness)

theorem Q2Presentation.Induction.edgeF0_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z w : ↥(edgeZ1 chief K B ρ)) : edgeF0 chief K lam hinv Z B ρ (z + w) = edgeF0 chief K lam hinv Z B ρ z + edgeF0 chief K lam hinv Z B ρ w + edgePair chief K lam hinv Z B ρ z w + cochainCoboundary Γ fun (γ : ↑Γ.toProfinite.toTop) => ((edgeBaseFactor chief K lam hinv ⋯) (↑z γ)) (↑w γ)

The completed-square identity for F₀: F₀(z+w) = F₀(z) + F₀(w) + P(z,w) + δ(γ ↦ f(z γ, w γ)) — the cochain-level prop:phaseidentity cross-term computation.

theorem Q2Presentation.Induction.edgeF0_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : edgeF0 chief K lam hinv Z B ρ 0 = 0

edgeF0 at the zero cocycle is the zero cochain.

theorem Q2Presentation.Induction.edgePair_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (x x' y : ↥(edgeZ1 chief K B ρ)) : edgePair chief K lam hinv Z B ρ (x + x') y = edgePair chief K lam hinv Z B ρ x y + edgePair chief K lam hinv Z B ρ x' y

Pointwise additivity of the pairing cochain in the first slot.

theorem Q2Presentation.Induction.edgePair_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (x y y' : ↥(edgeZ1 chief K B ρ)) : edgePair chief K lam hinv Z B ρ x (y + y') = edgePair chief K lam hinv Z B ρ x y + edgePair chief K lam hinv Z B ρ x y'

Pointwise additivity of the pairing cochain in the second slot.

theorem Q2Presentation.Induction.edgeGraph_add_z {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (phi : towerC K → Module.Dual (ZMod 2) (towerM K ⧸ towerT K)) (z w : ↥(edgeZ1 chief K B ρ)) : edgeGraph chief K B ρ phi (z + w) = edgeGraph chief K B ρ phi z + edgeGraph chief K B ρ phi w

Pointwise additivity of the graph cochain in the cocycle slot.

χ-additivity of the constraint legs, and the pulled

representing cocycle edgeA

theorem Q2Presentation.Induction.gammaChi_add_chi {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi chi' : ↥(XT chief K)) (c : towerC K) (v : towerM K ⧸ towerT K) : (gammaChi chief K (chi + chi') c) v = (gammaChi chief K chi c) v + (gammaChi chief K chi' c) v

γ_χ is additive in χ (pointwise, via the retracted extension).

theorem Q2Presentation.Induction.edgeChiE_add_chi {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi chi' : ↥(XT chief K)) : edgeChiE chief K lam hinv Z B ρ (chi + chi') = edgeChiE chief K lam hinv Z B ρ chi + edgeChiE chief K lam hinv Z B ρ chi'

ρ*(χ_*e) is additive in χ (pointwise).

theorem Q2Presentation.Induction.edgeChiE_zero_chi {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : edgeChiE chief K lam hinv Z B ρ 0 = 0

ρ*(χ_*e) at χ = 0 is the zero cochain.

def Q2Presentation.Induction.edgeA {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) : ↥(edgeZ1 chief K B ρ)

a_{χ,κ} pulled to the cocycle level (design §4-N7 bullet 3): γ ↦ a_{χ,κ}(ρ̄γ) is a ρ̄-twisted cocycle — the engine's representing vector at χ.

Equations

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

theorem Q2Presentation.Induction.edgeA_val {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) (γ : ↑Γ.toProfinite.toTop) : ↑(edgeA chief K lam hinv Z B ρ chi) γ = aRep chief K lam hinv Z chi (lowerBar chief K B ρ γ)

theorem Q2Presentation.Induction.edgePair_edgeA {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) (z : ↥(edgeZ1 chief K B ρ)) : edgePair chief K lam hinv Z B ρ (edgeA chief K lam hinv Z B ρ chi) z = edgeGraph chief K B ρ (gammaChi chief K chi) z + edgeGraph chief K B ρ Z.gammaK z + cochainCoboundary Γ fun (γ : ↑Γ.toProfinite.toTop) => (gammaChi chief K chi (lowerBar chief K B ρ γ)) (↑z γ) + (Z.gammaK (lowerBar chief K B ρ γ)) (↑z γ)

The polar-representation identity at edgeA (the gammaChi-pairing computation, design §4-N7 bullet 3): pairing against the pulled representing cocycle reads the two graph legs, up to an explicit continuous coboundary — the cochain-level b_q̄(a_χ, ·) = γ_χ + γ_κ.

The solvability-indicator readings and the QuadF2 structure

(design §2.1: Q(z) := ι(F₀ z) — token-free DEFINITIONS, token-consuming LAWS; downstream reads iotaRead, never raw case splits)

def Q2Presentation.Induction.edgeQForm {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : ZMod 2

The liftability form Q(z) = ι_Γ(F₀ z).

Equations

• Q2Presentation.Induction.edgeQForm chief K lam hinv Z B ρ z = Q2Presentation.Induction.iotaRead Γ (Q2Presentation.Induction.edgeF0 chief K lam hinv Z B ρ z)

def Q2Presentation.Induction.edgePolarBit {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (x y : ↥(edgeZ1 chief K B ρ)) : ZMod 2

The polar bit β(x,y) = ι_Γ(P(x,y)).

Equations

• Q2Presentation.Induction.edgePolarBit chief K lam hinv Z B ρ x y = Q2Presentation.Induction.iotaRead Γ (Q2Presentation.Induction.edgePair chief K lam hinv Z B ρ x y)

def Q2Presentation.Induction.edgeEllRead {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) : ZMod 2

The linear leg ℓ(z) = ι_Γ(Γ_{γ_κ}(z)) (eq:Qkappadifference's linear term).

Equations

• Q2Presentation.Induction.edgeEllRead chief K lam hinv Z B ρ z = Q2Presentation.Induction.iotaRead Γ (Q2Presentation.Induction.edgeGraph chief K B ρ Z.gammaK z)

def Q2Presentation.Induction.edgeLRead {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(edgeZ1 chief K B ρ)) (chi : ↥(XT chief K)) : ZMod 2

The χ-constraint reading L(z)(χ) = ι_Γ(Γ_{γ_χ}(z)) (token-free def; linearity is token-consuming).

Equations

• Q2Presentation.Induction.edgeLRead chief K B ρ z chi = Q2Presentation.Induction.iotaRead Γ (Q2Presentation.Induction.edgeGraph chief K B ρ (Q2Presentation.Induction.gammaChi chief K chi) z)

def Q2Presentation.Induction.edgeKappaRead {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) : ZMod 2

The constraint target κ₀(χ) = ι_Γ(ρ*(χ_*e)).

Equations

• Q2Presentation.Induction.edgeKappaRead chief K lam hinv Z B ρ chi = Q2Presentation.Induction.iotaRead Γ (Q2Presentation.Induction.edgeChiE chief K lam hinv Z B ρ chi)

def Q2Presentation.Induction.edgeEpsRead {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : ZMod 2

The constant slot ε₀ = ι_Γ(ρ*δ_κ).

Equations

• Q2Presentation.Induction.edgeEpsRead chief K lam hinv Z B ρ = Q2Presentation.Induction.iotaRead Γ (Q2Presentation.Induction.edgeEps chief K lam hinv Z B ρ)

theorem Q2Presentation.Induction.edgeQForm_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z w : ↥(edgeZ1 chief K B ρ)) : edgeQForm chief K lam hinv Z B ρ (z + w) = edgeQForm chief K lam hinv Z B ρ z + edgeQForm chief K lam hinv Z B ρ w + edgePolarBit chief K lam hinv Z B ρ z w

The quadratic law of Q (token: the three legs are normalized 2-cocycles, the witness is explicit).

theorem Q2Presentation.Induction.edgePolarBit_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (x x' y : ↥(edgeZ1 chief K B ρ)) : edgePolarBit chief K lam hinv Z B ρ (x + x') y = edgePolarBit chief K lam hinv Z B ρ x y + edgePolarBit chief K lam hinv Z B ρ x' y

Polar-bit additivity, first slot.

theorem Q2Presentation.Induction.edgePolarBit_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (x y y' : ↥(edgeZ1 chief K B ρ)) : edgePolarBit chief K lam hinv Z B ρ x (y + y') = edgePolarBit chief K lam hinv Z B ρ x y + edgePolarBit chief K lam hinv Z B ρ x y'

Polar-bit additivity, second slot.

def Q2Presentation.Induction.edgePolarInner {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (x : ↥(edgeZ1 chief K B ρ)) : ↥(edgeZ1 chief K B ρ) →ₗ[ZMod 2] ZMod 2

The polar bit, packaged linearly in the second slot.

Equations

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

theorem Q2Presentation.Induction.edgePolarInner_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (x y : ↥(edgeZ1 chief K B ρ)) : (edgePolarInner chief K lam hinv Z B ρ tok x) y = edgePolarBit chief K lam hinv Z B ρ x y

def Q2Presentation.Induction.edgePolarMap {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) : ↥(edgeZ1 chief K B ρ) →ₗ[ZMod 2] ↥(edgeZ1 chief K B ρ) →ₗ[ZMod 2] ZMod 2

The bilinear polar form of the liftability indicator (additive hom package + ZMod 2-linearity is automatic).

Equations

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

theorem Q2Presentation.Induction.edgePolarMap_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (x y : ↥(edgeZ1 chief K B ρ)) : ((edgePolarMap chief K lam hinv Z B ρ tok) x) y = edgePolarBit chief K lam hinv Z B ρ x y

def Q2Presentation.Induction.edgeQ {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) : Quadratic.QuadF2 ↥(edgeZ1 chief K B ρ)

edgeQ — the P6-engine form at W_ρ = Z¹_ρ(V) (design §2.1, the W2 instantiation): form = ι∘F₀, polar = ι∘P; quadratic law from the completed-square cochain identity plus the token.

Equations

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

theorem Q2Presentation.Induction.edgeQ_form_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z : ↥(edgeZ1 chief K B ρ)) : (edgeQ chief K lam hinv Z B ρ tok).form z = edgeQForm chief K lam hinv Z B ρ z

theorem Q2Presentation.Induction.edgeQ_polar_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (x y : ↥(edgeZ1 chief K B ρ)) : ((edgeQ chief K lam hinv Z B ρ tok).polar x) y = edgePolarBit chief K lam hinv Z B ρ x y

The constraint map L, the linear leg ℓ, and the target κ₀

(linearity from the token; AddMonoidHom.mk' + the ZMod 2 upgrade)

theorem Q2Presentation.Induction.edgeLRead_add_z {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (chi : ↥(XT chief K)) (z w : ↥(edgeZ1 chief K B ρ)) : edgeLRead chief K B ρ (z + w) chi = edgeLRead chief K B ρ z chi + edgeLRead chief K B ρ w chi

theorem Q2Presentation.Induction.edgeLRead_add_chi {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z : ↥(edgeZ1 chief K B ρ)) (chi chi' : ↥(XT chief K)) : edgeLRead chief K B ρ z (chi + chi') = edgeLRead chief K B ρ z chi + edgeLRead chief K B ρ z chi'

theorem Q2Presentation.Induction.edgeEllRead_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z w : ↥(edgeZ1 chief K B ρ)) : edgeEllRead chief K lam hinv Z B ρ (z + w) = edgeEllRead chief K lam hinv Z B ρ z + edgeEllRead chief K lam hinv Z B ρ w

theorem Q2Presentation.Induction.edgeKappaRead_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (chi chi' : ↥(XT chief K)) : edgeKappaRead chief K lam hinv Z B ρ (chi + chi') = edgeKappaRead chief K lam hinv Z B ρ chi + edgeKappaRead chief K lam hinv Z B ρ chi'

def Q2Presentation.Induction.edgeLInner {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z : ↥(edgeZ1 chief K B ρ)) : Module.Dual (ZMod 2) ↥(XT chief K)

The per-z constraint functional (χ ↦ ι(Γ_{γ_χ}(z))) ∈ 𝒳_T^∨.

Equations

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

def Q2Presentation.Induction.edgeL {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) : ↥(edgeZ1 chief K B ρ) →ₗ[ZMod 2] Module.Dual (ZMod 2) ↥(XT chief K)

The constraint map L : W_ρ →ₗ 𝒳_T^∨ (design §4-N7 bullet 4: L z = (χ ↦ ι(χ-pushout defect)), in the coboundary-free graph spelling; edgeLRead_eq_chiDefect aligns it with the ∂-defect).

Equations

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

theorem Q2Presentation.Induction.edgeL_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z : ↥(edgeZ1 chief K B ρ)) (chi : ↥(XT chief K)) : ((edgeL chief K B ρ tok) z) chi = edgeLRead chief K B ρ z chi

def Q2Presentation.Induction.edgeEll {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) : Module.Dual (ZMod 2) ↥(edgeZ1 chief K B ρ)

The linear leg ℓ ∈ W_ρ^∨ (eq:Qkappadifference).

Equations

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

theorem Q2Presentation.Induction.edgeEll_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (z : ↥(edgeZ1 chief K B ρ)) : (edgeEll chief K lam hinv Z B ρ tok) z = edgeEllRead chief K lam hinv Z B ρ z

def Q2Presentation.Induction.edgeKappa {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) : Module.Dual (ZMod 2) ↥(XT chief K)

The constraint target κ₀ ∈ 𝒳_T^∨ (the ρ*e-class read).

Equations

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

theorem Q2Presentation.Induction.edgeKappa_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (chi : ↥(XT chief K)) : (edgeKappa chief K lam hinv Z B ρ tok) chi = edgeKappaRead chief K lam hinv Z B ρ chi

theorem Q2Presentation.Induction.edgePolarBit_edgeA {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (chi : ↥(XT chief K)) (z : ↥(edgeZ1 chief K B ρ)) : edgePolarBit chief K lam hinv Z B ρ (edgeA chief K lam hinv Z B ρ chi) z = edgeLRead chief K B ρ z chi + edgeEllRead chief K lam hinv Z B ρ z

The representing identity hA (design §4-N7 bullet 3, the gammaChi-pairing computation): β(a_χ, z) = L(z)(χ) + ℓ(z).

theorem Q2Presentation.Induction.towerActM_cancel_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (m : towerM K) : ((towerActM K) c⁻¹) (((towerActM K) c) m) = m

Inverse cancellation of the M-level action (the towerActM mirror of headActE_cancel_left).

theorem Q2Presentation.Induction.edgeLRead_eq_chiDefect {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) (z : ↥(edgeZ1 chief K B ρ)) (sec : towerM K ⧸ towerT K → towerM K) (hsec : ∀ (v : towerM K ⧸ towerT K), Submodule.Quotient.mk (sec v) = v) : edgeLRead chief K B ρ z chi = iotaRead Γ fun (γ γ' : ↑Γ.toProfinite.toTop) => (chiTilde chief K chi) (sec (↑z γ) + ((towerActM K) (lowerBar chief K B ρ γ)) (sec (↑z γ')) + sec (↑z (γ * γ')))

The ∂-defect alignment of the constraint reading (design §4-N7 bullet 4, "L z = (χ ↦ ι(χ_*-pushout defect))"): against ANY set-section sec of M ↠ V, the γ_χ-graph reading equals the ι-reading of the χ̃-pushout of the T-valued lifting defect ẑ(γ) + ρ̄γ·ẑ(γ′) + ẑ(γγ′) — the two spellings differ by the explicit continuous coboundary of γ ↦ χ̃(ẑγ) (eq:affineequation's per-χ read; no cohomology carrier).

The deck-reading calculus (order-2 central kernel: descRead is

additive on the deck; every nontrivial deck element is THE element)

theorem Q2Presentation.Induction.descRead_def {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 = if x = 1 then 0 else 1

Classical if-form of descRead (the sGammaZ_def fix-class: cite this, never re-haveI a Decidable instance).

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_of_ne {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} (hx : x ≠ 1) : descRead chief K lam hinv D hW x = 1

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_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) {x y : (descTarget chief K lam hinv D hW).Y} (hx : x ∈ (descKernel chief K lam hinv D hW hne).N) (hy : y ∈ (descKernel chief K lam hinv D hW hne).N) : descRead chief K lam hinv D hW (x * y) = descRead chief K lam hinv D hW x + descRead chief K lam hinv D hW y

Deck-read additivity on the order-2 kernel: descRead (x·y) = descRead x + descRead y for x, y in the deck.

theorem Q2Presentation.Induction.deck_eq_of_read_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) {x y : (descTarget chief K lam hinv D hW).Y} (hx : x ∈ (descKernel chief K lam hinv D hW hne).N) (hy : y ∈ (descKernel chief K lam hinv D hW hne).N) (hread : descRead chief K lam hinv D hW x = descRead chief K lam hinv D hW y) : x = y

Elements of the deck are their own reading's k₀-power: a deck element with reading 0 is 1, and any two nontrivial deck elements coincide (used by the lift-assembly direction).

theorem Q2Presentation.Induction.descTarget_qYMap_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) (x : (descTarget chief K lam hinv D hW).Y) : (descTarget chief K lam hinv D hW).qYMap x = (btChild chief K).fst.qYMap ((descToBt chief K lam hinv D hW hne) x)

The frame factorization of the descended target: the q_Y-data of a descended point is the q_Y-data of its B/T′-collapse (all four decoration legs are quotient lifts computed on mk-chains).

The pinned-lift bridge (design §4-N7 bullet 1: the defect cochain

of the z-twisted lift through descTarget, READ off the pinning)

def Q2Presentation.Induction.pinnedLift {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (γ : ↑Γ.toProfinite.toTop) : (descTarget chief K lam hinv Z.D ⋯).Y

The set-level lift ĝ_z(γ) = ℓ̂(z γ)·σ̂(ρ̄γ) of the z-twisted lift through the descended cover, in pinning coordinates.

Equations

• Q2Presentation.Induction.pinnedLift chief K lam hinv Z B ρ P z γ = P.ellHat (↑z γ) * P.sigmaHat (Q2Presentation.Induction.lowerBar chief K B ρ γ)

theorem Q2Presentation.Induction.pinnedLift_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (γ : ↑Γ.toProfinite.toTop) : pinnedLift chief K lam hinv Z B ρ P z γ = P.ellHat (↑z γ) * P.sigmaHat (lowerBar chief K B ρ γ)

theorem Q2Presentation.Induction.pinnedLift_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) : pinnedLift chief K lam hinv Z B ρ P z 1 = 1

theorem Q2Presentation.Induction.pinnedLift_lc {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) : IsLocallyConstant (pinnedLift chief K lam hinv Z B ρ P z)

theorem Q2Presentation.Induction.descToBt_pinnedLift {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (γ : ↑Γ.toProfinite.toTop) : (descToBt chief K lam hinv Z.D ⋯ ⋯) (pinnedLift chief K lam hinv Z B ρ P z γ) = vInG chief K (↑z γ) * P.s (lowerBar chief K B ρ γ)

theorem Q2Presentation.Induction.edgeDescToBt_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)) (Z : ZeroEdgeDescentData chief K lam hinv) (x : (descTarget chief K lam hinv Z.D ⋯).Y) : (descToBt chief K lam hinv Z.D ⋯ ⋯) x = 1 ↔ x ∈ (descKernel chief K lam hinv Z.D ⋯ ⋯).N

ker descToBt = descKernel (elementwise; the collapse is injective past the deck quotient).

theorem Q2Presentation.Induction.pinnedLift_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)) (Z : ZeroEdgeDescentData chief K lam hinv) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : ∃ k ∈ (descKernel chief K lam hinv Z.D ⋯ ⋯).N, descRead chief K lam hinv Z.D ⋯ k = edgeDefectFull chief K lam hinv Z B ρ z γ γ' ∧ pinnedLift chief K lam hinv Z B ρ P z γ * pinnedLift chief K lam hinv Z B ρ P z γ' = k * pinnedLift chief K lam hinv Z B ρ P z (γ * γ')

The pinned-lift defect computation (the heart of the bridge): ĝ_z(γ)·ĝ_z(γ′) = k·ĝ_z(γγ′) for a deck element k whose reading is EXACTLY the full defect cochain — fib_read + conj_read + sec_read assemble to F₀ + Γ_{γ_κ} + ρ*δ_κ on the nose.

def Q2Presentation.Induction.edgeLiftableDesc {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) : Prop

Desc-liftability of the z-twisted lift — N1's descLiftableWeak shape at the pinned V⋊C-lift γ ↦ vInG(z γ)·s(ρ̄γ) (= btLiftVal (edgeTrivial … P.s … z), edgeTrivial_apply).

Equations

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

theorem Q2Presentation.Induction.edgeLift_frame {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (γ : ↑Γ.toProfinite.toTop) : (btChild chief K).fst.qYMap (vInG chief K (↑z γ) * P.s (lowerBar chief K B ρ γ)) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom B.toBoundary) γ)

The frame value of the pinned V⋊C-lift (the edgeTrivial frame computation, restated).

def Q2Presentation.Induction.descLiftVal {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) {Γ : ProfiniteGrp.{0}} (dt : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (descTarget chief K lam hinv Z.D ⋯).Y)) (γ : ↑Γ.toProfinite.toTop) : (descTarget chief K lam hinv Z.D ⋯).Y

Raw-carrier readout of a descended lift (the banked btLiftVal fix-class: only a def with the raw-typed signature keeps HMul homogeneous across the wrapped×raw boundary — ascriptions do not survive to instance search).

Equations

• Q2Presentation.Induction.descLiftVal chief K lam hinv Z dt γ = (ProfiniteGrp.Hom.hom dt) γ

theorem Q2Presentation.Induction.edgeLiftableDesc_iff_solvable {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) : edgeLiftableDesc chief K lam hinv Z B ρ P z ↔ CochainSolvable Γ (edgeDefectFull chief K lam hinv Z B ρ z)

The bridge (design §4-N7 bullet 1, exit): the z-twisted lift descends through descTarget iff its full defect 2-cocycle equation is continuously solvable — prop:phaseidentity's carrier statement, dissolved into the normalized-cochain calculus.

Instances for the engine carrier (statement-level: the

Module.evalEquiv reindex and the dual-dual sum need them at elaboration time)

instance Q2Presentation.Induction.instModuleFiniteXTPointwise {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Module.Finite (ZMod 2) ↥(XT chief K)

instance Q2Presentation.Induction.instFiniteDualXTPointwise {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Finite (Module.Dual (ZMod 2) ↥(XT chief K))

noncomputable instance Q2Presentation.Induction.instFintypeDualDualXTPointwise {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Fintype (Module.Dual (ZMod 2) (Module.Dual (ZMod 2) ↥(XT chief K)))

Equations

• Q2Presentation.Induction.instFintypeDualDualXTPointwise chief K = Fintype.ofFinite (Module.Dual (ZMod 2) (Module.Dual (ZMod 2) ↥(Q2Presentation.Induction.XT chief K)))

theorem Q2Presentation.Induction.iotaSign_eq_signChar {Γ : ProfiniteGrp.{0}} (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : iotaSign Γ F = Quadratic.Dickson.signChar (iotaRead Γ F)

±1-indicator through the bit: iotaSign = signChar ∘ iotaRead (the engine's phase carrier alignment).

theorem Q2Presentation.Induction.edgeLiftableDesc_iff_form {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) : edgeLiftableDesc chief K lam hinv Z B ρ P z ↔ edgeQForm chief K lam hinv Z B ρ z + edgeEllRead chief K lam hinv Z B ρ z = edgeEpsRead chief K lam hinv Z B ρ

The constrained-count alignment: the z-twisted lift descends iff Q(z) + ℓ(z) = ε₀ — eq:Qkappadifference dissolved (the constant is absorbed into the ε-slot, exactly as the engine consumes it).

The ∂-surjectivity floor (design §5 F-∂; the riskiest N7

sub-lemma, delivered as the design's fallback)

def Q2Presentation.Induction.EdgeDelSurj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Prop

F-∂ floor Prop (design §5 #F-∂; lem:elementarystage l.4171–4205, dual-injectivity spelling): no 0 ≠ χ ∈ 𝒳_T kills every constraint defect reading — i.e. the transpose of ∂_{Γ,ρ} is injective. PROVENANCE + dissolution program: the manuscript proof is the counting dévissage H²_{Γ,ρ}(M) = 0 at the intermediate χ-pushout kernels M_χ = ker χ̃; in-tree this is the clause-(d) ladder (q2_localduality_weakZ1_card) at M_χ-kernels for the LOCAL source — derivable, expected NOT to survive — and the N6 corank engine for the candidate (manuscript fallback per the §5 table). Consumed as a HYPOTHESIS (never an axiom) by the engine fire below; edgeL_surjective_of_delSurj converts it to the engine's hL.

Equations

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

theorem Q2Presentation.Induction.edgeL_surjective_of_delSurj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (hdel : EdgeDelSurj chief K B ρ) : Function.Surjective ⇑(edgeL chief K B ρ tok)

The floor discharges the engine's surjectivity hypothesis (finite 𝔽₂-duality: a proper range is killed by a nonzero functional, which the double-dual reindex reads as a nonzero χ).

The engine fire and the phase bridge (design §4-N7 bullet 5)

theorem Q2Presentation.Induction.edgeConstrainedGauss {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) [Fintype ↥(edgeZ1 chief K B ρ)] (hL : Function.Surjective ⇑(edgeL chief K B ρ tok)) (κ : Module.Dual (ZMod 2) ↥(XT chief K)) (ε : ZMod 2) : 2 * ↑(Nat.card (Module.Dual (ZMod 2) ↥(XT chief K))) * ↑(Quadratic.constrainedZeros (edgeL chief K B ρ tok) (edgeQ chief K lam hinv Z B ρ tok) (edgeEll chief K lam hinv Z B ρ tok) κ ε) = ↑(Nat.card ↥(edgeZ1 chief K B ρ)) + Quadratic.Dickson.gaussSum (edgeQ chief K lam hinv Z B ρ tok) * ∑ ψ : Module.Dual (ZMod 2) (Module.Dual (ZMod 2) ↥(XT chief K)), Quadratic.Dickson.signChar (ψ κ + ε + (edgeQ chief K lam hinv Z B ρ tok).form (edgeA chief K lam hinv Z B ρ ((Module.evalEquiv (ZMod 2) ↥(XT chief K)).symm ψ)))

The P6 engine, fired at W_ρ (constrainedGauss_count instantiated; eq:pointwiseconstrained l.4332–4340 at the cocycle-level carrier, κ/ε free).

theorem Q2Presentation.Induction.edgePhaseBridge {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) (chi : ↥(XT chief K)) : Quadratic.Dickson.signChar (((Module.evalEquiv (ZMod 2) ↥(XT chief K)) chi) (edgeKappa chief K lam hinv Z B ρ tok) + edgeEpsRead chief K lam hinv Z B ρ + (edgeQ chief K lam hinv Z B ρ tok).form (edgeA chief K lam hinv Z B ρ chi)) = iotaSign Γ (pullCochain (cChild chief K).fst (Delta chief K lam hinv Z chi) B (cChild chief K).snd ρ)

The phase bridge (prop:phaseidentity l.4108–4146, dissolved): per χ ∈ 𝒳_T, the engine's phase at the pulled representing vector EQUALS the ±1-indicator of ρ*(Δ_{χ,κ}) — Δ's three legs are the κ₀/ε₀/Q(a_χ)-reads on the nose (δ_κ enters exactly once, the P6 §7.6 discipline, because Delta already contains it once).

theorem Q2Presentation.Induction.edgePointwise_count {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) [Fintype ↥(edgeZ1 chief K B ρ)] (P : ZeroEdgePinning chief K lam hinv Z) (hdel : EdgeDelSurj chief K B ρ) : 2 * 2 ^ rT chief K * ↑(Nat.card { z : ↥(edgeZ1 chief K B ρ) // (edgeL chief K B ρ tok) z = edgeKappa chief K lam hinv Z B ρ tok ∧ edgeLiftableDesc chief K lam hinv Z B ρ P z }) = ↑(Nat.card ↥(edgeZ1 chief K B ρ)) + Quadratic.Dickson.gaussSum (edgeQ chief K lam hinv Z B ρ tok) * ∑ chi : ↥(XT chief K), iotaSign Γ (pullCochain (cChild chief K).fst (Delta chief K lam hinv Z chi) B (cChild chief K).snd ρ)

The R4b pointwise identity, engine form (design §4-N7 output, per (ρ, source-token) at a pinned Z; the design's 2^{rT+1}·#{…} = |W_ρ| + G(Q_ρ)·Σ_χ ind_ρ(Δ_{χ,κ})):

2·2^{r_T}·#{z ∈ Z¹_ρ(V) : L z = κ₀ ∧ z-lift descends}
  = |Z¹_ρ(V)| + G(Q_ρ)·∑_{χ∈𝒳_T} ι±(ρ*(Δ_{χ,κ}))

The count is over the CONSTRAINED desc-liftable twisted cocycles; the f-level Zcount-fibre absorption (T′-stage torsor, |W_ρ| = 2^{2d} numerics) is the recorded N5/N6/N9 assembly, not asserted here.

The radical layer (design §4-N7 bullet 3 → §4-N8 consumption):

B¹_ρ(V) annihilates edgeQ, and the Gauss sum fibres by 2^{dim V}. F1 + audit-§A: the descended Gauss type stays OPAQUE — no ram pin, no sign tie, no gaussType (edgeHeadForm …) identification (the §5 sign floors own constancy/value).

def Q2Presentation.Induction.edgeCobound {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (v : towerM K ⧸ towerT K) : ↥(edgeZ1 chief K B ρ)

The twisted coboundary cocycle w_v(γ) = v + ρ̄γ·v.

Equations

• Q2Presentation.Induction.edgeCobound chief K B ρ v = ⟨fun (γ : ↑Γ.toProfinite.toTop) => v + (Q2Presentation.Induction.headActE chief K (Q2Presentation.Induction.lowerBar chief K B ρ γ)) v, ⋯⟩

theorem Q2Presentation.Induction.edgeCobound_val {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (v : towerM K ⧸ towerT K) (γ : ↑Γ.toProfinite.toTop) : ↑(edgeCobound chief K B ρ v) γ = v + (headActE chief K (lowerBar chief K B ρ γ)) v

theorem Q2Presentation.Induction.edgeCobound_add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (v w : towerM K ⧸ towerT K) : edgeCobound chief K B ρ (v + w) = edgeCobound chief K B ρ v + edgeCobound chief K B ρ w

def Q2Presentation.Induction.edgeCoboundMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : towerM K ⧸ towerT K →ₗ[ZMod 2] ↥(edgeZ1 chief K B ρ)

B¹-inclusion as a linear map V →ₗ W_ρ.

Equations

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

theorem Q2Presentation.Induction.edgeCoboundMap_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (v : towerM K ⧸ towerT K) : (edgeCoboundMap chief K B ρ) v = edgeCobound chief K B ρ v

def Q2Presentation.Induction.edgeB1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Submodule (ZMod 2) ↥(edgeZ1 chief K B ρ)

The coboundary submodule B¹_ρ(V) ≤ W_ρ.

Equations

• Q2Presentation.Induction.edgeB1 chief K B ρ = (Q2Presentation.Induction.edgeCoboundMap chief K B ρ).range

theorem Q2Presentation.Induction.edgeCoboundMap_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Function.Injective ⇑(edgeCoboundMap chief K B ρ)

v ↦ w_v is injective: the head has no C-fixed vectors (headInv_eq_zero, N5's target-side V^C = 0; ρ̄ is onto C).

theorem Q2Presentation.Induction.edgeF0_edgeCobound {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (v : towerM K ⧸ towerT K) : edgeF0 chief K lam hinv Z B ρ (edgeCobound chief K B ρ v) = cochainCoboundary Γ fun (γ : ↑Γ.toProfinite.toTop) => Z.mC (lowerBar chief K B ρ γ) v + ((edgeBaseFactor chief K lam hinv ⋯) v) ((headActE chief K (lowerBar chief K B ρ γ)) v) + (edgeHeadForm chief K lam hinv ⋯).form v

F₀ at a coboundary cocycle is an explicit continuous coboundary (the completed-square residue collapses).

theorem Q2Presentation.Induction.edgePair_edgeCobound_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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (v : towerM K ⧸ towerT K) (z : ↥(edgeZ1 chief K B ρ)) : edgePair chief K lam hinv Z B ρ (edgeCobound chief K B ρ v) z = cochainCoboundary Γ fun (γ : ↑Γ.toProfinite.toTop) => ((edgeHeadForm chief K lam hinv ⋯).polar (↑z γ)) ((headActE chief K (lowerBar chief K B ρ γ)) v)

Pairing a coboundary cocycle (first slot) is an explicit continuous coboundary.

theorem Q2Presentation.Induction.edgeQ_annihilates_coboundaries {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) : Annihilates (edgeQ chief K lam hinv Z B ρ tok) (edgeB1 chief K B ρ)

B¹ annihilates edgeQ (form and polar both vanish on coboundaries — the "polar radical ⊇ coboundary part" half; the converse inclusion is per-source duality, owned by the N5-extension/N6 ladder, NOT asserted here).

theorem Q2Presentation.Induction.edgeB1_finrank {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Module.finrank (ZMod 2) ↥(edgeB1 chief K B ρ) = dimV chief K

theorem Q2Presentation.Induction.edgeGaussSum_factor {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) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) [Fintype ↥(edgeZ1 chief K B ρ)] : Quadratic.Dickson.gaussSum (edgeQ chief K lam hinv Z B ρ tok) = 2 ^ dimV chief K * Quadratic.Dickson.gaussSum ⋯.descend

The Gauss-sum fibration factor (§4-N8 consumption): G(Q_ρ) = 2^{dim V}·G(Q̄_ρ) — the B¹(V)-part of eq:mumultiplicity fused into the engine's |W|-term. gaussType of the descended form is LEFT FREE (F1 discipline).

The LOCAL instantiation (design §6.1: the source-token slot

discharged by N3's citable q2_trivialCoeff_h2_line; the CANDIDATE slot stays the abstract IotaToken-hypothesis of the generic layer — N4 plugs in without touching this file)

theorem Q2Presentation.Induction.q2_edgePointwise_count {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) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (hdel : EdgeDelSurj chief K B ρ) : 2 * 2 ^ rT chief K * ↑(Nat.card { z : ↥(edgeZ1 chief K B ρ) // (edgeL chief K B ρ ⋯) z = edgeKappa chief K lam hinv Z B ρ ⋯ ∧ edgeLiftableDesc chief K lam hinv Z B ρ P z }) = ↑(Nat.card ↥(edgeZ1 chief K B ρ)) + Quadratic.Dickson.gaussSum (edgeQ chief K lam hinv Z B ρ ⋯) * ∑ chi : ↥(XT chief K), iotaSign GQ2Profinite (pullCochain (cChild chief K).fst (Delta chief K lam hinv Z chi) B (cChild chief K).snd ρ)

q2_zeroEdgePointwise — the R4b pointwise identity at the LOCAL source (prop:zeroedge clauses S3–S5 at G_ℚ₂, engine form): the ι-token is the placed citable q2_trivialCoeff_h2_line (NSW (7.1.8)(ii)

• (7.2.6), audit §H); only the F-∂ floor remains hypothesis-shaped.

theorem Q2Presentation.Induction.q2_edgeGaussSum_factor {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) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Quadratic.Dickson.gaussSum (edgeQ chief K lam hinv Z B ρ ⋯) = 2 ^ dimV chief K * Quadratic.Dickson.gaussSum ⋯.descend

The local Gauss-factor specialization (type still opaque — F1).