Framed target marked-quotient proof packet

This sidecar lowers the four current Section 8 target-side residual packets in the final route to one coherent framed quotient packet.

The current API has theorem-level quotient-map algebra once quotient children are supplied, but it does not construct quotient boundary-framed targets from a normal subgroup killed by both piY and the decoration thetaY. In particular, it has no field asserting the manuscript fact that the decorations vanish on the block K (lem:decorationblock). Therefore the fully framed quotient constructor is still a real residual.

The packet below keeps the quotient children, inherited marked kernels, and the restricted marked maps tied to the same canonical quotient tower Y -> Y/R -> Y/K. Downstream projections are theorem-level.

One coherent framed target quotient packet

def Q2Presentation.Induction.targetQuotientChildEquivData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetQuotientChildEquivData B (targetSubgroupTowerData_of_concrete B D)

Quotient-child equivalences extracted from a framed quotient witness.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.targetQuotientMapsData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)

The ambient quotient maps belonging to a framed quotient witness.

Equations

• One or more equations did not get rendered due to their size.

structure Q2Presentation.Induction.CentralCoverTargetFramedMarkedQuotientData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type 1

Coherent lower packet for the framed quotients and inherited marked maps.

Unlike the four independently quantified residuals, all fields here refer to the same framed quotient witnesses and the quotient maps derived from them.

• framed : CentralCoverTargetCanonicalFramedQuotientData B D
• topMarked : CentralCoverTargetTopMarkedRestrictionSurjData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D self.framed)
• middleMarked : CentralCoverTargetMiddleMarkedRestrictionSurjData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D self.framed)
• middleAmbientKernelMarked : CentralCoverTargetMiddleAmbientKernelMarkedData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D self.framed)

axiom Q2Presentation.Induction.centralCover_targetFramedMarkedQuotientData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetFramedMarkedQuotientData B D)

The remaining framed quotient-constructor residual.

Projections to the old four target packets

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

The old canonical framed quotient packet is a projection of the coherent framed quotient packet.

theorem Q2Presentation.Induction.centralCover_targetTopMarkedRestrictionSurjData_from_framedProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : ∃ (F : CentralCoverTargetCanonicalFramedQuotientData B D), Nonempty (CentralCoverTargetTopMarkedRestrictionSurjData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F))

Top marked restriction for the quotient maps attached to the coherent framed quotient packet.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedRestrictionSurjData_from_framedProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : ∃ (F : CentralCoverTargetCanonicalFramedQuotientData B D), Nonempty (CentralCoverTargetMiddleMarkedRestrictionSurjData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F))

Middle marked restriction for the quotient maps attached to the coherent framed quotient packet.

theorem Q2Presentation.Induction.centralCover_targetMiddleAmbientKernelMarkedData_from_framedProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : ∃ (F : CentralCoverTargetCanonicalFramedQuotientData B D), Nonempty (CentralCoverTargetMiddleAmbientKernelMarkedData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F))

Middle ambient kernel markedness for the quotient maps attached to the coherent framed quotient packet.

Route-ready reassembly through the coherent packet

def Q2Presentation.Induction.targetTopMarkedExactData_of_framedPacket {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetFramedMarkedQuotientData B D) : CentralCoverTargetTopMarkedExactData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F.framed)

Top marked exactness for the quotient maps attached to a framed quotient witness.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.targetMiddleMarkedExactData_of_framedPacket {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetFramedMarkedQuotientData B D) : CentralCoverTargetMiddleMarkedExactData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F.framed)

Middle marked exactness for the quotient maps attached to a framed quotient witness.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.targetMiddleMarkedRestrictionData_of_framedPacket {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetFramedMarkedQuotientData B D) : CentralCoverTargetMiddleMarkedRestrictionData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F.framed)

The middle marked restriction and kernel data needed by the proper-image sidecar, extracted from a framed quotient packet.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.targetMiddleMarkedKernelOfRestrictionData_of_framedPacket {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetFramedMarkedQuotientData B D) : CentralCoverTargetMiddleMarkedKernelOfRestrictionData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F.framed) (targetMiddleMarkedRestrictionData_of_framedPacket B D F)

Kernel identification for the middle marked restriction extracted from a framed quotient packet.

Equations

• One or more equations did not get rendered due to their size.

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

Canonical target quotient tower for a block produced by a Section 7 group tower, using the single coherent framed quotient packet.

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

Cover realization through the coherent framed target marked-quotient packet.

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

Nonterminal branch through the coherent framed target marked-quotient packet.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_framedProofs (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)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_framedProofs (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)

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetMarkedQuotientFramedProofs (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 coherent framed quotient packet.