Decomposition of the corrected R ≠ 1 branch

This file decomposes the coarse manuscript-true packet sec7_fourierBranch_of_frattiniNontrivial into:

• Sec7RawTowerPacket — the raw §7 tower over the ⊆-minimal kernel: the finite 𝔽₂ modules R, M, T, the lower group C, the actions, head nontriviality, dual-invariant vanishing (lem:simplehead), and the literal K/Φ(K) ≃ M bridge. Its existence for a first chief factor with Φ(K) ≠ 1 is the residual sec7_rawTowerPacket_exists (manuscript: lem:simplehead + lem:collapse, both proved there for a first chief factor — the coprime step uses below_scalar).
• the 𝒳_R ≠ 0 sub-branch — proved: build the MinimalBlock and the concrete target-subgroup packet from the raw tower and drive the (B, Dsub)-parameterized §8 engine (fourierBranch_of_blockConcrete);
• the 𝒳_R = 0 sub-branch — residual sec7_fourierBranch_of_XRzero (manuscript: prop:finalfourier degenerates to e_Γ(Y) = z_R·e_Γ(B); no scalar pushouts, no nonzero determinant character — the case the old interface wrongly excluded).

Together they give sec7_fourierBranch_of_frattiniNontrivial_decomposed, replacing the coarse packet in the corrected route.

The raw §7 tower packet over the corrected kernel

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

The raw §7 tower over the ⊆-minimal kernel: lem:simplehead data (modules, actions, head, dual vanishing) plus the literal K/Φ(K) ≃ M provenance. No determinant character is carried — 𝒳_R = 0 is legal (prop:finalfourier needs only R ≠ 1).

