Route197 Section 7/6 determinant lowerer

Route196 exposes the two pushout/determinant atoms

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar gives a Route196-compatible provider whose closure avoids both atoms. The replacement surface is the lower determinant-semantic manuscript surface:

• the standard scalar pushout square/polar packets minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, and minimalBlock_preheadCentralPushoutPolarSymmData;
• the four same-family simple-head determinant pieces minimalBlock_preheadCentralPushoutNaturalitySemanticData, minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData, minimalBlock_preheadCentralPushoutPolarZeroSemanticData, and minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

Manuscript anchors: Section 6 for the scalar determinant square/polar family and Section 7.1, prop:simpleheaddet, for the simple-head determinant pieces.

Lower surface

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute197DeterminantLowerClosers.minimalBlock_preheadRoute197DeterminantLowerSurface {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPreheadCentralPushoutStandardData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semanticData) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semanticData) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semanticData) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semanticData)

Audit-facing Route197 lower surface.

The standard scalar pushout packet exposes the three Section 6 square/polar leaves, while the four semantic determinant packets expose the Section 7.1 simple-head determinant leaves for the same semantic family.

Route196 atom replacements

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute197DeterminantLowerClosers.minimalBlock_preheadActualScalarCentralPushoutData_from_route197DeterminantLowerClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadActualScalarCentralPushoutData D)

Route197 proof of the Route196 actual scalar central-pushout atom from the strictly lower standard square/polar packets.

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute197DeterminantLowerClosers.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_route197DeterminantLowerClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Route197 proof of the Route196 actual simple-head determinant atom for any selected semantic central-pushout family, from the lower Section 7.1 semantic determinant packets.

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute197DeterminantLowerClosers.minimalBlock_preheadRoute196PushoutAtoms_from_route197DeterminantLowerClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (A : MinimalBlockPreheadActualScalarCentralPushoutData D), Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData A.toSemanticData)

Same-family reconstruction of the two Route196 pushout atoms from lower determinant-semantic packets.

This theorem is audit-facing: its closure should contain the seven lower Section 6/7 packets listed in the module header, not the two Route196 atoms.

Drop-in determinant provider

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute197DeterminantLowerClosers.minimalBlock_preheadPushoutRouteLowerData_from_route197DeterminantLowerClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadPushoutRouteLowerData D)

Route197 lower pushout packet through the same-family actual scalar family and the determinant-semantic simple-head proof.

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute197DeterminantLowerClosers.minimalBlock_preheadDeterminantPackets_from_route197DeterminantLowerClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

Drop-in determinant provider for the Route196 nonterminal branch with the pushout/determinant frontier lowered to the seven Section 6/7 packets.