Route138 target K/R closers

This sidecar leaves the routed/public files untouched. It keeps the Route138 candidate and Section 7 providers, but replaces the target Route22 leaves by the lower transport-final K/R bridge atoms:

• centralCover_targetLowerProjectionData, the concrete projection Y -> B.C with kernel K;
• centralCover_targetKmodRProjectedConjugationActionData, the projected conjugation action on the literal quotient K/R.

These are the manuscript-shaped §7--§8 tower facts for Y -> B = Y/R -> C = Y/K and M = K/R.

Route22 target leaf replacements

theorem Q2Presentation.Induction.TargetKmodRRoute138Closers.centralCover_targetRoute22CanonicalLowerActionEquivData_from_route138Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D)

Route138 replacement for Route22's canonical lower-action equivalence leaf.

The equivalence Y/K ~= B.C is induced by the lower transport-final projection Y -> B.C with kernel K.

theorem Q2Presentation.Induction.TargetKmodRRoute138Closers.centralCover_targetRoute22CanonicalRepresentativeActionData_from_route138Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D (TargetKmodRRoute22ActualProofs.canonicalLowerProjectionData_of_route22LowerActionEquiv B D E))

Route138 replacement for Route22's canonical representative-action leaf.

The representative law is obtained from the lower projected-conjugation action by choosing representatives for the canonical Route22 projection.

theorem Q2Presentation.Induction.TargetKmodRRoute138Closers.centralCover_targetRoute138LowerAtomsAudit {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : ∃ (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D), TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P

Audit surface exposing the lower target atoms used instead of the Route22 leaves.

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

Direct target K/R quotient-action provider from the lower Route138 target atoms.

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

Target decoration-kernel provider downstream of the lowered Route138 target bridge.

Route138 context with only the target provider swapped

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

Route138 cover realization with the target Route22 leaves lowered to the transport-final lower projection and projected K/R conjugation atoms.

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

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

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