• rawModuleData : MinimalBlockRawModuleData p chief.toNonScalarChiefFactor
• rawActionData : MinimalBlockRawActionData self.rawModuleData
• headNontrivialData : MinimalBlockHeadNontrivialData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)
• dualInvariantData : MinimalBlockDualInvariantVanishesData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)
• KmodR_equiv_rawM : ↥(Subgroup.map (QuotientGroup.mk' (kernelFrattini K)) K.Ksub) ≃* Multiplicative self.rawModuleData.M

theorem Q2Presentation.Induction.sec7_rawTowerPacket_exists {p : FramedPair} (_h : ¬ScalarTerminal p) (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (_hR : 1 < Nat.card ↥(kernelFrattini K)) : Nonempty (Sec7RawTowerPacket chief K)

The corrected raw §7 tower packet exists for a first non-scalar chief factor and a ⊆-minimal kernel with nontrivial Frattini layer.

All fields are now the concrete ones constructed over K: the raw modules/actions from Section7RawTowerAssembly, and the literal quotient-image bridge from Section7RawTowerBridge.

def Q2Presentation.Induction.Sec7RawTowerPacket.rawTowerData {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (T : Sec7RawTowerPacket chief K) : MinimalBlockRawTowerData p chief.toNonScalarChiefFactor

The raw tower assembled from the packet.

Equations

• T.rawTowerData = Q2Presentation.Induction.MinimalBlockRawTowerData.ofModuleAction T.rawModuleData T.rawActionData

def Q2Presentation.Induction.Sec7RawTowerPacket.preheadTowerData {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (T : Sec7RawTowerPacket chief K) : MinimalBlockPreheadTowerData p chief.toNonScalarChiefFactor

The pre-head tower assembled from the packet.

Equations

• T.preheadTowerData = Q2Presentation.Induction.MinimalBlockPreheadTowerData.ofRaw T.rawTowerData ⋯

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

The canonical raw tower packet — the literal §7 constructors (checkpoint-F9). Using this definitional packet (instead of an opaque Nonempty-obtained one) lets the crux-lowered pushout packet of Section7PushoutConstruction be consumed directly.

Equations

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

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPushoutDataOfRawTower {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (T : Sec7RawTowerPacket chief K) : Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData T.preheadTowerData)

checkpoint-F8: group-backed §6 pushout residual. The generic-D form minimalBlock_preheadActualCentralExtensionPushoutData is falsifiable at abstract prehead towers: an invariant character on R (e.g. trivial C-action on R = F₂) together with a non-self-dual simple head and T = 0 makes its radical clause force an equivariant self-duality M ≃ M^∨ that need not exist — instance #14 of the over-strong residual shape documented in PROGRESS.md. The manuscript constructs the packet from the ACTUAL kernel group K of the raw §7 tower (prop:simpleheaddet: scalar central pushouts K_λ = K/ker λ, their squaring maps and commutator pairings), so the honest residual is stated over the raw tower packet, which carries K.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantPackets_ofRawTower {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (T : Sec7RawTowerPacket chief K) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData T.preheadTowerData), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

Determinant packets over the raw tower, from the group-backed pushout residual (replicates minimalBlock_preheadDeterminantPackets_from_finalClosers at D := T.preheadTowerData without consuming the generic-D axiom).

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantPackets_ofCruxCanonical {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

checkpoint-F9: determinant packets over the CANONICAL raw tower, from the crux-lowered pushout packet (sec7_pushoutPacket) — the mechanism layer of prop:simpleheaddet is theorem-level in Section7PushoutConstruction; only the crux bundle (sec7_pushoutCruxData) remains residual.

The 𝒳_R ≠ 0 sub-branch (proved down to the granular §8 atoms)

axiom Q2Presentation.Induction.centralCover_blockRealizationPacket {p : FramedPair} (h : ¬ScalarTerminal p) (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) : Nonempty ((L : CentralCoverLiftTorsorData (minimalBlock_of_preheadRefinedData h chief.toNonScalarChiefFactor (sec7RawTowerPacketCanonical chief K).preheadTowerData X Fdet A Rdet N)) ×' (C : CentralCoverChildrenData (minimalBlock_of_preheadRefinedData h chief.toNonScalarChiefFactor (sec7RawTowerPacketCanonical chief K).preheadTowerData X Fdet A Rdet N)) ×' CentralCoverLocalPartialFormulaRealization (minimalBlock_of_preheadRefinedData h chief.toNonScalarChiefFactor (sec7RawTowerPacketCanonical chief K).preheadTowerData X Fdet A Rdet N) L C (centralCover_candidateCountingPartialFormula (minimalBlock_of_preheadRefinedData h chief.toNonScalarChiefFactor (sec7RawTowerPacketCanonical chief K).preheadTowerData X Fdet A Rdet N) L C))

Fused §8 block realization packet (soundness repair #16–#18). Existence-form at full manuscript provenance: the block B is the pinned def-application over the crux-route data (keeping sec7_simpleHeadCruxData3 live and the provenance transparent), and the packet supplies the lift-torsor data L, the children data C, and the local realization of the common partial-count formula (cor:sourceinterface). Replaces the three former free-B axioms centralCover_candidateActualMiddleFrattiniCoherentData, centralCover_localRealizesCandidatePartialFormula, and centralCover_localTateEulerAffineLiftWitness, each falsifiable at junk B/T instantiations (zcard-pinned torsor fibres against canonical source counts; see PROGRESS.md #16–#18). To be discharged by the §8 torsor formalization.

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

The 𝒳_R ≠ 0 sub-branch, proved. A nonzero invariant determinant character turns the raw tower into a MinimalBlock (via the pre-head refinement and the determinant-pushout packets) together with its concrete target-subgroup provenance (R = Φ(K) ≤ K ≤ L_Y, K/R ≃ M), and the (B, Dsub)-parameterized §8 engine yields the Fourier-branch packet.

The 𝒳_R = 0 sub-branch (residual)

axiom Q2Presentation.Induction.sec7_xrzero_liftTorsorChild {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) : ∃ (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)

Residual (lem:obstructionseparation + eq:recursionR1, degenerate 𝒳_R = 0 case; manuscript l.4207-4262 with |𝒳_R| = 1). With no nonzero invariant character on the canonical R, the complete R-obstruction is detected by 𝒳_R = 0, hence vanishes identically: every boundary-framed exact-image map to the middle child B = Y/R lifts, in a torsor of the common size z_R = 2^{2·dim R}, for each source. Existence-form over manuscript-constructed objects: the child (Y/R with the inherited frame, strictly smaller since R ≠ 1), its finite counts, and the two lift-torsor identities.

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

The 𝒳_R = 0 sub-branch (PROVED from the degenerate torsor counts). eq:recursionR1 collapses to e_Γ(Y) = z_R·e_Γ(B): the obstruction space is zero, only χ = 0 exists, and the single child is the strictly smaller B.

The decomposed R ≠ 1 branch

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

The decomposed R ≠ 1 branch: raw tower (residual) + 𝒳_R dichotomy, with the 𝒳_R ≠ 0 side fully proved down to the granular §8 atoms.