Proper-image restriction semantic closers

This sidecar splits the remaining canonical restriction residual from ProperImageExactClosers.lean into the three semantic facts used in the manuscript proof of eq:Mdescent.

For every proper exact-image subgroup J < B mapping onto C, the actual quotient map B -> C should restrict to a surjective map J ∩ L_B -> L_C, and the kernel of B -> C should lie in L_B. The kernel-equivalence and literal-intersection parts are already theorem-level in ProperImageExactClosers; this file isolates only those three restriction facts and reassembles the older canonical restriction packet from them.

Split semantic restriction packets

structure Q2Presentation.Induction.CentralCoverElementaryProperImageMiddleKernelMarkedData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Prop

The middle kernel of the actual quotient map B -> C lies in the marked kernel L_B. This is the membership needed to view J ∩ ker(B -> C) as a subgroup of J ∩ L_B.

• middleKernel_le_marked (z : ↥T.middleToLower.ker) : ↑z ∈ T.middleChild.fst.LY

structure Q2Presentation.Induction.CentralCoverElementaryProperImageMapsToLowerMarkedData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Prop

The actual quotient map B -> C sends each proper exact-image marked intersection J ∩ L_B into L_C.

• mapsToLowerMarked (i : CentralCoverElementaryProperExactImageSubgroups T) (x : ↥(T.middleChild.fst.LY.subgroupOf ↑i)) : T.middleToLower (elementaryProperImageRestrictedDomainVal x) ∈ T.lowerChild.fst.LY

structure Q2Presentation.Induction.CentralCoverElementaryProperImageRestrictedSurjData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Prop

The restricted quotient map J ∩ L_B -> L_C is onto for each proper exact-image subgroup appearing in the elementary subtraction.

• restricted_surj (i : CentralCoverElementaryProperExactImageSubgroups T) (y : ↥T.lowerChild.fst.LY) : ∃ (x : ↥(T.middleChild.fst.LY.subgroupOf ↑i)), T.middleToLower (elementaryProperImageRestrictedDomainVal x) = ↑y

def Q2Presentation.Induction.elementaryProperImageCanonicalRestrictionData_of_semanticParts {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageMiddleKernelMarkedData B T) (M : CentralCoverElementaryProperImageMapsToLowerMarkedData B T) (S : CentralCoverElementaryProperImageRestrictedSurjData B T) : CentralCoverElementaryProperImageCanonicalRestrictionData B T

Reassemble the older canonical restriction packet from the three narrower semantic facts.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCanonicalRestrictionData_from_semanticParts {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageMiddleKernelMarkedData B T) → Nonempty (CentralCoverElementaryProperImageMapsToLowerMarkedData B T) → Nonempty (CentralCoverElementaryProperImageRestrictedSurjData B T) → Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B T)

Nonempty reassembly of the canonical restriction packet from split semantic restriction packets.

Residual names at the split semantic layer

axiom Q2Presentation.Induction.centralCover_elementaryProperImageMiddleKernelMarkedData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageMiddleKernelMarkedData B T)

Semantic residual: ker(B -> C) <= L_B.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageMapsToLowerMarkedData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageMapsToLowerMarkedData B T)

Semantic residual: the actual map B -> C maps J ∩ L_B into L_C.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedSurjData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageRestrictedSurjData B T)

Semantic residual: the actual restricted map J ∩ L_B -> L_C is surjective.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCanonicalRestrictionData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B T)

Replacement for the old one-piece canonical restriction residual. The closure of this theorem names only the three split semantic packets above.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCardinalityData_from_restrictionSemanticClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverMiddleKernelEquivData B T) → Nonempty (CentralCoverElementaryProperImageCardinalityData B T)

Proper-image cardinality data using the split semantic restriction packets, not the old one-piece residual axiom.