Route167 target K/R quotient/action closers

Route166's target frontier contains the four coherent Route164 projection and representative-action atoms. This sidecar replaces that Route164 packet by the lower manuscript-shaped projection/action bridge already isolated in TargetKmodRProjectionSemanticClosers:

• a literal lower quotient map Y -> Y/K;
• an equivalence from that lower child to the abstract action group B.C;
• representative-level action on K/R;
• class-independence of quotient conjugation on K/R.

The Route164 surface is rebuilt theorem-level from those lower packets only so the downstream decoration-kernel provider is a drop-in replacement for TargetKmodRRoute164Closers.centralCover_targetDecorationKernelData_from_route152Closers_route164 without depending on any Route164 residual declarations.

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

Route167 coherent replacement for the four Route164 target atoms.

• lowerProjectionMapData : TargetKmodRRoute164Closers.CentralCoverTargetRoute164LowerProjectionMapData B D
• lowerProjectionSurjectivityData : TargetKmodRRoute164Closers.CentralCoverTargetRoute164LowerProjectionSurjectivityData B D self.lowerProjectionMapData
• lowerProjectionKernelData : TargetKmodRRoute164Closers.CentralCoverTargetRoute164LowerProjectionKernelData B D self.lowerProjectionMapData
• representativeActionData : TargetKmodRRoute164Closers.CentralCoverTargetRoute164RepresentativeActionData B D self.lowerProjectionMapData ⋯

def Q2Presentation.Induction.TargetKmodRRoute167Closers.route164Packet_of_projectionSemantic {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P) : CentralCoverTargetRoute167AsRoute164Data B D

Rebuild the Route164 coherent projection/action packet from the lower projection-semantic bridge.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute167Closers.centralCover_targetRoute164Data_from_route167Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute167AsRoute164Data B D)

Route167 proves the Route164 projection/action surface from lower semantic projection/action packets, without using the Route164 residual axioms.

theorem Q2Presentation.Induction.TargetKmodRRoute167Closers.centralCover_targetKmodRProjectedConjugationActionData_from_route167Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route167 projected-action provider through the rebuilt Route164 bridge surface.

theorem Q2Presentation.Induction.TargetKmodRRoute167Closers.centralCover_targetKmodRQuotientActionData_from_route167Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route167 quotient-action provider.

theorem Q2Presentation.Induction.TargetKmodRRoute167Closers.centralCover_targetDecorationKernelData_from_route167Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetDecorationKernelData B D)

Route167 drop-in target decoration-kernel provider.

theorem Q2Presentation.Induction.TargetKmodRRoute167Closers.centralCover_targetDecorationKernelData_from_route152Closers_route167 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetDecorationKernelData B D)

Name mirroring the Route164 call site for a one-line replacement.

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

Convenience framed-quotient provider through Route167.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated167TargetRoute167 {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))

Route167 cover realization: Route166's candidate, pushout, and kernel providers with the target Route164 provider replaced by Route167.

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated167TargetRoute167 (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_currentIntegrated167TargetRoute167 (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_currentIntegrated167TargetRoute167 (p : FramedPair) : framedCountA p = framedCountQ p

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