Semantic target marked-quotient closers

This sidecar attacks the current target marked/quotient residuals from TargetMarkedQuotientClosers.lean without editing routed files.

Manuscript anchors:

• Section 7, eq:targettower: choose R = Phi(K) <= K <= L_Y, set B = Y/R, C = Y/K, and identify M = K/R;
• Section 8, eq:Mstage/eq:Mdescent: use the marked-kernel exact sequences L_Y -> L_B -> L_C and identify ker(B -> C) with M.

What is proved here:

• the split canonical middle/lower quotient packets are projections of the existing canonical quotient-target packet;
• the split ker(B -> C) -> K/R hom and bijectivity packets are projections of the existing kernel-image equivalence packet;
• the marked restriction packets are split into existing map/kernel packets plus new semantic agreement packets saying that the marked maps are the restrictions of the ambient quotient maps.

The new agreement packets are the genuine remaining semantic content for the marked restrictions: the current API can construct a map L_Y -> L_B or L_B -> L_C and identify its kernel, but it does not yet say that the map is literally the quotient-map restriction.

Canonical quotient targets from canonical quotient data

def Q2Presentation.Induction.targetCanonicalMiddleQuotientData_of_canonical {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetCanonicalQuotientData B D) : CentralCoverTargetCanonicalMiddleQuotientData B D

Project the canonical Y/R quotient target out of the combined canonical quotient packet.

Equations

• Q2Presentation.Induction.targetCanonicalMiddleQuotientData_of_canonical B D Q = { middleChild := Q.middleChild, middleEquiv := Q.middleEquiv }

def Q2Presentation.Induction.targetCanonicalLowerQuotientData_of_canonical {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetCanonicalQuotientData B D) : CentralCoverTargetCanonicalLowerQuotientData B D

Project the canonical Y/K quotient target out of the combined canonical quotient packet.

Equations

• Q2Presentation.Induction.targetCanonicalLowerQuotientData_of_canonical B D Q = { lowerChild := Q.lowerChild, lowerEquiv := Q.lowerEquiv }

theorem Q2Presentation.Induction.centralCover_targetCanonicalMiddleQuotientData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalMiddleQuotientData B D)

The middle quotient target Y/R follows from the canonical quotient-target packet.

theorem Q2Presentation.Induction.centralCover_targetCanonicalLowerQuotientData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalLowerQuotientData B D)

The lower quotient target Y/K follows from the canonical quotient-target packet.

theorem Q2Presentation.Induction.centralCover_targetQuotientChildConcreteData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B (targetSubgroupTowerData_of_concrete B D))

Quotient-child concrete data assembled through the split middle/lower projection theorems above.

Marked restrictions as actual quotient-map restrictions

structure Q2Presentation.Induction.CentralCoverTargetTopMarkedRestrictionAgreementData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedMapData B S Q) : Prop

Agreement saying the selected map L_Y -> L_B is the restriction of the ambient quotient map Y -> B = Y/R.

• topMarkedMap_agrees (x : ↥p.fst.LY) : ↑(D.topMarkedMap x) = Q.topToMiddle ↑x

structure Q2Presentation.Induction.CentralCoverTargetMiddleMarkedRestrictionAgreementData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedMapData B S Q) : Prop

Agreement saying the selected map L_B -> L_C is the restriction of the ambient quotient map B -> C.

• middleMarkedMap_agrees (x : ↥Q.middleChild.fst.LY) : ↑(D.middleMarkedMap x) = Q.middleToLower ↑x

axiom Q2Presentation.Induction.centralCover_targetTopMarkedRestrictionAgreementData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedMapData B S Q) : Nonempty (CentralCoverTargetTopMarkedRestrictionAgreementData B S Q D)

Finer semantic residual: the top marked map agrees with the ambient quotient restriction.

axiom Q2Presentation.Induction.centralCover_targetMiddleMarkedRestrictionAgreementData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedMapData B S Q) : Nonempty (CentralCoverTargetMiddleMarkedRestrictionAgreementData B S Q D)

Finer semantic residual: the middle marked map agrees with the ambient quotient restriction.

def Q2Presentation.Induction.targetTopMarkedRestrictionData_of_mapAgreement {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedMapData B S Q) (A : CentralCoverTargetTopMarkedRestrictionAgreementData B S Q D) : CentralCoverTargetTopMarkedRestrictionData B S Q

Build the top restriction packet from the selected map and its quotient-map agreement.

Equations

