Final provenance-semantic closers for the Section 7 minimal block

This sidecar keeps the routed files untouched and proves a route-ready replacement for the residual packet

minimalBlock_provenanceSemanticData : Nonempty (MinimalBlockProvenanceSemanticData chief).

The construction is tied to one concrete subgroup tower. The lower raw tower is definitionally the one extracted from MinimalBlockKernelModuleConcreteProvenanceData, so the head and lower scalar packets cannot be chosen on a different K/R tower.

The concrete lower tower selected by provenance

def Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockLowerGroupModuleData chief

The lower group/module tower definitionally extracted from one concrete Section 7 provenance packet.

Equations

• Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance P = (Q2Presentation.Induction.MinimalBlockKernelModuleConcreteBundle.ofProvenance P).actualProofs.lowerGroupModuleData

Manuscript-shaped final pieces

structure Q2Presentation.Induction.MinimalBlockProvenanceFinalPieces {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

The remaining final-closure pieces for the provenance-semantic packet, all attached to the raw tower forced by the same concrete K/R provenance.

Fields correspond to the manuscript Section 7 steps:

• concrete subgroup provenance: least K, R = Phi(K), M = K/R, T, C, action, bridge, Frattini-collapse facts;
• no-trivial-dual quotient-head data from lem:simplehead;
• quotient-head simplicity for the first non-scalar head;
• lower scalar quotient/invariant character on the Frattini layer.

• concrete : MinimalBlockKernelModuleConcreteProvenanceData chief
• headNoTrivial : MinimalBlockRawHeadQuotientNoTrivialData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData
• headSimplicity : MinimalBlockRawHeadSimplicityActualData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData
• lowerScalar : MinimalBlockRawLowerScalarQuotientData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData

def Q2Presentation.Induction.MinimalBlockProvenanceFinalPieces.lower {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceFinalPieces chief) : MinimalBlockLowerGroupModuleData chief

The selected lower tower.

Equations

• P.lower = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance P.concrete

def Q2Presentation.Induction.MinimalBlockProvenanceFinalPieces.headActual {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceFinalPieces chief) : MinimalBlockRawHeadSimpleNoTrivialActualData P.lower.rawTowerData

The actual simple/no-trivial head packet on the selected lower tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockProvenanceFinalPieces.lowerCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceFinalPieces chief) : MinimalBlockRawLowerInvariantCharacterActualData P.lower.rawTowerData

The actual lower invariant character packet on the selected lower tower.

Equations

• P.lowerCharacter = Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofLowerScalarQuotient P.lowerScalar

def Q2Presentation.Induction.MinimalBlockProvenanceFinalPieces.toProvenanceSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceFinalPieces chief) : MinimalBlockProvenanceSemanticData chief

Convert the explicit final pieces into the route packet used by MinimalBlockProvenanceSemanticProofs.

Equations

• P.toProvenanceSemanticData = { concrete := P.concrete, lower := P.lower, lower_eq_concrete := ⋯, headActual := ⋯, lowerCharacter := P.lowerCharacter }

Closers

theorem Q2Presentation.Induction.minimalBlock_provenanceFinalPieces_from_existingClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceFinalPieces chief)

The manuscript-shaped final pieces follow from the current concrete provenance closer plus the three remaining raw-tower representation/scalar packets on the raw tower forced by that provenance.

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

Route-ready replacement for the residual axiom minimalBlock_provenanceSemanticData. This theorem has the same mathematical target, but its axiom closure is the smaller manuscript-shaped split exposed in MinimalBlockProvenanceFinalPieces.

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

The group/invariant route packet with the provenance-semantic residual closed through the final pieces above.

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

The group tower consumed by determinant and central-cover routes, using the final provenance closers rather than the minimalBlock_provenanceSemanticData axiom.