W7b(a): the phase-cover pair, its deck kernel, and n_{Γ,0}(ζ)

noncomputable def Q2Presentation.Induction.phaseCoverPair {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : FramedPair

The phase-cover framed pair C_ζ (lem:phasecover's carrier, l.4376–4378): the normalized-cocycle central double cover of the C-child, with the pulled-back boundary framing of lem:covertransform (l.3822–3830). Built by W7a (Lifting/CocycleCover.lean); P3-U8's phaseCoverPair sketch resolves to this definition (P7 owns the carrier, U8 imports it — the §2.5/§7 coordination note of the P7 design).

Equations

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

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.phaseKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Lifting.ElementaryKernel (phaseCoverPair chief K zeta hz1 hz2 hzc).fst

The deck kernel of the phase cover, as an order-2 elementary kernel (the phaseKernel of P3 §4.7).

Equations

• Q2Presentation.Induction.phaseKernel chief K zeta hz1 hz2 hzc = Q2Presentation.Lifting.cocycleKernel (Q2Presentation.Induction.cChild chief K).fst zeta hz1 hz2 hzc

theorem Q2Presentation.Induction.phaseCoverPair_measure {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : framedMeasure (phaseCoverPair chief K zeta hz1 hz2 hzc) = 2 * framedMeasure (cChild chief K)

eq:phasecoverdescent, equality half (l.4411–4413): |L_{C_ζ}| = 2·|L_C|.

noncomputable def Q2Presentation.Induction.phaseCount {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : ℕ

n_{Γ,0}(ζ) (l.4377–4379): the number of lower exact-image maps ρ ∈ X_Γ(C) for which the phase cover is unobstructed, i.e. which admit a weak (no image condition) framed lift through p_ζ. The child transport of P3-§4.7's phaseChildTransport slot is W7a's cocycleChildEquiv, absorbed into cocycleCoverLiftHom.

Equations

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

W7b(b): the exact-image strata of the phase cover

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.phaseCoverStrata {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Type

The exact-image strata of the phase cover — the manuscript sum index {J̃ ≤ C_ζ : p_ζ(J̃) = C} (l.4386–4389), as P2's generic coverStrata (the top stratum J̃ = ⊤ included, manuscript-faithfully).

Equations

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

noncomputable def Q2Presentation.Induction.phaseStratumPair {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (J : phaseCoverStrata chief K zeta hz1 hz2 hzc) : FramedPair

The stratum framed pair (J̃, J̃ ∩ L̃, π̃|_J̃, θ̃|_J̃; same frame) — an ordinary exact-image object in the same global boundary-framed category (l.3841–3843; mirror of scalarCoverStratumPair).

Equations

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

W7b(c): the exit theorems (eq:phasecovertransform, per source)

theorem Q2Presentation.Induction.sec7_phaseCoverPartition_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : 8 * phaseCount chief K zeta hz1 hz2 hzc boundaryPackage_GammaA = ∑ J : phaseCoverStrata chief K zeta hz1 hz2 hzc, Nat.card (boundaryFramedSurj boundaryPackage_GammaA (phaseStratumPair chief K zeta hz1 hz2 hzc J).fst (phaseStratumPair chief K zeta hz1 hz2 hzc J).snd)

lem:phasecover eq:phasecovertransform (l.4384–4390), candidate source: the exact eight-lift partition of lem:covertransform applied to p_ζ at the FULL lower target (manuscript proof l.4395–4396) — a literal partition, no equidistribution assumption (l.3853–3856), hR-free and division-free.

theorem Q2Presentation.Induction.sec7_phaseCoverPartition_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : 8 * phaseCount chief K zeta hz1 hz2 hzc boundaryPackage_GQ2 = ∑ J : phaseCoverStrata chief K zeta hz1 hz2 hzc, Nat.card (boundaryFramedSurj boundaryPackage_GQ2 (phaseStratumPair chief K zeta hz1 hz2 hzc J).fst (phaseStratumPair chief K zeta hz1 hz2 hzc J).snd)

lem:phasecover eq:phasecovertransform (l.4384–4390), local source: mirror of sec7_phaseCoverPartition_gammaA for G_{ℚ₂}; the uniform 8 is cover_Z1_card_gq2, derived from the EXISTING citable q2_localduality_general count clause (NSW VII.2–3 Euler–Poincaré — provenance note of CoverEightLocal); no keep is touched.

W7c: the signed sum s_Γ(ζ) and eq:recursionR5a

noncomputable def Q2Presentation.Induction.sGammaZ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [Finite (boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd)] : ℤ

s_Γ(ζ) (l.4350–4355): the signed sum over the exact-image lower maps, with the sign BY DEFINITION the splitting indicator of the phase cover (l.4371–4374: "its splitting indicator realizes the sign"). The identification of this indicator with the quadratic phase signChar (χκ + ε + Q⁰(Aχ)) of the P6 engine is prop:phaseidentity and is deliberately NOT asserted here (P6 §3 contract; P8's obligation). The Finite instance is a hypothesis so the ambient sum is well-posed; both sources supply it (centralCover_candidateBoundaryFramedSurj_finite, sec7_localBoundaryFramedSurj_finite).

Equations

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

theorem Q2Presentation.Induction.sGammaZ_def {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [Finite (boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd)] : sGammaZ chief K zeta hz1 hz2 hzc B = ∑ g : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd, if Nonempty (Lifting.cocycleCoverLiftHom (cChild chief K).fst zeta hz1 hz2 hzc B (cChild chief K).snd g) then 1 else -1

Unfolding lemma for sGammaZ (single-def rfl application lemma, banked fix-class): both sides elaborate the term-mode haveI-inlined sum with the def's own classical ite instances, so downstream rewrites are syntactic on a constant-headed LHS (a tactic-mode haveI would be an OPAQUE fvar and break the defeq).

theorem Q2Presentation.Induction.phaseCount_le_eC {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [Finite (boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd)] : phaseCount chief K zeta hz1 hz2 hzc B ≤ eC chief K B

Trivial bound feeding P8's ℕ-rearrangements (P3 §7's note): n_{Γ,0}(ζ) ≤ e_Γ(C).

theorem Q2Presentation.Induction.sGammaZ_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [Finite (boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd)] : sGammaZ chief K zeta hz1 hz2 hzc B = 2 * ↑(phaseCount chief K zeta hz1 hz2 hzc B) - ↑(eC chief K B)

eq:recursionR5a (l.4380–4382): s_Γ(ζ) = 2·n_{Γ,0}(ζ) − e_Γ(C) — the decomposition of the signed sum by the two indicator values (manuscript proof l.4394–4395). Division-free and ℤ-valued (no ℕ-subtraction); phaseCount_le_eC supplies P8's nonneg spelling.

W7d: the measure chain (eq:phasecoverdescent + |K| ≥ 4)

def Q2Presentation.Induction.cChildLYProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↥(XRZero.xrChild chief K).fst.LY →* (XRZero.xrChild chief K).fst.Y ⧸ mChild chief K

The marked-kernel comparison hom L_B →* B ⧸ M' (the xrChildLYProj idiom one level down).

Equations

• Q2Presentation.Induction.cChildLYProj chief K = (QuotientGroup.mk' (Q2Presentation.Induction.mChild chief K)).comp (Q2Presentation.Induction.XRZero.xrChild chief K).fst.LY.subtype

theorem Q2Presentation.Induction.cChild_measure_factor {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : framedMeasure (XRZero.xrChild chief K) = Nat.card ↥(mChild chief K) * framedMeasure (cChild chief K)

The C-child measure factorization m_B = |M'| · m_C (first- isomorphism count for cChildLYProj, mirror of xrChild_measure_factor, ScalarCoverChildren.lean:79–113).

theorem Q2Presentation.Induction.two_le_card_mChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : 2 ≤ Nat.card ↥(mChild chief K)

2 ≤ |M'| — the in-tree half of the manuscript's |K| ≥ 4 (l.4422–4424): the non-scalar head is nontrivial, unconditionally (mChild_ne_bot); the other factor of 2 is |Φ(K)| > 1 (hR).

theorem Q2Presentation.Induction.phaseStratumPair_measure_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (J : phaseCoverStrata chief K zeta hz1 hz2 hzc) : framedMeasure (phaseStratumPair chief K zeta hz1 hz2 hzc J) ≤ 2 * framedMeasure (cChild chief K)

Stratum measure bound: |J̃ ∩ L̃| ≤ 2·|L_C| — eq:phasecoverdescent in its consumption shape (generic stratum bound + order-2 deck kernel + cover-child/base marked-kernel identification).

theorem Q2Presentation.Induction.phaseStratumPair_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (hR : 1 < Nat.card ↥(kernelFrattini K)) (J : phaseCoverStrata chief K zeta hz1 hz2 hzc) : framedMeasure (phaseStratumPair chief K zeta hz1 hz2 hzc J) < framedMeasure p

Strict decrease below the PARENT (lem:strictdecrease eq:phasecoverdescent l.4411–4414 + l.4422–4424, in-tree chain ≤ 2·m_C ≤ |M'|·m_C = m_B < P): every phase-cover stratum — including the top stratum J̃ = ⊤ — is a strictly smaller induction target. hR (implied by P8's hcard) enters only here.

W7e: list forms for P8 (ScalarCoverChildren mirror)

noncomputable def Q2Presentation.Induction.phaseStrataChildren {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : List FramedPair

The phase-cover strata as a children list (canonical Finset.univ enumeration through the GLOBAL Fintype (coverStrata …) instance, CoverLiftPartition.lean:54 — the same instance the exit sums elaborate against).

Equations

• Q2Presentation.Induction.phaseStrataChildren chief K zeta hz1 hz2 hzc = List.map (Q2Presentation.Induction.phaseStratumPair chief K zeta hz1 hz2 hzc) Finset.univ.toList

theorem Q2Presentation.Induction.phaseStrataChildren_sum_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : 8 * phaseCount chief K zeta hz1 hz2 hzc boundaryPackage_GammaA = (List.map (⇑Cardinal.toNat ∘ framedCountA) (phaseStrataChildren chief K zeta hz1 hz2 hzc)).sum

sec7_phaseCoverPartition_gammaA in list form: the candidate block sum is 8·n_{A,0}(ζ).

theorem Q2Presentation.Induction.phaseStrataChildren_sum_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : 8 * phaseCount chief K zeta hz1 hz2 hzc boundaryPackage_GQ2 = (List.map (⇑Cardinal.toNat ∘ framedCountQ) (phaseStrataChildren chief K zeta hz1 hz2 hzc)).sum

sec7_phaseCoverPartition_gq2 in list form: the local block sum is 8·n_{Q,0}(ζ).

theorem Q2Presentation.Induction.phaseStrataChildren_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (zeta : (cChild chief K).fst.Y → (cChild chief K).fst.Y → ZMod 2) (hz1 : ∀ (y : (cChild chief K).fst.Y), zeta 1 y = 0) (hz2 : ∀ (y : (cChild chief K).fst.Y), zeta y 1 = 0) (hzc : ∀ (a b c : (cChild chief K).fst.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (hR : 1 < Nat.card ↥(kernelFrattini K)) (c : FramedPair) : c ∈ phaseStrataChildren chief K zeta hz1 hz2 hzc → framedMeasure c < framedMeasure p

Every member of a phase-strata block is strictly smaller than the parent at hR — the per-child small-witness for P8's children list (branch-free: no 4 ≤ |Φ(K)| needed, unlike the scalar-cover blocks).