Actual Section 7 invariant packet, second pass

This sidecar keeps the edit isolated while narrowing the two current final-route invariant residuals

• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawLowerScalarQuotientData.

The new residual is attached to one selected raw tower. On the head side it records the manuscript simple-head mechanism: invariant codimension-one kernels contain T, the quotient head has no nontrivial stable submodules, and the head action is not trivial. On the scalar side it records only a C-invariant character of R that hits 1; surjectivity to F_2 is then proved here.

The route theorem below constructs MinimalBlockGroupInvariantRouteData without calling either of the two residual axioms named above.

Simple-head no-trivial-quotient data

def Q2Presentation.Induction.minimalBlock_rawHeadStable {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : Prop

A submodule of the raw quotient head M/T is stable under the induced C-action.

Equations

• Q2Presentation.Induction.minimalBlock_rawHeadStable D U = ∀ (c : D.C), ∀ x ∈ U, (Q2Presentation.Induction.minimalBlock_rawHeadAction D c) x ∈ U

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

Manuscript-shaped replacement for the head packet.

The first field is the radical/minimality statement used to force invariant functionals on M to kill T. The second and third fields say the quotient head is simple and not the trivial C-module; together these prove that the head has no invariant dual quotient.

• invariant_kernels_contain_T (phi : Module.Dual (ZMod 2) D.M) : phi ≠ 0 → (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) → ∀ t ∈ D.T, phi t = 0
• head_simple (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : minimalBlock_rawHeadStable D U → U = ⊥ ∨ U = ⊤
• head_action_nontrivial : ∃ (c : D.C) (x : D.M ⧸ D.T), (minimalBlock_rawHeadAction D c) x ≠ x

def Q2Presentation.Induction.MinimalBlockRawHeadQuotientNoTrivialData.ofSimpleNoTrivialActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : MinimalBlockRawHeadSimpleNoTrivialActualData D) : MinimalBlockRawHeadQuotientNoTrivialData D

Convert the simple-head actual packet into the currently routed head-quotient packet.

Equations

• ⋯ = ⋯

Lower scalar character data

structure Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Type

Lower scalar invariant-character data. This is weaker than asking for a surjective quotient map: over F_2, hitting 1 already proves surjectivity.

• character : Module.Dual (ZMod 2) D.R
• character_hits_one : ∃ (r : D.R), self.character r = 1
• character_invariant (c : D.C) : self.character ∘ₗ ↑(D.actR c) = self.character

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

A lower invariant character hitting 1 gives the current lower scalar quotient packet.

Equations

• Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofInvariantCharacterActual Q = { quotient := Q.character, quotient_surjective := ⋯, quotient_invariant := ⋯ }

Same raw-tower packet and route projections

structure Q2Presentation.Induction.MinimalBlockInvariantActualProofs2Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Type

Coherent actual invariant packet for one raw tower.

• head : MinimalBlockRawHeadSimpleNoTrivialActualData D
• lowerCharacter : MinimalBlockRawLowerInvariantCharacterActualData D

def Q2Presentation.Induction.MinimalBlockInvariantActualProofs2Data.headQuotientNoTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockRawHeadQuotientNoTrivialData D

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockInvariantActualProofs2Data.lowerScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockRawLowerScalarQuotientData D

Equations

• S.lowerScalarQuotientData = Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofInvariantCharacterActual S.lowerCharacter

def Q2Presentation.Induction.MinimalBlockInvariantActualProofs2Data.dualInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockDualInvariantVanishesData D

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockInvariantActualProofs2Data.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockRawInvariantCharacterData D

Equations

• ⋯ = ⋯

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

New smaller same-tower Section 7 invariant residual.

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

Route-ready theorem deriving the old head packet from the new smaller same-tower packet. Its axiom closure does not contain minimalBlock_rawHeadQuotientNoTrivialData.

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

Route-ready theorem deriving the old lower scalar packet from the new smaller same-tower packet. Its axiom closure does not contain minimalBlock_rawLowerScalarQuotientData.

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

The old dual-invariant conclusion, routed through the new smaller packet.

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

The old raw invariant-character conclusion, routed through the new smaller packet.

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

Coherent semantic packet assembled from the new same-tower residual.

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

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

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

Group-tower reassembly through the new invariant packet.

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

Nonterminal Fourier branch through the new invariant packet.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_invariantActualProofs2 (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)

Recursive branch through the new invariant packet.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_invariantActualProofs2 (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)

Recursion step through the new invariant packet.

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

Boundary-framed count equality through the new invariant packet.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_invariantActualProofs2 (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 new invariant packet.