Further Section 7 packet closers

This sidecar keeps the currently routed CountsEqualDeaxiom closure untouched. It records the cleanest next refinement of the minimal-block packets: the pre-head scalar quotient is derived from the manuscript's actual input, a nonzero invariant character in (R^vee)^C.

Compared with routing through minimalBlock_preheadScalarQuotientData, this replaces a chosen surjective scalar quotient by the smaller nonzero-character residual. The surjectivity field is then theorem-level over F_2, via minimalBlock_preheadScalarQuotientData_from_invariantCharacter in MinimalBlockPacketClosers.

Pre-head scalar quotient from invariant characters

axiom Q2Presentation.Induction.minimalBlock_preheadInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadInvariantCharacterData D)

Residual Section 7 axiom: nonzero pre-head invariant determinant character.

Manuscript anchor: the determinant character space X_R = (R^vee)^B = (R^vee)^C used in the simple-head determinant pushouts on page 42. This is weaker and more literal than a pre-selected scalar quotient: over F_2, any nonzero character is automatically onto F_2, so the quotient packet is reassembled below as a theorem.

theorem Q2Presentation.Induction.minimalBlock_preheadScalarQuotientData_from_characterResidual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadScalarQuotientData D)

Reassemble the old pre-head scalar-quotient packet from the smaller invariant character residual.

theorem Q2Presentation.Induction.minimalBlock_preheadNonzeroInvariantCharacterData_from_characterResidual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadInvariantCharacterData D)

The pre-head nonzero-character interface used by minimalBlock_of_preheadRefinedData is exactly the new residual.

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_proven_character_refined (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

Alternative exact replacement for minimalBlock_of_nonScalar_proven_refined with the scalar quotient residual replaced by the nonzero invariant-character residual. This is a sidecar route only; CountsEqualDeaxiom is not rerouted here.

Acceptance checks