Finer concrete provenance closers for the Section 7 minimal block

This sidecar keeps the routed files untouched. It replaces the four current Section 7 provenance/representation packets in the final route

• minimalBlock_kernelModuleConcreteProvenanceData;
• minimalBlock_dualInvariantVanishesData;
• minimalBlock_rawHeadSimplicityActualData;
• minimalBlock_rawInvariantCharacterData;

by smaller manuscript-shaped obligations on the same selected K/R tower.

Concrete provenance from the existing concrete packets

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteProvenanceData_from_concreteClosers2 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

The coherent provenance packet follows from the five lower concrete kernel/module packets. This removes the newer one-packet provenance axiom by expanding it back into the least-K, Frattini-collapse, raw tower, quotient bridge, and nonzero-head obligations.

Dual-invariant vanishing from two quotient-head packets

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

Invariant functionals on M kill the lower layer T.

• invariant_functionals_kill_T (phi : Module.Dual (ZMod 2) D.M) : (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) → ∀ t ∈ D.T, phi t = 0

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

The quotient head has no trivial dual invariant.

• head_dualInv_zero (psi : Module.Dual (ZMod 2) (D.M ⧸ D.T)) : (∀ (c : D.C), psi ∘ₗ minimalBlock_rawHeadAction D c = psi) → psi = 0

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

Residual radical-killing packet for invariant functionals.

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

Residual no-trivial-dual packet on the quotient head.

def Q2Presentation.Induction.MinimalBlockRawHeadQuotientNoTrivialData.ofHeadDualClosers2 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (K : MinimalBlockRawInvariantFunctionalsKillTData D) (H : MinimalBlockRawHeadDualInvariantZeroData D) : MinimalBlockRawHeadQuotientNoTrivialData D

Assemble the existing quotient-head packet from the two smaller representation-theoretic obligations.

Equations

• ⋯ = ⋯

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

The direct dual-invariant packet follows from the two quotient-head representation packets, without using minimalBlock_dualInvariantVanishesData or the combined minimalBlock_rawHeadQuotientNoTrivialData axiom.

Head simplicity from the nonzero-stable-submodule criterion

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

A simple-module criterion for the quotient head: every nonzero stable submodule is the whole head.

• eq_top_of_nonzero_stable (U : Submodule (ZMod 2) (D.M ⧸ D.T)) : minimalBlock_rawHeadStable D U → (∃ x ∈ U, x ≠ 0) → U = ⊤

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

Residual irreducibility criterion for the quotient head.

def Q2Presentation.Induction.MinimalBlockRawHeadSimplicityActualData.ofNonzeroStableEqTop {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockRawHeadNonzeroStableEqTopData D) : MinimalBlockRawHeadSimplicityActualData D

Convert the nonzero-stable-submodule criterion into the existing head simplicity packet.

Equations

• ⋯ = ⋯

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

The current head-simplicity packet follows from the nonzero-stable-submodule criterion, without using minimalBlock_rawHeadSimplicityActualData.

Raw invariant character from the lower scalar quotient

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

The raw nonzero invariant character follows from the lower scalar quotient, without using minimalBlock_rawInvariantCharacterData.

Same-tower concrete final pieces through the finer split

theorem Q2Presentation.Induction.minimalBlock_provenanceConcreteFinalPieces_from_concreteClosers2 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance pieces through the finer split in this sidecar.

theorem Q2Presentation.Induction.minimalBlock_provenanceSemanticData_from_concreteClosers2 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Route-ready provenance-semantic replacement through the finer split.

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

Route-ready group tower through the finer Section 7 provenance split.