Semantic invariant proofs for Section 7 minimal blocks

This sidecar targets the two invariant residuals that feed the lower Section 7 minimal-block route:

• minimalBlock_dualInvariantVanishesData;
• minimalBlock_rawInvariantCharacterData.

It does not edit any routed file. The manuscript-shaped narrowing is the same tower used on pages 40--42: after extracting the raw tower R, M, T, C, the simple-head argument supplies the no-trivial-dual quotient statement, and the scalar lower layers supply an invariant scalar quotient of R.

The two theorem-level replacements below therefore depend only on the already split lower invariant packets minimalBlock_rawHeadQuotientNoTrivialData and minimalBlock_rawLowerScalarQuotientData, not on the two broader residuals named above.

Same-tower invariant semantic packet

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

Same-tower semantic data for the Section 7 invariant step.

The first field is the Lean form of the manuscript argument for (M^vee)^C = 0: invariant functionals kill the scalar radical/prehead part T, and the quotient head has no trivial dual invariant.

The second field is the scalar-lower-layer input: the Frattini layer R has a C-invariant scalar quotient. Over F_2, this is exactly the nonzero invariant determinant character used later in X_R = (R^vee)^C.

• headNoTrivial : MinimalBlockRawHeadQuotientNoTrivialData D
• lowerScalarQuotient : MinimalBlockRawLowerScalarQuotientData D

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

Recover (M^vee)^C = 0 from the quotient-head statement.

Equations

• ⋯ = ⋯

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

Recover the raw invariant determinant character from the scalar quotient.

Equations

• ⋯ = ⋯

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

Assemble the same-tower invariant semantic packet from the two narrower manuscript-shaped residuals already present in the API.

The two requested theorem-level replacements

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

Theorem-level replacement for minimalBlock_dualInvariantVanishesData.

This is the manuscript's (M^vee)^C = 0 conclusion, narrowed to the quotient-head no-trivial-dual packet.

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

Theorem-level replacement for minimalBlock_rawInvariantCharacterData.

This is the invariant-character conclusion narrowed to the scalar quotient of the lower Frattini layer.

Route-ready reassembly for MinimalBlockLowerGroupProofs users

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

Route packet assembled from the coherent lower group/module proof and the narrowed invariant semantic replacements above.

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

Group-tower reassembly through the narrowed invariant semantic route.