• Q2Presentation.Induction.targetTopMarkedRestrictionData_of_mapAgreement B S Q D A = { topMarkedMap := D.topMarkedMap, topMarkedMap_surj := ⋯, topMarkedMap_agrees := ⋯ }

def Q2Presentation.Induction.targetMiddleMarkedRestrictionData_of_mapAgreement {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedMapData B S Q) (A : CentralCoverTargetMiddleMarkedRestrictionAgreementData B S Q D) : CentralCoverTargetMiddleMarkedRestrictionData B S Q

Build the middle restriction packet from the selected map and its quotient-map agreement.

Equations

• Q2Presentation.Induction.targetMiddleMarkedRestrictionData_of_mapAgreement B S Q D A = { middleMarkedMap := D.middleMarkedMap, middleMarkedMap_surj := ⋯, middleMarkedMap_agrees := ⋯ }

theorem Q2Presentation.Induction.centralCover_targetTopMarkedRestrictionData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedRestrictionData B S Q)

The top marked restriction packet is the existing marked-map packet plus the semantic agreement that it is the ambient quotient-map restriction.

theorem Q2Presentation.Induction.centralCover_targetTopMarkedKernelOfRestrictionData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedRestrictionData B S Q) : Nonempty (CentralCoverTargetTopMarkedKernelOfRestrictionData B S Q D)

The kernel of a chosen top restriction follows from the existing kernel packet for its underlying marked map.

theorem Q2Presentation.Induction.centralCover_targetTopMarkedExactData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedExactData B S Q)

Top marked exactness assembled without the old top restriction/kernel residual names.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedRestrictionData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleMarkedRestrictionData B S Q)

The middle marked restriction packet is the existing marked-map packet plus the semantic agreement that it is the ambient quotient-map restriction.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedKernelOfRestrictionData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) : Nonempty (CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q D)

The kernel of a chosen middle restriction follows from the existing kernel packet for its underlying marked map.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedExactData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleMarkedExactData B S Q)

Middle marked exactness assembled without the old middle restriction/kernel residual names.

Middle kernel image from the canonical image equivalence

def Q2Presentation.Induction.targetMiddleKernelImageHomData_of_imageData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (I : CentralCoverTargetMiddleKernelImageData B S Q) : CentralCoverTargetMiddleKernelImageHomData B S Q

Turn the existing equivalence ker(B -> C) ~= K/R into the split hom packet.

Equations

• Q2Presentation.Induction.targetMiddleKernelImageHomData_of_imageData B S Q I = { middleKernelImageHom := I.middleKernelImageEquiv.toMonoidHom }

def Q2Presentation.Induction.targetMiddleKernelImageBijectiveData_of_imageData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (I : CentralCoverTargetMiddleKernelImageData B S Q) : CentralCoverTargetMiddleKernelImageBijectiveData B S Q (targetMiddleKernelImageHomData_of_imageData B S Q I)

The split comparison hom is bijective because it comes from the existing equivalence ker(B -> C) ~= K/R.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelImageData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleKernelImageData B S Q)

The split hom/bijectivity residuals follow from the existing semantic kernel-image equivalence.

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelIdentificationData_from_semanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) : Nonempty (CentralCoverTargetMiddleKernelIdentificationData B (targetSubgroupTowerData_of_concrete B D) Q)

Middle-kernel identification assembled using the semantic kernel-image equivalence and the concrete K/R ~= M bridge.

Final route through the semantic sidecar

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientTowerData_from_selfGroupTower_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CentralCoverTargetCanonicalQuotientTowerData (G.toMinimalBlock h F A R))

Canonical target quotient data for the minimal block built from a Section 7 group tower, using the semantic quotient/marked restriction route in this file.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerSemanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CoverRealization (G.toMinimalBlock h F A R))

Cover realization for the specific block produced by a Section 7 group tower, routed through the semantic marked-quotient sidecar.

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_targetMarkedQuotientSemanticClosers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal branch routed through semantic target marked-quotient closers.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_targetMarkedQuotientSemanticClosers (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursive branch using the semantic target marked-quotient route.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_targetMarkedQuotientSemanticClosers (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursion step using the semantic target marked-quotient nonterminal branch.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_targetMarkedQuotientSemanticClosers (p : FramedPair) : framedCountA p = framedCountQ p

Boundary-framed counts equal through the semantic target marked-quotient route.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetMarkedQuotientSemanticClosers (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Equal finite surjection counts through the semantic target marked-quotient route.