Actual Section 7 invariant packet, third pass

This sidecar refines the residual

minimalBlock_invariantActualProofs2Data : Nonempty (MinimalBlockInvariantActualProofs2Data D).

The previous packet asked, in one axiom, for both the first non-scalar head mechanism and the lower scalar invariant character. Here those are split along the manuscript proof of lem:simplehead and the scalar lower-layer construction:

• quotient-head simplicity is the only new head-side residual;
• the head action is proved nontrivial from no-trivial-dual plus the known nonzero simple head;
• the lower invariant character hitting 1 is proved from the scalar quotient packet.

The route theorems at the bottom replace uses of minimalBlock_invariantActualProofs2Data without editing routed files.

First non-scalar quotient head

structure Q2Presentation.Induction.MinimalBlockRawHeadSimplicityActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

The remaining irreducibility part of lem:simplehead for the raw quotient head M/T.

This is narrower than MinimalBlockRawHeadSimpleNoTrivialActualData: it asserts only that the quotient head has no nontrivial stable submodules. The radical-killing/no-trivial-dual fields come from MinimalBlockRawHeadQuotientNoTrivialData, and nontriviality of the action is proved below.

• head_simple (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : minimalBlock_rawHeadStable D U → U = ⊥ ∨ U = ⊤

axiom Q2Presentation.Induction.minimalBlock_rawHeadSimplicityActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadSimplicityActualData D)

Residual head-simplicity packet for the first non-scalar layer.

def Q2Presentation.Induction.MinimalBlockRawHeadSimpleNoTrivialActualData.ofSimplicityActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : MinimalBlockRawHeadQuotientNoTrivialData D) (N : MinimalBlockHeadNontrivialData D) (S : MinimalBlockRawHeadSimplicityActualData D) : MinimalBlockRawHeadSimpleNoTrivialActualData D

Assemble the stronger head packet used by ActualProofs2 from the quotient no-trivial-dual packet, nonzero-head data, and the new head-simplicity residual.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_rawHeadSimpleNoTrivialActualData_from_simplicityActual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadSimpleNoTrivialActualData D)

Head side of ActualProofs2, now split so the only new residual is quotient-head simplicity.

theorem Q2Presentation.Induction.minimalBlock_rawHeadSimpleNoTrivialActualData_from_lowerSimplicityActual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockRawHeadSimpleNoTrivialActualData D.rawTowerData)

Coherent head side for a selected lower group/module tower, using the head nontriviality field already attached to that same tower.

Lower scalar layers and invariant character

def Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofLowerScalarQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (Q : MinimalBlockRawLowerScalarQuotientData D) : MinimalBlockRawLowerInvariantCharacterActualData D

A scalar quotient of R supplies the actual lower invariant character used by ActualProofs2: surjectivity gives an element hitting 1.

Equations

• Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofLowerScalarQuotient Q = { character := Q.quotient, character_hits_one := ⋯, character_invariant := ⋯ }

theorem Q2Presentation.Induction.minimalBlock_rawLowerInvariantCharacterActualData_from_lowerScalarQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterActualData D)

Lower scalar side of ActualProofs2, proved from the existing scalar quotient packet.

Same-tower replacement for minimalBlock_invariantActualProofs2Data

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_proven {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D)

The ActualProofs2 packet with its monolithic axiom replaced by smaller manuscript-shaped packets:

• raw head no-trivial-dual;
• raw head nontriviality;
• raw head simplicity;
• lower scalar quotient.

The axiom closure of this theorem does not contain minimalBlock_invariantActualProofs2Data.

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_lowerSimplicityActual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D.rawTowerData)

Same replacement, but tied to a selected coherent lower group/module tower so the nonzero-head witness is not reselected separately.

Route-ready projections without the ActualProofs2 axiom

theorem Q2Presentation.Induction.minimalBlock_rawHeadQuotientNoTrivialData_from_invariantActualProofs3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadQuotientNoTrivialData D)

theorem Q2Presentation.Induction.minimalBlock_rawLowerScalarQuotientData_from_invariantActualProofs3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerScalarQuotientData D)

theorem Q2Presentation.Induction.minimalBlock_dualInvariantVanishesData_from_invariantActualProofs3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockDualInvariantVanishesData D)

theorem Q2Presentation.Induction.minimalBlock_rawInvariantCharacterData_from_invariantActualProofs3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantCharacterData D)

theorem Q2Presentation.Induction.minimalBlock_invariantSemanticData_from_invariantActualProofs3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockInvariantSemanticData D)

theorem Q2Presentation.Induction.minimalBlock_groupInvariantRouteData_from_invariantActualProofs3 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route packet assembled from the lower group/module proof and the third-pass same-raw-tower invariant split.

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_invariantActualProofs3 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_invariantActualProofs3 (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal Fourier branch through the third-pass invariant split.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_invariantActualProofs3 (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_invariantActualProofs3 (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_invariantActualProofs3 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_invariantActualProofs3 (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Count equality theorem through the third-pass invariant split.