@[reducible, inline]

abbrev Q2Presentation.Induction.XRZero.NR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup p.fst.Y

The Frattini layer as the quotient kernel.

Equations

• Q2Presentation.Induction.XRZero.NR chief K = Q2Presentation.Induction.kernelFrattini K

instance Q2Presentation.Induction.XRZero.instNormalYFstBoundaryFramedTargetBoundaryFrameNR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (NR chief K).Normal

theorem Q2Presentation.Induction.XRZero.NR_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : NR chief K ≤ p.fst.LY

theorem Q2Presentation.Induction.XRZero.NR_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (n : p.fst.Y) : n ∈ NR chief K → p.fst.thetaY n = 1

theorem Q2Presentation.Induction.XRZero.NR_nongenerating {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : Subgroup p.fst.Y) (hJ : Subgroup.map (QuotientGroup.mk' (NR chief K)) J = ⊤) : J = ⊤

Frattini non-generation at the kernel layer.

The child and its measure decrease

def Q2Presentation.Induction.XRZero.xrChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : FramedPair

The 𝒳_R = 0 child: the quotient framed pair at N = Φ-layer.

Equations

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

theorem Q2Presentation.Induction.XRZero.xrChild_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) : framedMeasure (xrChild chief K) < framedMeasure p

Strict measure decrease (the Frattini layer is nontrivial).

The cochain keep and the count assembly

theorem Q2Presentation.Induction.XRZero.sec7_xrzero_cochainData {p : FramedPair} (h : ¬ScalarTerminal p) (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) (hchar : ¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R), lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C), lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam) : ∃ (kdim : ℕ), (∀ (g : boundaryFramedSurj boundaryPackage_GammaA (xrChild chief K).fst (xrChild chief K).snd), Nonempty (TorsorProgram.liftHom p.fst (NR chief K) ⋯ ⋯ boundaryPackage_GammaA p.snd g)) ∧ (∀ (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (NR chief K) ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (NR chief K) ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst (NR chief K) ⋯ ⋯ boundaryPackage_GammaA p.snd g), Nat.card (TorsorProgram.Z1 p.fst (NR chief K) ⋯ ⋯ boundaryPackage_GammaA p.snd g f₀) = 2 ^ (2 * kdim)) ∧ (∀ (g : boundaryFramedSurj boundaryPackage_GQ2 (xrChild chief K).fst (xrChild chief K).snd), Nonempty (TorsorProgram.liftHom p.fst (NR chief K) ⋯ ⋯ boundaryPackage_GQ2 p.snd g)) ∧ ∀ (g : boundaryFramedSurj boundaryPackage_GQ2 (TorsorProgram.quotientFramedTarget p.fst (NR chief K) ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (NR chief K) ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst (NR chief K) ⋯ ⋯ boundaryPackage_GQ2 p.snd g), Nat.card (TorsorProgram.Z1 p.fst (NR chief K) ⋯ ⋯ boundaryPackage_GQ2 p.snd g f₀) = 2 ^ (2 * kdim)

The 𝒳_R = 0 cochain statement, PROVEN (lem:affinelifting + eq:mumultiplicity + lem:obstructionseparation at |𝒳_R| = 1; manuscript l.4207-4262). Per source: every child-framed surjection admits a framed lift (the complete obstruction is detected by invariant characters, of which there are none), and the twisted cocycle set has the common size 2^{2·dim R}. Derived from the sharp XR-layer keep and the canonical local-duality keep via the elementary-kernel assembly (XRLayerKeep).

theorem Q2Presentation.Induction.XRZero.source_count {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [hfinP : Finite (boundaryFramedSurj B p.fst p.snd)] [hfinC : Finite (boundaryFramedSurj B (xrChild chief K).fst (xrChild chief K).snd)] (m : ℕ) (hne : ∀ (g : boundaryFramedSurj B (xrChild chief K).fst (xrChild chief K).snd), Nonempty (TorsorProgram.liftHom p.fst (NR chief K) ⋯ ⋯ B p.snd g)) (hcnt : ∀ (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget p.fst (NR chief K) ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (NR chief K) ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst (NR chief K) ⋯ ⋯ B p.snd g), Nat.card (TorsorProgram.Z1 p.fst (NR chief K) ⋯ ⋯ B p.snd g f₀) = m) : Nat.card (boundaryFramedSurj B p.fst p.snd) = m * Nat.card (boundaryFramedSurj B (xrChild chief K).fst (xrChild chief K).snd)

Per-source torsor count over the fibration engine.

The packet, proven; the branch, rewired

theorem Q2Presentation.Induction.XRZero.sec7_xrzero_liftTorsorChild_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) (hchar : ¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R), lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C), lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam) : ∃ (child : FramedPair) (k : ℕ) (nA : ℕ) (nQ : ℕ), framedMeasure child < framedMeasure p ∧ framedCountA child = ↑nA ∧ framedCountQ child = ↑nQ ∧ framedCountA p = ↑(2 ^ (2 * k) * nA) ∧ framedCountQ p = ↑(2 ^ (2 * k) * nQ)

The former sec7_xrzero_liftTorsorChild packet, PROVEN.

theorem Q2Presentation.Induction.XRZero.sec7_fourierBranch_of_XRzero_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) (hchar : ¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R), lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C), lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam) : Nonempty (FourierBranchData p)

The 𝒳_R = 0 Fourier branch, over the PROVEN packet (clone of the checkpoint-XR0 assembly).

theorem Q2Presentation.Induction.XRZero.sec7_fourierBranch_of_frattiniNontrivial_decomposed' {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) : Nonempty (FourierBranchData p)

The decomposed R ≠ 1 branch over the proven 𝒳_R = 0 side.